[GHC] #11821: Internal error: not in scope during type checking, but it passed the renamer

11 Apr 2016

      #11821: Internal error: not in scope during type checking, but it passed the
renamer
-------------------------------------+-------------------------------------
           Reporter:  darchon        |             Owner:
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:  8.0.1
          Component:  Compiler       |           Version:  8.0.1-rc3
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  GHC rejects
  Unknown/Multiple                   |  valid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 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.

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