Re: [GHC] #9667: Type inference is weaker for GADT than analogous Data Family

2 Nov 2014

      #9667: Type inference is weaker for GADT than analogous Data Family
-------------------------------------+-------------------------------------
              Reporter:  carter      |            Owner:
                  Type:  feature     |           Status:  new
  request                            |        Milestone:
              Priority:  normal      |          Version:  7.8.3
             Component:  Compiler    |         Keywords:
  (Type checker)                     |     Architecture:  Unknown/Multiple
            Resolution:              |       Difficulty:  Unknown
      Operating System:              |       Blocked By:
  Unknown/Multiple                   |  Related Tickets:
       Type of failure:  GHC         |
  rejects valid program              |
             Test Case:              |
              Blocking:              |
Differential Revisions:              |
-------------------------------------+-------------------------------------

Comment (by goldfire):

 Adding the following definitions made this more perspicuous to me:

 {{{
 fromList1DF :: (List l a, List l b) => [(a,b)] -> DFProd l (Pair Unit
 Unit) (a, b)
 fromList1DF [] = DFPair (DFLeaf nil) (DFLeaf nil)
 fromList1DF ((a,b):xs) = case fromList1DF xs of
     DFPair (DFLeaf as) (DFLeaf bs) ->
       DFPair (DFLeaf (a `cons` as)) (DFLeaf (b `cons` bs))

 fromList1GA :: (List l a, List l b) => [(a,b)] -> GAProd l (Pair Unit
 Unit) (a, b)
 fromList1GA [] = GAPair (GALeaf nil) (GALeaf nil)
 fromList1GA ((a,b):xs) = case fromList1GA xs of
     GAPair (GALeaf as) (GALeaf bs) ->
       GAPair (GALeaf (a `cons` as)) (GALeaf (b `cons` bs))
     -- GAPair (GAPair _ _) _ -> undefined
     -- GAPair (GALeaf _) (GAPair _ _) -> undefined
     _ -> error "GADT warnings bad"
 }}}

 (Note that the one pattern in `fromList1GA` is actually complete, but
 #3927 bites unless we have the catchall case. The commented-out lines were
 my tests to make sure that other patterns were indeed inaccessible.)

 `fromList1DF` compiles just fine. `fromList1GA` fails with two errors, the
 second being

 {{{
 /Users/rae/temp/bug/SimplerGadtVsData.hs:104:32:
     Couldn't match type ‘l0’ with ‘l’
       ‘l0’ is untouchable
         inside the constraints ('Pair 'Unit 'Unit ~ 'Pair pra prb,
                                 (a, b) ~ (a1, b1))
         bound by a pattern with constructor
                    GAPair :: forall (v :: * -> *) (pra :: Prod) a (prb ::
 Prod) b.
                              GAProd v pra a
                              -> GAProd v prb b -> GAProd v ('Pair pra prb)
 (a, b),
                  in a case alternative
         at /Users/rae/temp/bug/SimplerGadtVsData.hs:103:5-34
       ‘l’ is a rigid type variable bound by
           the type signature for
             fromList1GA :: (List l a, List l b) =>
                            [(a, b)] -> GAProd l ('Pair 'Unit 'Unit) (a, b)
           at /Users/rae/temp/bug/SimplerGadtVsData.hs:100:16
     Expected type: l a
       Actual type: l0 a1
     Relevant bindings include
       bs :: l0 b1
         (bound at /Users/rae/temp/bug/SimplerGadtVsData.hs:103:32)
       as :: l0 a1
         (bound at /Users/rae/temp/bug/SimplerGadtVsData.hs:103:20)
       fromList1GA :: [(a, b)] -> GAProd l ('Pair 'Unit 'Unit) (a, b)
         (bound at /Users/rae/temp/bug/SimplerGadtVsData.hs:101:1)
     In the second argument of ‘cons’, namely ‘as’
     In the first argument of ‘GALeaf’, namely ‘(a `cons` as)’
 }}}

 (The first is a failure about class constraints. This failure is a direct
 consequence of the error listed above. Indeed, I would say that the first
 error -- which complains about ambiguity of `l0` -- should be suppressed
 when we also report that `l0` is untouchable.)

 The problem is that GHC can't infer the result type of the GADT pattern
 match. Perhaps this result type somehow depends on the information we
 learn about `pra` and `prb` in the match, and there's no way to infer this
 dependency. So, GHC gives up -- this is the essence of "untouchable"
 variables.

 I think there ''is'' room for improvement here, because the GADT pattern
 match wasn't actually informative, in this case: all the information that
 comes out of the match is known beforehand, via the details of the type
 signature. It is perhaps conceivable to detect this corner case and not
 make the "global" tyvars become untouchable. I don't know if this is worth
 pursuing very deeply, but I think that's what's going on.

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9667#comment:14
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler