[GHC] #9695: GADT Constraint breaks type inference

16 Oct 2014

      #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