Opened 23 months ago
Closed 10 months ago
#11821 closed bug (fixed)
Internal error: not in scope during type checking, but it passed the renamer
Reported by: | darchon | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | 8.0.2 |
Component: | Compiler | Version: | 8.0.1-rc3 |
Keywords: | TypeInType | Cc: | goldfire |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | GHC rejects valid program | Test Case: | polykinds/T11821, polykinds/T11821a |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | Phab:D2146 | |
Wiki Page: |
Description
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.
Change History (17)
comment:1 Changed 22 months ago by
Cc: | goldfire added |
---|---|
Milestone: | 8.0.1 → 8.0.2 |
comment:2 Changed 22 months ago by
Richard I wonder if you might look at this? The dreaded splitTelescopeTvs
seems to be implicated, and I really don't understand that function.
I bet it's not hard to fix.
comment:3 Changed 22 months ago by
Keywords: | TypeInType added |
---|
comment:4 Changed 22 months ago by
Harrumph. I successfully removed splitTelescopeTvs
(patch on the way), but this problem persists.
comment:5 Changed 22 months ago by
Aha. Well removing that function is a Massive Step Forward none the less. I'm looking forward to it.
comment:6 Changed 22 months ago by
Indeed. And now I've fixed this bug, made dead simple by getting splitTelescopeTvs
out of the way. You can see the fix on branch wip/no-telescope-tvs
, but there's a small validation issue still outstanding.
comment:7 Changed 22 months ago by
Differential Rev(s): | → Phab:D2146 |
---|---|
Status: | new → patch |
comment:9 Changed 22 months ago by
Status: | patch → merge |
---|---|
Test Case: | → polykinds/T11821 |
This is a vast simplification, and I think worth merging (for 8.0.2). Do let me know if you run into merge trouble!
comment:11 Changed 18 months ago by
Resolution: | → fixed |
---|---|
Status: | merge → closed |
Merged to ghc-8.0
as ced7cc010785df5968d15b24703d8f01328a82ba.
comment:12 Changed 15 months ago by
I've stumbled on this bug with a smaller example:
{-# LANGUAGE TypeInType, ConstraintKinds #-} import Data.Proxy type SameKind (a :: k1) (b :: k2) = ('Proxy :: Proxy k1) ~ ('Proxy :: Proxy k2)
And the error message with GHC 8.0 is
SameKind.hs:3:77: error: • GHC internal error: ‘k2’ is not in scope during type checking, but it passed the renamer tcl_env of environment: [arZ :-> Type variable ‘k1’ = k1, as0 :-> Type variable ‘a’ = a, as2 :-> Type variable ‘b’ = b, rq7 :-> ATcTyCon SameKind] • In the first argument of ‘Proxy’, namely ‘k2’ In the kind ‘Proxy k2’ In the second argument of ‘~’, namely ‘(Proxy :: Proxy k2)’
The bug is indeed fixed in GHC 8.0.2. I'm posting this because I believe a smaller test case would be a valuable addition to the test suite.
comment:14 Changed 15 months ago by
Test Case: | polykinds/T11821 → polykinds/T11821, polykinds/T11821a |
---|
Added test for case from comment:12
comment:15 Changed 10 months ago by
I can still trigger the same internal error in GHC 8.0.2 with the following, admittedly silly example:
{-# LANGUAGE TypeInType #-} data X :: Y where Y :: X
The error message is:
Bug.hs:2:11: error: … • GHC internal error: ‘Y’ is not in scope during type checking, but it passed the renamer tcl_env of environment: [r1cR :-> APromotionErr TyConPE] • In the kind ‘Y’
comment:16 Changed 10 months ago by
Resolution: | fixed |
---|---|
Status: | closed → new |
comment:17 Changed 10 months ago by
Resolution: | → fixed |
---|---|
Status: | new → closed |
I think this is a different bug. I will open a new ticket anyway.
It doesn't look like anything will be happening to address this for 8.0.1. Bumping.