#9695: GADT Constraint breaks type inference -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 Keywords: | Operating System: Architecture: Unknown/Multiple | Unknown/Multiple Difficulty: Unknown | Type of failure: GHC Blocked By: | rejects valid program Related Tickets: | Test Case: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- The following code compiles: {{{ #!haskell {-# 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: {{{ #!haskell 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? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9695 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler