Opened 3 months ago

Last modified 8 days ago

#13938 new bug

Iface type variable out of scope: k1

Reported by: RyanGlScott Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 8.0.1
Keywords: TypeInType, TypeApplications Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Incorrect error/warning at compile-time Test Case:
Blocked By: #14119 Blocking:
Related Tickets: #14038 Differential Rev(s):
Wiki Page:

Description

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

Change History (2)

comment:1 Changed 5 weeks ago by goldfire

Blocked By: 14119 added

This is, I'm pretty sure, #14038 again, and thus blocked by #14119.

comment:2 Changed 8 days ago by Ben Gamari <ben@…>

In 86e1db7/ghc:

Test #13938, with expect_broken

test case: dependent/should_compile/T13938
Note: See TracTickets for help on using tickets.