Iface type variable out of scope: k1
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:
{-# 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)
{-# 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
Trac metadata
Trac field | Value |
---|---|
Version | 8.0.1 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |