TypeApplications regression in GHC HEAD: ‘p0’ is untouchable inside the constraints: ()
This file:
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# 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
instance AppType (:->) where
type App k1 (:->) k2 (f :: k1 -> k2) x = f x
instance FunType (:~>) where
type Fun k1 (:~>) k2 = k1 ~> k2
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)
Typechecks in GHC 8.2.1 without issue, but fails in GHC HEAD:
$ ghc5/inplace/bin/ghc-stage2 --interactive Bug.hs
GHCi, version 8.3.20170725: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Eliminator ( Bug.hs, interpreted )
Bug.hs:59:12: error:
• Couldn't match type ‘p0’ with ‘p’
because type variables ‘a1’, ‘p’ would escape their scope
These (rigid, skolem) type variables are bound by
the type signature for:
elimList :: forall a1 (p :: [a1] -> *) (l :: [a1]).
Sing l
-> p '[]
-> (forall (x :: a1) (xs :: [a1]).
Sing x -> Sing xs -> p xs -> p (x : xs))
-> p l
at Bug.hs:(54,1)-(58,15)
Expected type: Sing l
-> p '[]
-> (forall (x :: a1) (xs :: [a1]).
Sing x -> Sing xs -> p xs -> p (x : xs))
-> p l
Actual type: Sing l
-> App [a1] (':->) * p0 '[]
-> (forall (x :: a1) (xs :: [a1]).
Sing x
-> Sing xs
-> App [a1] (':->) * p0 xs
-> App [a1] (':->) * p0 (x : xs))
-> App [a1] (':->) * p0 l
• In the expression: elimListPoly @(:->)
In an equation for ‘elimList’: elimList = elimListPoly @(:->)
• Relevant bindings include
elimList :: Sing l
-> p '[]
-> (forall (x :: a1) (xs :: [a1]).
Sing x -> Sing xs -> p xs -> p (x : xs))
-> p l
(bound at Bug.hs:59:1)
|
59 | elimList = elimListPoly @(:->)
| ^^^^^^^^^^^^^^^^^^^
Bug.hs:59:12: error:
• Couldn't match type ‘p0’ with ‘p’
‘p0’ is untouchable
inside the constraints: ()
bound by a type expected by the context:
forall (x :: a1) (xs :: [a1]).
Sing x
-> Sing xs
-> App [a1] (':->) * p0 xs
-> App [a1] (':->) * p0 (x : xs)
at Bug.hs:59:12-30
‘p’ is a rigid type variable bound by
the type signature for:
elimList :: forall a1 (p :: [a1] -> *) (l :: [a1]).
Sing l
-> p '[]
-> (forall (x :: a1) (xs :: [a1]).
Sing x -> Sing xs -> p xs -> p (x : xs))
-> p l
at Bug.hs:(54,1)-(58,15)
Expected type: Sing x
-> Sing xs
-> App [a1] (':->) * p0 xs
-> App [a1] (':->) * p0 (x : xs)
Actual type: Sing x -> Sing xs -> p xs -> p (x : xs)
• In the expression: elimListPoly @(:->)
In an equation for ‘elimList’: elimList = elimListPoly @(:->)
• Relevant bindings include
elimList :: Sing l
-> p '[]
-> (forall (x :: a1) (xs :: [a1]).
Sing x -> Sing xs -> p xs -> p (x : xs))
-> p l
(bound at Bug.hs:59:1)
|
59 | elimList = elimListPoly @(:->)
| ^^^^^^^^^^^^^^^^^^^
A workaround is to explicitly apply p
with TypeApplications
in line 59:
elimList = elimListPoly @(:->) @_ @p
Trac metadata
Trac field | Value |
---|---|
Version | 8.3 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | high |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |