[GHC] #9733: Strange errors when using type families as parameters

[GHC]

#9733: Strange errors when using type families as parameters
-------------------------------------+-------------------------------------
       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:
-------------------------------------+-------------------------------------
 I seem to have found a dark corner of GHC. In the process of finding a
 minimal example, I found a few different ways to trigger a bug. I'm
 assuming they are all related.

 == Example 1 ==
 I started  off with a GADT parameterized by a type list:

 {{{#!haskell
 {-# LANGUAGE TypeFamilies, GADTs, DataKinds, TypeOperators #-}

 module Foo where

 type TList = '[Float, Double]

 type family PrevElt (xs :: [*]) (a :: *) :: * where
   PrevElt (b ': a ': xs) a = b
   PrevElt (b ': c ': xs) a = PrevElt (c ': xs) a

 data FooList :: ([*] -> * -> *) where
   Bar :: FooList prevrp ((PrevElt prevrp rp) -> rp)

 test1 :: FooList TList ((PrevElt TList rp) -> rp)
 test1 = Bar
 }}}
 which compiles as expected.

 If I make a syntactic change and parameterize the GADT with the type
 family rather than the type list:

 {{{#!hs
 {-# LANGUAGE TypeFamilies, GADTs, DataKinds, TypeOperators #-}

 module Foo where

 type TList = '[Float, Double]

 type family PrevElt (xs :: [*]) (a :: *) :: * where
   PrevElt (b ': a ': xs) a = b
   PrevElt (b ': c ': xs) a = PrevElt (c ': xs) a

 data FooTF :: ((* -> *) -> * -> *) where
   Bar :: FooTF prevrp ((prevrp rp) -> rp)

 test2 :: FooTF (PrevElt TList) ((PrevElt TList rp) -> rp)
 test2 = Bar
 }}}
 I get a non-sensical error:
 {{{
 Foo.hs:15:9:
     Couldn't match type `PrevElt TList rp' with `PrevElt TList rp'
     NB: `PrevElt' is a type function, and may not be injective
     Expected type: FooTF (PrevElt TList) (PrevElt TList rp -> rp)
       Actual type: FooTF (PrevElt TList) (PrevElt TList rp -> rp)
     Relevant bindings include
       test2 :: FooTF (PrevElt TList) (PrevElt TList rp -> rp)
         (bound at testsuite\Foo.hs:15:1)
     In the expression: Bar
     In an equation for `test2': test2 = Bar
 }}}
 As far as I know, this should compile.

 == Example 2 ==
 Another simple example uses [https://hackage.haskell.org/package/syntactic
 syntactic], along with the type-family-parameterized GADT:
 {{{#!hs
 {-# LANGUAGE TypeFamilies, GADTs, DataKinds, TypeOperators #-}

 module Foo where

 import Data.Syntactic

 type family PrevElt (xs :: [*]) (a :: *) :: * where
   PrevElt (b ': a ': xs) a = b
   PrevElt (b ': c ': xs) a = PrevElt (c ': xs) a

 data FooTF :: ((* -> *) -> * -> *) where
   Const :: FooTF prevrp (Full rp)
   Bar :: FooTF prevrp ((prevrp rp) :-> Full rp)

 type T1 = Double
 type T2 = Float
 type Dom = FooTF (PrevElt '[T1, T2])

 leaf = inj (Const :: Dom (Full T1)) :: ASTF Dom T1
 t1 = inj (Bar :: Dom (T1 :-> Full T2)) :$ leaf :: ASTF Dom T2
 }}}

 By only changing the types `T1` and `T2`:
 {{{#!hs
 {-# LANGUAGE TypeFamilies, GADTs, DataKinds, TypeOperators #-}

 module Foo where

 import Data.Syntactic

 type family PrevElt (xs :: [*]) (a :: *) :: * where
   PrevElt (b ': a ': xs) a = b
   PrevElt (b ': c ': xs) a = PrevElt (c ': xs) a

 data FooTF :: ((* -> *) -> * -> *) where
   Const :: FooTF prevrp (Full rp)
   Bar :: FooTF prevrp ((prevrp rp) :-> Full rp)

 data T
 type T1 = T Double
 type T2 = T Float
 type Dom = FooTF (PrevElt '[T1, T2])

 leaf = inj (Const :: Dom (Full T1)) :: ASTF Dom T1
 t1 = inj (Bar :: Dom (T1 :-> Full T2)) :$ leaf :: ASTF Dom T2
 }}}

 GHC complains:

 {{{
 Foo.hs:21:11:
     Couldn't match type ‘Double’ with ‘T Float’
     Expected type: Dom (T1 :-> Full T2)
       Actual type: FooTF T (T Double :-> Full Double)
     In the first argument of ‘inj’, namely
       ‘(Bar :: Dom (T1 :-> Full T2))’
     In the first argument of ‘(:$)’, namely
       ‘inj (Bar :: Dom (T1 :-> Full T2))’
 Failed, modules loaded: none.
 }}}

 == Example 3 ==
 I've also attached a larger example (also using
 [https://hackage.haskell.org/package/syntactic syntactic]) that has [more,
 different] errors, which I believe to be related to this problem. Errors
 for the attached file are:

 {{{
 Foo.hs:32:6:
     Couldn't match type `NextElt TList (PrevElt ((':) * (T' Float) ('[]
 *)) Double)'
                   with `Double'
     Expected type: Double
       Actual type: NextElt TList (PrevElt TList Double)
     In the first argument of `(:$)', namely `inj' Bar'
     In the expression: inj' Bar :$ leaf
     In an equation for `t1': t1 = inj' Bar :$ leaf

 Foo.hs:32:11:
     Couldn't match type `PrevElt TList' with T'
     Expected type: Dom (Foo (T' Double) T1 :-> Full (Foo Double T1))
       Actual type: FooTF
                      T' (Foo (T' Double) T1 :-> Full (Foo Double T1))
     In the first argument of inj', namely `Bar'
     In the first argument of `(:$)', namely `inj' Bar'
 }}}

 In the first error, the `Actual type: NextElt TList (PrevElt TList
 Double)` is strange because `Double` only occurs as a parameter to `T'`,
 and never as a naked type that could be applied to type family.

 In the second error, GHC seems to be confusing two types of kind `(* ->
 *)`: `T'` and `PrevElt TList`.

 Changing the GADT from type-family-indexed to type-list-index (like in the
 first example) makes the attached code compile. I minimized the attached
 example as much as possible: any changes I made to simplify the code
 resulted in different errors, which may also be helpful for finding this
 bug.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9733>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler