GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2019-07-07T18:04:18Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/15527TypeApplications error message doesn't parenthesize infix name2019-07-07T18:04:18ZRyan ScottTypeApplications error message doesn't parenthesize infix nameIf you compile the following program:
```hs
module Bug where
f :: (Int -> Int) -> (Int -> Int) -> (Int -> Int)
f = (.) @Int
```
You'll get this error:
```
$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs,...If you compile the following program:
```hs
module Bug where
f :: (Int -> Int) -> (Int -> Int) -> (Int -> Int)
f = (.) @Int
```
You'll get this error:
```
$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:4:6: error:
Pattern syntax in expression context: .@Int
Did you mean to enable TypeApplications?
|
4 | f = (.) @Int
| ^^^^^^^^
```
I was taken aback by this strange `.@` thing before I realized what was actually going on: the error message simply forgot to parenthesize `.`. This is `ppr_expr`'s fault, since it calls `ppr` on an `RdrName` instead of `pprPrefixOcc`. Patch incoming.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.4.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"TypeApplications error message doesn't parenthesize infix name","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["TypeApplications"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"If you compile the following program:\r\n\r\n{{{#!hs\r\nmodule Bug where\r\n\r\nf :: (Int -> Int) -> (Int -> Int) -> (Int -> Int)\r\nf = (.) @Int\r\n}}}\r\n\r\nYou'll get this error:\r\n\r\n{{{\r\n$ /opt/ghc/8.4.3/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:4:6: error:\r\n Pattern syntax in expression context: .@Int\r\n Did you mean to enable TypeApplications?\r\n |\r\n4 | f = (.) @Int\r\n | ^^^^^^^^\r\n}}}\r\n\r\nI was taken aback by this strange `.@` thing before I realized what was actually going on: the error message simply forgot to parenthesize `.`. This is `ppr_expr`'s fault, since it calls `ppr` on an `RdrName` instead of `pprPrefixOcc`. Patch incoming.","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/14796Pretty Printing: GHC doesn't parenthesise (() :: Constraint)2019-07-07T18:15:32ZIcelandjackPretty Printing: GHC doesn't parenthesise (() :: Constraint)From Ryan's [How to derive Generic for (some) GADTs using QuantifiedConstraints](https://ryanglscott.github.io/2018/02/11/how-to-derive-generic-for-some-gadts/):
```hs
data ECC ctx f a where
ECC :: ctx => f a -> ECC ctx f a
```
When ...From Ryan's [How to derive Generic for (some) GADTs using QuantifiedConstraints](https://ryanglscott.github.io/2018/02/11/how-to-derive-generic-for-some-gadts/):
```hs
data ECC ctx f a where
ECC :: ctx => f a -> ECC ctx f a
```
When instantiating the `Constraint` using `-XTypeApplications` with the empty constraint, GHC doesn't add parentheses (it should look like `... -> ECC (() :: Constraint) [] ()`)
```
$ ~/code/qc-ghc/inplace/bin/ghc-stage2 --interactive -ignore-dot-ghci
GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help
Prelude> :set -XGADTs -XConstraintKinds -XTypeApplications
Prelude> data ECC ctx f a where ECC :: ctx => f a -> ECC ctx f a
Prelude> :t ECC @[] @() @()
ECC @[] @() @() :: [()] -> ECC () :: Constraint [] ()
```
Doesn't seem to happen in other cases:
```
Prelude> :t ECC @[] @() @((), ())
ECC @[] @() @((), ())
:: [()] -> ECC (() :: Constraint, () :: Constraint) [] ()
Prelude> :t ECC @[] @() @(Eq Int)
ECC @[] @() @(Eq Int) :: [()] -> ECC (Eq Int) [] ()
```8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/14038TypeApplications regression in GHC HEAD: ‘p0’ is untouchable inside the const...2019-07-07T18:18:45ZRyan ScottTypeApplications regression in GHC HEAD: ‘p0’ is untouchable inside the constraints: ()This file:
```hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeA...This file:
```hs
{-# 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:
```hs
elimList = elimListPoly @(:->) @_ @p
```
<details><summary>Trac metadata</summary>
| 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 | |
</details>
<!-- {"blocked_by":[],"summary":"TypeApplications regression in GHC HEAD: ‘p0’ is untouchable inside the constraints: ()","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.4.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.3","keywords":["TypeApplications"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This file:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE AllowAmbiguousTypes #-}\r\n{-# LANGUAGE ConstraintKinds #-}\r\n{-# LANGUAGE ExistentialQuantification #-}\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE RankNTypes #-}\r\n{-# LANGUAGE ScopedTypeVariables #-}\r\n{-# LANGUAGE TypeApplications #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# LANGUAGE TypeOperators #-}\r\nmodule Eliminator where\r\n\r\nimport Data.Kind (Type)\r\n\r\ndata family Sing (a :: k)\r\ndata instance Sing (z :: [a]) where\r\n SNil :: Sing '[]\r\n SCons :: Sing x -> Sing xs -> Sing (x:xs)\r\n\r\ndata TyFun :: Type -> Type -> Type\r\ntype a ~> b = TyFun a b -> Type\r\ninfixr 0 ~>\r\n\r\ntype family Apply (f :: k1 ~> k2) (x :: k1) :: k2\r\ntype a @@ b = Apply a b\r\ninfixl 9 @@\r\n\r\ndata FunArrow = (:->) -- ^ '(->)'\r\n | (:~>) -- ^ '(~>)'\r\n\r\nclass FunType (arr :: FunArrow) where\r\n type Fun (k1 :: Type) arr (k2 :: Type) :: Type\r\n\r\nclass FunType arr => AppType (arr :: FunArrow) where\r\n type App k1 arr k2 (f :: Fun k1 arr k2) (x :: k1) :: k2\r\n\r\ntype FunApp arr = (FunType arr, AppType arr)\r\n\r\ninstance FunType (:->) where\r\n type Fun k1 (:->) k2 = k1 -> k2\r\n\r\ninstance AppType (:->) where\r\n type App k1 (:->) k2 (f :: k1 -> k2) x = f x\r\n\r\ninstance FunType (:~>) where\r\n type Fun k1 (:~>) k2 = k1 ~> k2\r\n\r\ninstance AppType (:~>) where\r\n type App k1 (:~>) k2 (f :: k1 ~> k2) x = f @@ x\r\n\r\ninfixr 0 -?>\r\ntype (-?>) (k1 :: Type) (k2 :: Type) (arr :: FunArrow) = Fun k1 arr k2\r\n\r\nelimList :: forall (a :: Type) (p :: [a] -> Type) (l :: [a]).\r\n Sing l\r\n -> p '[]\r\n -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p xs -> p (x:xs))\r\n -> p l\r\nelimList = elimListPoly @(:->)\r\n\r\nelimListTyFun :: forall (a :: Type) (p :: [a] ~> Type) (l :: [a]).\r\n Sing l\r\n -> p @@ '[]\r\n -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p @@ xs -> p @@ (x:xs))\r\n -> p @@ l\r\nelimListTyFun = elimListPoly @(:~>) @_ @p\r\n\r\nelimListPoly :: forall (arr :: FunArrow) (a :: Type) (p :: ([a] -?> Type) arr) (l :: [a]).\r\n FunApp arr\r\n => Sing l\r\n -> App [a] arr Type p '[]\r\n -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> App [a] arr Type p xs -> App [a] arr Type p (x:xs))\r\n -> App [a] arr Type p l\r\nelimListPoly SNil pNil _ = pNil\r\nelimListPoly (SCons x (xs :: Sing xs)) pNil pCons = pCons x xs (elimListPoly @arr @a @p @xs xs pNil pCons)\r\n}}}\r\n\r\nTypechecks in GHC 8.2.1 without issue, but fails in GHC HEAD:\r\n\r\n{{{\r\n$ ghc5/inplace/bin/ghc-stage2 --interactive Bug.hs\r\nGHCi, version 8.3.20170725: http://www.haskell.org/ghc/ :? for help \r\nLoaded GHCi configuration from /home/rgscott/.ghci \r\n[1 of 1] Compiling Eliminator ( Bug.hs, interpreted ) \r\n \r\nBug.hs:59:12: error: \r\n • Couldn't match type ‘p0’ with ‘p’ \r\n because type variables ‘a1’, ‘p’ would escape their scope \r\n These (rigid, skolem) type variables are bound by \r\n the type signature for: \r\n elimList :: forall a1 (p :: [a1] -> *) (l :: [a1]). \r\n Sing l \r\n -> p '[] \r\n -> (forall (x :: a1) (xs :: [a1]). \r\n Sing x -> Sing xs -> p xs -> p (x : xs)) \r\n -> p l \r\n at Bug.hs:(54,1)-(58,15) \r\n Expected type: Sing l \r\n -> p '[] \r\n -> (forall (x :: a1) (xs :: [a1]).\r\n Sing x -> Sing xs -> p xs -> p (x : xs))\r\n -> p l\r\n Actual type: Sing l\r\n -> App [a1] (':->) * p0 '[]\r\n -> (forall (x :: a1) (xs :: [a1]).\r\n Sing x\r\n -> Sing xs\r\n -> App [a1] (':->) * p0 xs\r\n -> App [a1] (':->) * p0 (x : xs))\r\n -> App [a1] (':->) * p0 l\r\n • In the expression: elimListPoly @(:->)\r\n In an equation for ‘elimList’: elimList = elimListPoly @(:->)\r\n • Relevant bindings include\r\n elimList :: Sing l\r\n -> p '[]\r\n -> (forall (x :: a1) (xs :: [a1]).\r\n Sing x -> Sing xs -> p xs -> p (x : xs))\r\n -> p l\r\n (bound at Bug.hs:59:1)\r\n |\r\n59 | elimList = elimListPoly @(:->)\r\n | ^^^^^^^^^^^^^^^^^^^\r\n\r\nBug.hs:59:12: error:\r\n • Couldn't match type ‘p0’ with ‘p’\r\n ‘p0’ is untouchable\r\n inside the constraints: ()\r\n bound by a type expected by the context:\r\n forall (x :: a1) (xs :: [a1]).\r\n Sing x\r\n -> Sing xs\r\n -> App [a1] (':->) * p0 xs\r\n -> App [a1] (':->) * p0 (x : xs)\r\n at Bug.hs:59:12-30\r\n ‘p’ is a rigid type variable bound by\r\n the type signature for:\r\n elimList :: forall a1 (p :: [a1] -> *) (l :: [a1]).\r\n Sing l\r\n -> p '[]\r\n -> (forall (x :: a1) (xs :: [a1]).\r\n Sing x -> Sing xs -> p xs -> p (x : xs))\r\n -> p l\r\n at Bug.hs:(54,1)-(58,15)\r\n Expected type: Sing x\r\n -> Sing xs\r\n -> App [a1] (':->) * p0 xs\r\n -> App [a1] (':->) * p0 (x : xs)\r\n Actual type: Sing x -> Sing xs -> p xs -> p (x : xs)\r\n • In the expression: elimListPoly @(:->)\r\n In an equation for ‘elimList’: elimList = elimListPoly @(:->)\r\n • Relevant bindings include\r\n elimList :: Sing l\r\n -> p '[]\r\n -> (forall (x :: a1) (xs :: [a1]).\r\n Sing x -> Sing xs -> p xs -> p (x : xs))\r\n -> p l\r\n (bound at Bug.hs:59:1)\r\n |\r\n59 | elimList = elimListPoly @(:->)\r\n | ^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nA workaround is to explicitly apply `p` with `TypeApplications` in line 59:\r\n\r\n{{{#!hs\r\nelimList = elimListPoly @(:->) @_ @p\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/13938Iface type variable out of scope: k12019-07-07T18:19:20ZRyan ScottIface type variable out of scope: k1I 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 #-}
{-# L...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
```
<details><summary>Trac metadata</summary>
| 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 | |
</details>
<!-- {"blocked_by":[],"summary":"Iface type variable out of scope: k1","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["TypeApplications","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","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:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE AllowAmbiguousTypes #-}\r\n{-# LANGUAGE ConstraintKinds #-}\r\n{-# LANGUAGE ExistentialQuantification #-}\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE RankNTypes #-}\r\n{-# LANGUAGE ScopedTypeVariables #-}\r\n{-# LANGUAGE TemplateHaskell #-}\r\n{-# LANGUAGE TypeApplications #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# LANGUAGE TypeOperators #-}\r\nmodule Eliminator where\r\n\r\nimport Data.Kind (Type)\r\n\r\ndata family Sing (a :: k)\r\ndata instance Sing (z :: [a]) where\r\n SNil :: Sing '[]\r\n SCons :: Sing x -> Sing xs -> Sing (x:xs)\r\n\r\ndata TyFun :: Type -> Type -> Type\r\ntype a ~> b = TyFun a b -> Type\r\ninfixr 0 ~>\r\n\r\ntype family Apply (f :: k1 ~> k2) (x :: k1) :: k2\r\ntype a @@ b = Apply a b\r\ninfixl 9 @@\r\n\r\ndata FunArrow = (:->) -- ^ '(->)'\r\n | (:~>) -- ^ '(~>)'\r\n\r\nclass FunType (arr :: FunArrow) where\r\n type Fun (k1 :: Type) arr (k2 :: Type) :: Type\r\n\r\nclass FunType arr => AppType (arr :: FunArrow) where\r\n type App k1 arr k2 (f :: Fun k1 arr k2) (x :: k1) :: k2\r\n\r\ntype FunApp arr = (FunType arr, AppType arr)\r\n\r\ninstance FunType (:->) where\r\n type Fun k1 (:->) k2 = k1 -> k2\r\n\r\n$(return []) -- This is only necessary for GHC 8.0 -- GHC 8.2 is smarter\r\n\r\ninstance AppType (:->) where\r\n type App k1 (:->) k2 (f :: k1 -> k2) x = f x\r\n\r\ninstance FunType (:~>) where\r\n type Fun k1 (:~>) k2 = k1 ~> k2\r\n\r\n$(return [])\r\n\r\ninstance AppType (:~>) where\r\n type App k1 (:~>) k2 (f :: k1 ~> k2) x = f @@ x\r\n\r\ninfixr 0 -?>\r\ntype (-?>) (k1 :: Type) (k2 :: Type) (arr :: FunArrow) = Fun k1 arr k2\r\n\r\nelimList :: forall (a :: Type) (p :: [a] -> Type) (l :: [a]).\r\n Sing l\r\n -> p '[]\r\n -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p xs -> p (x:xs))\r\n -> p l\r\nelimList = elimListPoly @(:->)\r\n\r\nelimListTyFun :: forall (a :: Type) (p :: [a] ~> Type) (l :: [a]).\r\n Sing l\r\n -> p @@ '[]\r\n -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p @@ xs -> p @@ (x:xs))\r\n -> p @@ l\r\nelimListTyFun = elimListPoly @(:~>) @_ @p\r\n\r\nelimListPoly :: forall (arr :: FunArrow) (a :: Type) (p :: ([a] -?> Type) arr) (l :: [a]).\r\n FunApp arr\r\n => Sing l\r\n -> App [a] arr Type p '[]\r\n -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> App [a] arr Type p xs -> App [a] arr Type p (x:xs))\r\n -> App [a] arr Type p l\r\nelimListPoly SNil pNil _ = pNil\r\nelimListPoly (SCons x (xs :: Sing xs)) pNil pCons = pCons x xs (elimListPoly @arr @a @p @xs xs pNil pCons)\r\n}}}\r\n{{{#!hs\r\n{-# LANGUAGE AllowAmbiguousTypes #-}\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE RankNTypes #-}\r\n{-# LANGUAGE ScopedTypeVariables #-}\r\n{-# LANGUAGE TypeApplications #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# LANGUAGE TypeOperators #-}\r\n{-# LANGUAGE UndecidableInstances #-}\r\nmodule ListSpec where\r\n\r\nimport Eliminator\r\nimport Data.Kind\r\nimport Data.Type.Equality\r\nimport GHC.TypeLits\r\n\r\ntype family Length (l :: [a]) :: Nat where {}\r\ntype family Map (f :: a ~> b) (l :: [a]) :: [b] where {}\r\n\r\ntype WhyMapPreservesLength (f :: x ~> y) (l :: [x])\r\n = Length l :~: Length (Map f l)\r\ndata WhyMapPreservesLengthSym1 (f :: x ~> y) :: [x] ~> Type\r\ntype instance Apply (WhyMapPreservesLengthSym1 f) l = WhyMapPreservesLength f l\r\n\r\nmapPreservesLength :: forall (x :: Type) (y :: Type) (f :: x ~> y) (l :: [x]).\r\n Length l :~: Length (Map f l)\r\nmapPreservesLength\r\n = elimListTyFun @x @(WhyMapPreservesLengthSym1 f) @l undefined undefined undefined\r\n}}}\r\n\r\nYou'll need to compile the files like this:\r\n\r\n{{{\r\n$ /opt/ghc/8.0.2/bin/ghc -fforce-recomp -O2 -c Eliminator.hs \r\n$ /opt/ghc/8.0.2/bin/ghc -fforce-recomp -O2 -c ListSpec.hs \r\n./Eliminator.hi\r\nDeclaration for elimListTyFun\r\nUnfolding of elimListTyFun:\r\n Iface type variable out of scope: k2\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1