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 |