GADT's displayed type is misleading
GHCi's :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.
The 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?
Trac metadata
Trac field | Value |
---|---|
Version | 8.6.1-beta1 |
Type | FeatureRequest |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | Windows |
Architecture | x86_64 (amd64) |