[GHC] #13938: Iface type variable out of scope: k1

[GHC]

#13938: Iface type variable out of scope:  k1
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.0.1
  (Type checker)                     |
           Keywords:  TypeInType,    |  Operating System:  Unknown/Multiple
  TypeApplications                   |
       Architecture:                 |   Type of failure:  Incorrect
  Unknown/Multiple                   |  error/warning at compile-time
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 I managed to make GHC spit out an unusual warning when doing some
 dependent Haskell recently. This issue is reproducible on GHC 8.0.1,
 8.0.2, 8.2.1, and HEAD. You'll need these two files:

 {{{#!hs
 {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE TypeOperators #-}
 module Eliminator where

 import Data.Kind (Type)

 data family Sing (a :: k)
 data instance Sing (z :: [a]) where
   SNil  :: Sing '[]
   SCons :: Sing x -> Sing xs -> Sing (x:xs)

 data TyFun :: Type -> Type -> Type
 type a ~> b = TyFun a b -> Type
 infixr 0 ~>

 type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
 type a @@ b = Apply a b
 infixl 9 @@

 data FunArrow = (:->) -- ^ '(->)'
               | (:~>) -- ^ '(~>)'

 class FunType (arr :: FunArrow) where
   type Fun (k1 :: Type) arr (k2 :: Type) :: Type

 class FunType arr => AppType (arr :: FunArrow) where
   type App k1 arr k2 (f :: Fun k1 arr k2) (x :: k1) :: k2

 type FunApp arr = (FunType arr, AppType arr)

 instance FunType (:->) where
   type Fun k1 (:->) k2 = k1 -> k2

 $(return []) -- This is only necessary for GHC 8.0 -- GHC 8.2 is smarter

 instance AppType (:->) where
   type App k1 (:->) k2 (f :: k1 -> k2) x = f x

 instance FunType (:~>) where
   type Fun k1 (:~>) k2 = k1 ~> k2

 $(return [])

 instance AppType (:~>) where
   type App k1 (:~>) k2 (f :: k1 ~> k2) x = f @@ x

 infixr 0 -?>
 type (-?>) (k1 :: Type) (k2 :: Type) (arr :: FunArrow) = Fun k1 arr k2

 elimList :: forall (a :: Type) (p :: [a] -> Type) (l :: [a]).
             Sing l
          -> p '[]
          -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p xs -> p
 (x:xs))
          -> p l
 elimList = elimListPoly @(:->)

 elimListTyFun :: forall (a :: Type) (p :: [a] ~> Type) (l :: [a]).
                  Sing l
               -> p @@ '[]
               -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p @@
 xs -> p @@ (x:xs))
               -> p @@ l
 elimListTyFun = elimListPoly @(:~>) @_ @p

 elimListPoly :: forall (arr :: FunArrow) (a :: Type) (p :: ([a] -?> Type)
 arr) (l :: [a]).
                 FunApp arr
              => Sing l
              -> App [a] arr Type p '[]
              -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> App [a]
 arr Type p xs -> App [a] arr Type p (x:xs))
              -> App [a] arr Type p l
 elimListPoly SNil                      pNil _     = pNil
 elimListPoly (SCons x (xs :: Sing xs)) pNil pCons = pCons x xs
 (elimListPoly @arr @a @p @xs xs pNil pCons)
 }}}
 {{{#!hs
 {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UndecidableInstances #-}
 module ListSpec where

 import Eliminator
 import Data.Kind
 import Data.Type.Equality
 import GHC.TypeLits

 type family Length (l :: [a]) :: Nat where {}
 type family Map (f :: a ~> b) (l :: [a]) :: [b] where {}

 type WhyMapPreservesLength (f :: x ~> y) (l :: [x])
   = Length l :~: Length (Map f l)
 data WhyMapPreservesLengthSym1 (f :: x ~> y) :: [x] ~> Type
 type instance Apply (WhyMapPreservesLengthSym1 f) l =
 WhyMapPreservesLength f l

 mapPreservesLength :: forall (x :: Type) (y :: Type) (f :: x ~> y) (l ::
 [x]).
                       Length l :~: Length (Map f l)
 mapPreservesLength
   = elimListTyFun @x @(WhyMapPreservesLengthSym1 f) @l undefined undefined
 undefined
 }}}

 You'll need to compile the files like this:

 {{{
 $ /opt/ghc/8.0.2/bin/ghc -fforce-recomp -O2 -c Eliminator.hs
 $ /opt/ghc/8.0.2/bin/ghc -fforce-recomp -O2 -c ListSpec.hs
 ./Eliminator.hi
 Declaration for elimListTyFun
 Unfolding of elimListTyFun:
   Iface type variable out of scope:  k2
 }}}

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