Hacker News new | ask | show | jobs
by dependenttypes 2172 days ago
You can still do

    data TC x where
      DC :: Ord x => x -> TC x
1 comments

Yes, 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!