Internal error: not in scope during type checking, but it passed the renamer

While trying to get the singletons package to compile on GHC8 (https://github.com/goldfirere/singletons/pull/142), I encountered the following error while trying to track down a bug:

[1 of 1] Compiling NotInScope       ( NotInScope.hs, interpreted )

NotInScope.hs:22:20: error:
    • GHC internal error: ‘b’ is not in scope during type checking, but it passed the renamer
      tcl_env of environment: [a1lm :-> Type variable ‘b’ = b,
                               a1lA :-> Type variable ‘l1’ = l1, a1lB :-> Type variable ‘l2’ = l2,
                               a1lC :-> Type variable ‘l3’ = l3, a1lE :-> Type variable ‘a’ = a,
                               a1lF :-> Type variable ‘l4’ = l4, r1aq :-> ATcTyCon Lgo,
                               r1aG :-> ATcTyCon Lgo1, r1aI :-> ATcTyCon Lgo2]
    • In the kind ‘b’
      In the definition of data constructor ‘Lgo1KindInference’
      In the data declaration for ‘Lgo1’

for the following code:

{-# LANGUAGE RankNTypes, DataKinds, PolyKinds, GADTs, TypeFamilies, UndecidableInstances #-}
module NotInScope where

import Data.Proxy

type KindOf (a :: k) = ('KProxy :: KProxy k)
data TyFun :: * -> * -> *
type family Apply (f :: TyFun k1 k2 -> *) (x :: k1) :: k2

data Lgo2 l1
          l2
          l3
          (l4 :: b)
          (l5 :: TyFun [a] b)
  = forall (arg :: [a]) . KindOf (Apply (Lgo2 l1 l2 l3 l4) arg) ~ KindOf (Lgo l1 l2 l3 l4 arg) =>
    Lgo2KindInference

data Lgo1 l1
          l2
          l3
          (l4 :: TyFun b (TyFun [a] b -> *))
  = forall (arg :: b) . KindOf (Apply (Lgo1 l1 l2 l3) arg) ~ KindOf (Lgo2 l1 l2 l3 arg) =>
    Lgo1KindInference

type family Lgo f
                z0
                xs0
                (a1 :: b)
                (a2 :: [a]) :: b where
  Lgo f z0 xs0 z '[]         = z
  Lgo f z0 xs0 z ('(:) x xs) = Apply (Apply (Lgo1 f z0 xs0) (Apply (Apply f z) x)) xs

Note that the above code works fine in GHC 7.10.2.

There are two options to make the code compile on GHC8-rc3:

• Remove the kind annotations on the forall arg . binders
• Or make the following changes using TypeInType:

{-# LANGUAGE RankNTypes, DataKinds, PolyKinds, GADTs, TypeFamilies, UndecidableInstances, TypeInType #-}
module NotInScope where

import Data.Proxy
import GHC.Types

type KindOf (a :: k) = ('KProxy :: KProxy k)
data TyFun :: * -> * -> *
type family Apply (f :: TyFun k1 k2 -> *) (x :: k1) :: k2

data Lgo2 a
          b
          l1
          l2
          l3
          (l4 :: b)
          (l5 :: TyFun [a] b)
  = forall (arg :: [a]) . KindOf (Apply (Lgo2 a b l1 l2 l3 l4) arg) ~ KindOf (Lgo a b l1 l2 l3 l4 arg) =>
    Lgo2KindInference

data Lgo1 a
          b
          l1
          l2
          l3
          (l4 :: TyFun b (TyFun [a] b -> *))
  = forall (arg :: b) . KindOf (Apply (Lgo1 a b l1 l2 l3) arg) ~ KindOf (Lgo2 a b l1 l2 l3 arg) =>
    Lgo1KindInference

type family Lgo a
                b
                f
                z0
                xs0
                (a1 :: b)
                (a2 :: [a]) :: b where
  Lgo a b f z0 xs0 z '[]         = z
  Lgo a b f z0 xs0 z ('(:) x xs) = Apply (Apply (Lgo1 a b f z0 xs0) (Apply (Apply f z) x)) xs

I'm sorry I didn't create a smaller test case. Let me know if one is required and I'll try. The error seems to be related to the recursive aspect of the three definitions and how implicit kind variables are handled in ghc8.

Trac metadata

Trac field	Value
Version	8.0.1-rc3
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture