GADT's displayed type is misleading
:t alleges these three data constructors have the same type
:: Int -> T Int (modulo name of the type constructor):
data DG a where MkDG :: Int -> DG Int MkDG2 :: (a ~ Int) => a -> DG a data family DF a data instance DF Int where MkDF :: Int -> DF Int
I tried switching on verbosity flags, but to no avail:
-fprint-explicit-foralls, -fprint-equality-relations, and a few others.
DG constructors are GADTs, the
DF constructor is not. So it's not hard to see different type-level behaviour:
f (MkDF x) = x -- accepted without a signature -- f :: DF Int -> Int -- inferred signature, or you can spec it -- f :: DF a -> a -- rejected: signature is too general/ -- a is a rigid type variable g (MkDG x) = x -- } without a signature, rejected g (MkDG2 x) = x -- } "untouchable" type (Note) -- g :: DG Int -> Int -- } g accepted with either sig -- g :: DG a -> a -- } ?but MkDG doesn't return DG a, allegedly
Note: at least the error message re
MkDG2 does show its type as
:: (forall a). (a ~ Int) => DG a -> a. But doggedly
MkDG :: Int -> DG Int.
"Untouchable" error messages are a fertile source of questions on StackOverflow. The message does say
Possible fix: add a type signature for 'g', but gives no clue what the signature might be.
If you've imported these data constructors from a library, such that you can't (easily) see they're GADTs, couldn't
:t give you better help to show what's going on? Or should one of the verbosity flags already do this?