[GHC] #15472: GHC HEAD type inference regression post-"Remove decideKindGeneralisationPlan"

3 Aug 2018

      #15472: GHC HEAD type inference regression post-"Remove
decideKindGeneralisationPlan"
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  highest        |         Milestone:  8.8.1
          Component:  Compiler       |           Version:  8.5
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Commit c955a514f033a12f6d0ab0fbacec3e18a5757ab5 (`Remove
 decideKindGeneralisationPlan`) causes the `singletons` library to no
 longer compile. Here is as minimal of an example as I can muster:

 {{{#!hs
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UndecidableInstances #-}
 module Bug (sPermutations) where

 import Data.Kind

 data TyFun :: Type -> Type -> Type
 type a ~> b = TyFun a b -> Type
 infixr 0 ~>
 type family Apply (f :: k1 ~> k2) (x :: k1) :: k2

 data family Sing :: forall k. k -> Type
 data instance Sing :: forall a. [a] -> Type where
   SNil  :: Sing '[]
   SCons :: Sing x -> Sing xs -> Sing (x:xs)

 newtype instance Sing (f :: k1 ~> k2) =
   SLambda { applySing :: forall t. Sing t -> Sing (Apply f t) }

 type SingFunction1 f = forall t. Sing t -> Sing (Apply f t)
 singFun1 :: forall f. SingFunction1 f -> Sing f
 singFun1 f = SLambda f

 type SingFunction2 f = forall t. Sing t -> SingFunction1 (Apply f t)
 singFun2 :: forall f. SingFunction2 f -> Sing f
 singFun2 f = SLambda (\x -> singFun1 (f x))

 type family Undefined :: k where {}

 sUndefined :: a
 sUndefined = undefined

 type family LetGo k z x ys where
   LetGo k z x '[] = z
   LetGo k z x (y ': ys) = Apply (Apply k y) (LetGo k z x ys)

 type family Foldr (k :: a ~> b ~> b) (x :: b) (xs :: [a]) :: b where
   Foldr k z x = LetGo k z x x

 sFoldr :: forall (t1 :: a ~> b ~> b) (t2 :: b) (t3 :: [a]).
           Sing t1 -> Sing t2 -> Sing t3
        -> Sing (Foldr t1 t2 t3 :: b)
 sFoldr (sK :: Sing k) (sZ :: Sing z) (sX :: Sing x)
   = let sGo :: forall arg. Sing arg -> Sing (LetGo k z x arg)
         sGo SNil = sZ
         sGo (SCons (sY :: Sing y) (sYs :: Sing ys))
           = sK `applySing` sY `applySing` sGo sYs
     in sGo sX

 type family LetInterleave xs0 t ts is (a1 :: [a]) (a2 :: [[a]]) :: [[a]]
 where
   LetInterleave xs0 t ts is a1 a2 = Undefined a1 a2
 data LetInterleaveSym5 l_ahko l_ahkp l_ahkq l_ahkr (l_ahks :: [a]) ::
 [[a]] ~> [[a]]
 type instance Apply (LetInterleaveSym5 l_ahko l_ahkp l_ahkq l_ahkr l_ahks)
 l_ahkn = LetInterleave l_ahko l_ahkp l_ahkq l_ahkr l_ahks l_ahkn
 data LetInterleaveSym4 l_ahkv l_ahkw l_ahkx l_ahky :: forall a. [a] ~>
 [[a]] ~> [[a]]
 type instance Apply (LetInterleaveSym4 l_ahkv l_ahkw l_ahkx l_ahky) l_ahku
 = LetInterleaveSym5 l_ahkv l_ahkw l_ahkx l_ahky l_ahku
 data LetInterleaveSym3 l_ahkB l_ahkC l_ahkD l_ahkA
 type instance Apply (LetInterleaveSym3 l_ahkB l_ahkC l_ahkD) l_ahkA =
 LetInterleaveSym4 l_ahkB l_ahkC l_ahkD l_ahkA
 data LetInterleaveSym2 l_ahkG l_ahkH l_ahkF
 type instance Apply (LetInterleaveSym2 l_ahkG l_ahkH) l_ahkF =
 LetInterleaveSym3 l_ahkG l_ahkH l_ahkF
 data LetInterleaveSym1 l_ahkK l_ahkJ
 type instance Apply (LetInterleaveSym1 l_ahkK) l_ahkJ = LetInterleaveSym2
 l_ahkK l_ahkJ
 data LetInterleaveSym0 l_ahkM
 type instance Apply LetInterleaveSym0 l_ahkM = LetInterleaveSym1 l_ahkM

 type family LetPerms xs0 a1 a2 where
   LetPerms xs0 '[] _ = '[]
   LetPerms xs0 (t ': ts) is =
     Foldr (LetInterleaveSym4 xs0 t ts is) (LetPerms xs0 ts (t ': is))
 (Permutations is)

 {-
 $(singletons [d|
   permutations            :: forall a. [a] -> [[a]]
   permutations xs0        =  xs0 : perms xs0 []
     where
       perms []     _  = []
       perms (t:ts) is = foldr interleave (perms ts (t:is)) (permutations
 is)
         where
               interleave :: [a] -> [[a]] -> [[a]]
               interleave = undefined
   |])
 -}

 type family Permutations (xs0 :: [a]) :: [[a]] where
   Permutations xs0 = xs0 ': LetPerms xs0 xs0 '[]

 sPermutations :: forall (t1 :: [a]).
                  Sing t1 -> Sing (Permutations t1 :: [[a]])
 sPermutations (sXs0 :: Sing xs0)
   = let sPerms :: forall arg1 arg2.
                   Sing arg1 -> Sing arg2
                -> Sing (LetPerms xs0 arg1 arg2)
         sPerms SNil _ = SNil
         sPerms (SCons (sT :: Sing t) (sTs :: Sing ts)) (sIs :: Sing is)
           = let sInterleave :: forall (t2 :: [a]) (t3 :: [[a]]).
                                Sing t2 -> Sing t3
                             -> Sing (LetInterleave xs0 t ts is t2 t3 ::
 [[a]])
                 sInterleave (sA1 :: Sing a1) (sA2 :: Sing a2)
                   = sUndefined sA1 sA2
             in sFoldr (singFun2 @(LetInterleaveSym4 xs0 t ts is)
 sInterleave)
                       (sPerms sTs (sT `SCons` sIs))
                       (sPermutations sIs)
     in sXs0 `SCons` sPerms sXs0 SNil
 }}}

 After that commit, this program (which previously typechecked) now errors
 with:

 {{{
 $ ~/Software/ghc4/inplace/bin/ghc-stage2 Bug.hs
 [1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

 Bug.hs:105:66: error:
     • Could not deduce: t2 ~~ t30
       from the context: arg1 ~ (x : xs)
         bound by a pattern with constructor:
                    SCons :: forall a (x :: a) (xs :: [a]).
                             Sing x -> Sing xs -> Sing (x : xs),
                  in an equation for ‘sPerms’
         at Bug.hs:99:17-53
       ‘t2’ is a rigid type variable bound by
         a type expected by the context:
           SingFunction2 (LetInterleaveSym4 t1 x xs arg2)
         at Bug.hs:105:24-76
       Expected type: Sing t
                      -> Sing t2
                      -> Sing (Apply (Apply (LetInterleaveSym4 t1 x xs
 arg2) t) t2)
         Actual type: Sing t20
                      -> Sing t30 -> Sing (LetInterleave t1 x xs arg2 t20
 t30)
     • In the second argument of ‘singFun2’, namely ‘sInterleave’
       In the first argument of ‘sFoldr’, namely
         ‘(singFun2 @(LetInterleaveSym4 xs0 t ts is) sInterleave)’
       In the expression:
         sFoldr
           (singFun2 @(LetInterleaveSym4 xs0 t ts is) sInterleave)
           (sPerms sTs (sT `SCons` sIs))
           (sPermutations sIs)
     • Relevant bindings include
         sInterleave :: forall (t2 :: [a1]) (t3 :: [[a1]]).
                        Sing t2 -> Sing t3 -> Sing (LetInterleave t1 x xs
 arg2 t2 t3)
           (bound at Bug.hs:103:17)
         sIs :: Sing arg2 (bound at Bug.hs:99:57)
         sTs :: Sing xs (bound at Bug.hs:99:39)
         sT :: Sing x (bound at Bug.hs:99:24)
         sPerms :: Sing arg1 -> Sing arg2 -> Sing (LetPerms t1 arg1 arg2)
           (bound at Bug.hs:98:9)
         sXs0 :: Sing t1 (bound at Bug.hs:94:16)
         (Some bindings suppressed; use -fmax-relevant-binds=N or -fno-max-
 relevant-binds)
     |
 105 |             in sFoldr (singFun2 @(LetInterleaveSym4 xs0 t ts is)
 sInterleave)
     |
 ^^^^^^^^^^^
 }}}

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