[Haskell-cafe] GADT is not great - sometimes: can be almost as stupid as stupid theta

[Viktor Dukhovni]

On Fri, Sep 11, 2020 at 06:19:27PM +1200, Anthony Clayden wrote:

>     data SetG a  where
>       NilSetG  :: Eq a => SetG a
>       ConsSetG :: Eq a => a -> SetG a -> SetG a
> 
>     elemSG x NilSetG                     = False
>     elemSG x (ConsSetG y ys) | x == y    = True
>                              | otherwise = elemSG x ys
>       -- ===> elemSG :: a -> SetG a -> Bool  -- no Eq a inferred

This, as I am sure you're aware, is correct, but I'd also say
unsurprising.  The function indeed works for all `a`, it is just that
for many `a` (those without an 'Eq' instance) the type `SetG a` is
uninhabited, so the function is correct vacuously.

I wouldn't describe this situation as there being something "stupid"
with GADTs.  The function is defined for all `a` and `SetG a`, even when
`SetG a` is uninhabited.  Once all the constructors imply the requisite
constraints, the functions are automatically safe for all, possibly
uninhabited, `SetG a` types.

With this particular type, I'd argue the real problem is adding the
constraints to the constructors in the first place.  With the
constructors unconstrained, one gains the ability to define Functor
instances, use Applicatives, ...  And the constraints can be imposed on
individual functions that actually test equality.

Yes, with the deprecated `DatatypeContexts` the constraint does
propagate to the use site (though one still needs to specify it
explicitly, as with "unFoo" below), but there are still some anomalies:

    λ> :set -XFlexibleContexts
    λ> :set -XDatatypeContexts

    <no location info>: warning:
        -XDatatypeContexts is deprecated: ...
    λ> data (Eq a) => Foo a = Foo a deriving Show
    λ> unFoo :: Eq a => Foo a -> a; unFoo (Foo a) = a
    λ> let x = Foo id
    λ> unFoo x (1 :: Int)

    <interactive>:12:1: error:
        • No instance for (Eq (Int -> Int))
        ...

So, even with the constraint in place, we still got to define a
(largely) uninhabited "x" term:

    x :: Eq (a -> a) =>  Foo (a -> a)
    x = Foo id

Though of course one can arrange for a few special cases:

    instance Eq (() -> ()) where
        f == g = f () == g ()
    instance Eq (Bool -> Bool) where
        f == g = f False == g False && f True == g True

Which then allow:

    λ> unFoo x True
    True

The same naturally extends to the GADT case:

    λ> let x = ConsSetG id NilSetG
    λ> elemSG (id :: Bool -> Bool) x -- Given above instance
    True

    λ> elemSG (id :: String -> String) x

    <interactive>:39:33: error:
        • No instance for (Eq (String -> String)) arising from a use of ‘x’
          ...

-- 
    Viktor.