GADT Constraint breaks type inference
The following code compiles:
{-# LANGUAGE TypeFamilies,
MultiParamTypeClasses, GADTs #-}
module Foo () where
class (Num src, Num tgt) => Bar src tgt where
bar :: (tgt, src)
type family Type a
data CT :: (* -> * -> *) where
CT :: --(Type rp ~ Type rq) =>
rp -> rq -> CT rp rq
foo :: (Bar rp rq) => CT rp rq -> CT rp rq
foo = let (b', a') = bar
in \(CT a b) -> CT (a * a') (b * b')
But when I add the [totally irrelevant] constraint to the GADT, foo
no longer compiles:
Foo.hs:16:22:
Could not deduce (Bar t1 t0) arising from a use of ‘bar’
from the context (Bar rp rq)
bound by the type signature for
foo :: Bar rp rq => CT rp rq -> CT rp rq
at testsuite/Foo.hs:15:8-42
The type variables ‘t0’, ‘t1’ are ambiguous
Relevant bindings include
b' :: t0 (bound at Foo.hs:16:12)
a' :: t1 (bound at Foo.hs:16:16)
In the expression: bar
In a pattern binding: (b', a') = bar
In the expression:
let (b', a') = bar in \ (CT a b) -> CT (a * a') (b * b')
Foo.hs:17:31:
Couldn't match expected type ‘rp’ with actual type ‘t1’
‘t1’ is untouchable
inside the constraints (Type rp ~ Type rq)
bound by a pattern with constructor
CT :: forall rp rq. Type rp ~ Type rq => rp -> rq -> CT rp rq,
in a lambda abstraction
at Foo.hs:17:12-17
‘rp’ is a rigid type variable bound by
the type signature for foo :: Bar rp rq => CT rp rq -> CT rp rq
at testsuite/Foo.hs:15:8
Relevant bindings include
a :: rp (bound at Foo.hs:17:15)
a' :: t1 (bound at Foo.hs:16:16)
foo :: CT rp rq -> CT rp rq (bound at Foo.hs:16:1)
In the second argument of ‘(*)’, namely ‘a'’
In the first argument of ‘CT’, namely ‘(a * a')’
Foo.hs:17:40:
Couldn't match expected type ‘rq’ with actual type ‘t0’
‘t0’ is untouchable
inside the constraints (Type rp ~ Type rq)
bound by a pattern with constructor
CT :: forall rp rq. Type rp ~ Type rq => rp -> rq -> CT rp rq,
in a lambda abstraction
at Foo.hs:17:12-17
‘rq’ is a rigid type variable bound by
the type signature for foo :: Bar rp rq => CT rp rq -> CT rp rq
at Foo.hs:15:8
Relevant bindings include
b :: rq (bound at Foo.hs:17:17)
b' :: t0 (bound at Foo.hs:16:12)
foo :: CT rp rq -> CT rp rq (bound at Foo.hs:16:1)
In the second argument of ‘(*)’, namely ‘b'’
In the second argument of ‘CT’, namely ‘(b * b')’
The errors can be fixed using -XScopedTypeVariables
and changing foo
to:
foo :: forall rp rq . (Bar rp rq) => CT rp rq -> CT rp rq
foo = let (b' :: rq, a' :: rp) = bar
in \(CT a b) -> CT (a * a') (b * b')
Why should I need an explicit type on bar
, when the type can be inferred from its use in foo
(as it was before the GADT constraint was added)? Is that expected behavior for GADTs?
Trac metadata
Trac field | Value |
---|---|
Version | 7.8.3 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |