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.