3 ms·
You can still do data TC x where DC :: Ord x => x -> TC x
by dependenttypes 6y ago
You can still do
data TC x where
DC :: Ord x => x -> TC x
- nybble41 6y agoYes, but that doesn't mean quite the same thing. With the constraint on the type (data Ord x => TC x = DC x) you can be sure that `x` implements `Ord` for any type `TC x`. In your GADT, however, the constraint only applies to the DC constructor, so `x` is only guaranteed to implement `Ord` when you actually have a value inside a `DC` constructor. If you don't match on the constructor then there might not be an `Ord` instance: -- `Ord x` exists when matching on DC constructor ex1 :: TC x -> x -> x -> Ordering ex1 (DC _) a b = compare a b -- Without constructor match, no Ord instance ex2 :: TC x -> x -> x -> Ordering ex2 _ a b = compare a b -- ERROR! -- This is why the above ex2 definition is an error badUser :: x -> x -> Ordering badUser a b = ex2 undefined a b -- No `TC x` value also means no Ord instance even -- though no arguments are ignored or undefined data Proxy x = Proxy ex2 :: Proxy (TC x) -> x -> x -> Ordering ex2 Proxy a b = compare a b -- ERROR!