Opened 18 months ago

Closed 5 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 17 months ago by bgamari

Cc: goldfire added
Milestone: 8.0.18.0.2

It doesn't look like anything will be happening to address this for 8.0.1. Bumping.

comment:2 Changed 17 months ago by simonpj

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 17 months ago by simonpj

Keywords: TypeInType added

comment:4 Changed 17 months ago by goldfire

Harrumph. I successfully removed splitTelescopeTvs (patch on the way), but this problem persists.

comment:5 Changed 17 months ago by simonpj

Aha. Well removing that function is a Massive Step Forward none the less. I'm looking forward to it.

comment:6 Changed 17 months ago by goldfire

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 17 months ago by goldfire

Differential Rev(s): Phab:D2146
Status: newpatch

comment:8 Changed 17 months ago by Richard Eisenberg <eir@…>

In c5919f75/ghc:

Remove the incredibly hairy splitTelescopeTvs.

This patch removes splitTelescopeTvs by adding information about
scoped type variables to TcTyCon. Vast simplification!

This also fixes #11821 by bringing only unzonked vars into scope.

Test case: polykinds/T11821

comment:9 Changed 17 months ago by goldfire

Status: patchmerge
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:10 Changed 17 months ago by goldfire

If you do merge, also please merge comment:8:ticket:11484.

comment:11 Changed 13 months ago by bgamari

Resolution: fixed
Status: mergeclosed

comment:12 Changed 10 months ago by int-index

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:13 Changed 10 months ago by Ben Gamari <ben@…>

In 6c54fa51/ghc:

testsuite: Add another testcase for #11821

comment:14 Changed 10 months ago by bgamari

Test Case: polykinds/T11821polykinds/T11821, polykinds/T11821a

Added test for case from comment:12

comment:15 Changed 5 months ago by mietek

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 5 months ago by mietek

Resolution: fixed
Status: closednew

comment:17 Changed 5 months ago by mpickering

Resolution: fixed
Status: newclosed

I think this is a different bug. I will open a new ticket anyway.

Note: See TracTickets for help on using tickets.