GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2019-07-07T18:19:41Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/13879Strange interaction between higher-rank kinds and type synonyms2019-07-07T18:19:41ZRyan ScottStrange interaction between higher-rank kinds and type synonymsHere's some code with typechecks with GHC 8.0.1, 8.0.2, 8.2.1, and HEAD:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAG...Here's some code with typechecks with GHC 8.0.1, 8.0.2, 8.2.1, and HEAD:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Kind
data family Sing (a :: k)
data (a :: j) :~~: (b :: k) where
HRefl :: a :~~: a
data instance Sing (z :: a :~~: b) where
SHRefl :: Sing HRefl
(%:~~:->) :: forall (j :: Type) (k :: Type) (a :: j) (b :: k) (r :: a :~~: b) (p :: forall (z :: Type) (y :: z). a :~~: y -> Type).
Sing r
-> p HRefl
-> p r
(%:~~:->) SHRefl pHRefl = pHRefl
type App f x = f x
type HRApp (f :: forall (z :: Type) (y :: z). a :~~: y -> Type) (x :: a :~~: b) = f x
```
Now I want to refactor this so that I use `App`:
```hs
(%:~~:->) :: forall (j :: Type) (k :: Type) (a :: j) (b :: k) (r :: a :~~: b) (p :: forall (z :: Type) (y :: z). a :~~: y -> Type).
Sing r
-> App p HRefl
-> App p r
```
However, GHC doesn't like that:
```
$ /opt/ghc/8.2.1/bin/ghci Bug.hs -fprint-explicit-kinds -fprint-explicit-foralls
GHCi, version 8.2.0.20170623: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:21:20: error:
• Expected kind ‘(:~~:) j z a a’,
but ‘'HRefl j a’ has kind ‘(:~~:) j j a a’
• In the second argument of ‘App’, namely ‘HRefl’
In the type signature:
(%:~~:->) :: forall (j :: Type)
(k :: Type)
(a :: j)
(b :: k)
(r :: a :~~: b)
(p :: forall (z :: Type) (y :: z). a :~~: y -> Type).
Sing r -> App p HRefl -> App p r
|
21 | -> App p HRefl
| ^^^^^
Bug.hs:22:20: error:
• Expected kind ‘(:~~:) j z a b’, but ‘r’ has kind ‘(:~~:) j k a b’
• In the second argument of ‘App’, namely ‘r’
In the type signature:
(%:~~:->) :: forall (j :: Type)
(k :: Type)
(a :: j)
(b :: k)
(r :: a :~~: b)
(p :: forall (z :: Type) (y :: z). a :~~: y -> Type).
Sing r -> App p HRefl -> App p r
|
22 | -> App p r
| ^
```
These errors are surprising to me, since it appears that the two higher-rank types, `z` and `y`, are behaving differently here: `y` appears to be willing to unify with other types in applications of `p`, but `z` isn't! I would expect //both// to be willing to unify in applications of `p`.
Out of desperation, I tried this other formulation of `(%:~~:->)` which uses `HRApp` instead of `App`:
```hs
(%:~~:->) :: forall (j :: Type) (k :: Type) (a :: j) (b :: k) (r :: a :~~: b) (p :: forall (z :: Type) (y :: z). a :~~: y -> Type).
Sing r
-> HRApp p HRefl
-> HRApp p r
```
But now I get an even stranger error message:
```
$ /opt/ghc/8.2.1/bin/ghci Bug.hs -fprint-explicit-kinds -fprint-explicit-foralls
GHCi, version 8.2.0.20170623: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:21:20: error:
• Expected kind ‘forall z (y :: z). (:~~:) j z a y -> *’,
but ‘p’ has kind ‘forall z (y :: z). (:~~:) j z a y -> *’
• In the first argument of ‘HRApp’, namely ‘p’
In the type signature:
(%:~~:->) :: forall (j :: Type)
(k :: Type)
(a :: j)
(b :: k)
(r :: a :~~: b)
(p :: forall (z :: Type) (y :: z). a :~~: y -> Type).
Sing r -> HRApp p HRefl -> HRApp p r
|
21 | -> HRApp p HRefl
| ^
Bug.hs:21:20: error:
• Expected kind ‘forall z (y :: z). (:~~:) j z a y -> *’,
but ‘p’ has kind ‘forall z (y :: z). (:~~:) j z a y -> *’
• In the first argument of ‘HRApp’, namely ‘p’
In the type signature:
(%:~~:->) :: forall (j :: Type)
(k :: Type)
(a :: j)
(b :: k)
(r :: a :~~: b)
(p :: forall (z :: Type) (y :: z). a :~~: y -> Type).
Sing r -> HRApp p HRefl -> HRApp p r
|
21 | -> HRApp p HRefl
| ^
Bug.hs:22:20: error:
• Expected kind ‘forall z (y :: z). (:~~:) j z a y -> *’,
but ‘p’ has kind ‘forall z (y :: z). (:~~:) j z a y -> *’
• In the first argument of ‘HRApp’, namely ‘p’
In the type signature:
(%:~~:->) :: forall (j :: Type)
(k :: Type)
(a :: j)
(b :: k)
(r :: a :~~: b)
(p :: forall (z :: Type) (y :: z). a :~~: y -> Type).
Sing r -> HRApp p HRefl -> HRApp p r
|
22 | -> HRApp p r
| ^
```
That's right, it can't match the kinds:
- `forall z (y :: z). (:~~:) j z a y -> *`, and
- `forall z (y :: z). (:~~:) j z a y -> *`
Uh... what? Those are the same kind!
<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":"Strange interaction between higher-rank kinds and type synonyms","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Here's some code with typechecks with GHC 8.0.1, 8.0.2, 8.2.1, and HEAD:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE RankNTypes #-}\r\n{-# LANGUAGE ScopedTypeVariables #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# LANGUAGE TypeOperators #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ndata family Sing (a :: k)\r\n\r\ndata (a :: j) :~~: (b :: k) where\r\n HRefl :: a :~~: a\r\n\r\ndata instance Sing (z :: a :~~: b) where\r\n SHRefl :: Sing HRefl\r\n\r\n(%:~~:->) :: forall (j :: Type) (k :: Type) (a :: j) (b :: k) (r :: a :~~: b) (p :: forall (z :: Type) (y :: z). a :~~: y -> Type).\r\n Sing r\r\n -> p HRefl\r\n -> p r\r\n(%:~~:->) SHRefl pHRefl = pHRefl\r\n\r\ntype App f x = f x\r\ntype HRApp (f :: forall (z :: Type) (y :: z). a :~~: y -> Type) (x :: a :~~: b) = f x\r\n}}}\r\n\r\nNow I want to refactor this so that I use `App`:\r\n\r\n{{{#!hs\r\n(%:~~:->) :: forall (j :: Type) (k :: Type) (a :: j) (b :: k) (r :: a :~~: b) (p :: forall (z :: Type) (y :: z). a :~~: y -> Type).\r\n Sing r\r\n -> App p HRefl\r\n -> App p r\r\n}}}\r\n\r\nHowever, GHC doesn't like that:\r\n\r\n{{{\r\n$ /opt/ghc/8.2.1/bin/ghci Bug.hs -fprint-explicit-kinds -fprint-explicit-foralls\r\nGHCi, version 8.2.0.20170623: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\n\r\nBug.hs:21:20: error:\r\n • Expected kind ‘(:~~:) j z a a’,\r\n but ‘'HRefl j a’ has kind ‘(:~~:) j j a a’\r\n • In the second argument of ‘App’, namely ‘HRefl’\r\n In the type signature:\r\n (%:~~:->) :: forall (j :: Type)\r\n (k :: Type)\r\n (a :: j)\r\n (b :: k)\r\n (r :: a :~~: b)\r\n (p :: forall (z :: Type) (y :: z). a :~~: y -> Type).\r\n Sing r -> App p HRefl -> App p r\r\n |\r\n21 | -> App p HRefl\r\n | ^^^^^\r\n\r\nBug.hs:22:20: error:\r\n • Expected kind ‘(:~~:) j z a b’, but ‘r’ has kind ‘(:~~:) j k a b’\r\n • In the second argument of ‘App’, namely ‘r’\r\n In the type signature:\r\n (%:~~:->) :: forall (j :: Type)\r\n (k :: Type)\r\n (a :: j)\r\n (b :: k)\r\n (r :: a :~~: b)\r\n (p :: forall (z :: Type) (y :: z). a :~~: y -> Type).\r\n Sing r -> App p HRefl -> App p r\r\n |\r\n22 | -> App p r\r\n | ^\r\n}}}\r\n\r\nThese errors are surprising to me, since it appears that the two higher-rank types, `z` and `y`, are behaving differently here: `y` appears to be willing to unify with other types in applications of `p`, but `z` isn't! I would expect //both// to be willing to unify in applications of `p`.\r\n\r\nOut of desperation, I tried this other formulation of `(%:~~:->)` which uses `HRApp` instead of `App`:\r\n\r\n{{{#!hs\r\n(%:~~:->) :: forall (j :: Type) (k :: Type) (a :: j) (b :: k) (r :: a :~~: b) (p :: forall (z :: Type) (y :: z). a :~~: y -> Type).\r\n Sing r\r\n -> HRApp p HRefl\r\n -> HRApp p r\r\n}}}\r\n\r\nBut now I get an even stranger error message:\r\n\r\n{{{\r\n$ /opt/ghc/8.2.1/bin/ghci Bug.hs -fprint-explicit-kinds -fprint-explicit-foralls\r\nGHCi, version 8.2.0.20170623: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\n\r\nBug.hs:21:20: error:\r\n • Expected kind ‘forall z (y :: z). (:~~:) j z a y -> *’,\r\n but ‘p’ has kind ‘forall z (y :: z). (:~~:) j z a y -> *’\r\n • In the first argument of ‘HRApp’, namely ‘p’\r\n In the type signature:\r\n (%:~~:->) :: forall (j :: Type)\r\n (k :: Type)\r\n (a :: j)\r\n (b :: k)\r\n (r :: a :~~: b)\r\n (p :: forall (z :: Type) (y :: z). a :~~: y -> Type).\r\n Sing r -> HRApp p HRefl -> HRApp p r\r\n |\r\n21 | -> HRApp p HRefl\r\n | ^\r\n\r\nBug.hs:21:20: error:\r\n • Expected kind ‘forall z (y :: z). (:~~:) j z a y -> *’,\r\n but ‘p’ has kind ‘forall z (y :: z). (:~~:) j z a y -> *’\r\n • In the first argument of ‘HRApp’, namely ‘p’\r\n In the type signature:\r\n (%:~~:->) :: forall (j :: Type)\r\n (k :: Type)\r\n (a :: j)\r\n (b :: k)\r\n (r :: a :~~: b)\r\n (p :: forall (z :: Type) (y :: z). a :~~: y -> Type).\r\n Sing r -> HRApp p HRefl -> HRApp p r\r\n |\r\n21 | -> HRApp p HRefl\r\n | ^\r\n\r\nBug.hs:22:20: error:\r\n • Expected kind ‘forall z (y :: z). (:~~:) j z a y -> *’,\r\n but ‘p’ has kind ‘forall z (y :: z). (:~~:) j z a y -> *’\r\n • In the first argument of ‘HRApp’, namely ‘p’\r\n In the type signature:\r\n (%:~~:->) :: forall (j :: Type)\r\n (k :: Type)\r\n (a :: j)\r\n (b :: k)\r\n (r :: a :~~: b)\r\n (p :: forall (z :: Type) (y :: z). a :~~: y -> Type).\r\n Sing r -> HRApp p HRefl -> HRApp p r\r\n |\r\n22 | -> HRApp p r\r\n | ^\r\n}}}\r\n\r\nThat's right, it can't match the kinds:\r\n\r\n* `forall z (y :: z). (:~~:) j z a y -> *`, and\r\n* `forall z (y :: z). (:~~:) j z a y -> *`\r\n\r\nUh... what? Those are the same kind!","type_of_failure":"OtherFailure","blocking":[]} -->8.2.1https://gitlab.haskell.org/ghc/ghc/-/issues/13895"Illegal constraint in a type" error - is it fixable?2019-07-07T18:19:36ZRyan Scott"Illegal constraint in a type" error - is it fixable?I recently sketched out a solution to #13327. Here is the type signature that I wanted to write:
```hs
dataCast1 :: forall (c :: Type -> Type) (t :: forall (k :: Type). k -> Type).
Typeable t
=> (forall d. Data d ...I recently sketched out a solution to #13327. Here is the type signature that I wanted to write:
```hs
dataCast1 :: forall (c :: Type -> Type) (t :: forall (k :: Type). k -> Type).
Typeable t
=> (forall d. Data d => c (t d))
-> Maybe (c a)
```
But this doesn't typecheck:
```
• Could not deduce (Typeable (t k0))
from the context: (Data a, Typeable (t k))
bound by the type signature for:
dataCast1 :: forall a.
Data a =>
forall k (c :: * -> *) (t :: forall k1. k1 -> *).
Typeable (t k) =>
(forall d. Data d => c (t * d)) -> Maybe (c a)
at NewData.hs:(170,3)-(173,26)
The type variable ‘k0’ is ambiguous
• In the ambiguity check for ‘dataCast1’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
When checking the class method:
dataCast1 :: forall a.
Data a =>
forall k (c :: * -> *) (t :: forall k1. k1 -> *).
Typeable (t k) =>
(forall d. Data d => c (t * d)) -> Maybe (c a)
In the class declaration for ‘Data’
|
170 | dataCast1 :: forall (c :: Type -> Type) (t :: forall (k :: Type). k -> Type).
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
```
This makes sense, since GHC has no way to conclude that the `k` in `t`'s kind is also `Typeable`. I tried to convince GHC of that fact:
```hs
dataCast1 :: forall (c :: Type -> Type) (t :: forall (k :: Type). Typeable k => k -> Type).
Typeable t
=> (forall d. Data d => c (t d))
-> Maybe (c a)
```
But this also doesn't work:
```
NewData.hs:171:25: error:
• Illegal constraint in a type: Typeable k0
• In the first argument of ‘Typeable’, namely ‘t’
In the type signature:
dataCast1 :: forall (c :: Type -> Type)
(t :: forall (k :: Type). Typeable k => k -> Type).
Typeable t => (forall d. Data d => c (t d)) -> Maybe (c a)
In the class declaration for ‘Data’
|
171 | Typeable t
| ^
NewData.hs:172:40: error:
• Illegal constraint in a type: Typeable k0
• In the first argument of ‘c’, namely ‘(t d)’
In the type signature:
dataCast1 :: forall (c :: Type -> Type)
(t :: forall (k :: Type). Typeable k => k -> Type).
Typeable t => (forall d. Data d => c (t d)) -> Maybe (c a)
In the class declaration for ‘Data’
|
172 | => (forall d. Data d => c (t d))
| ^^^
```
At this point, I'm stuck, since I have no idea how to work around this `Illegal constraint in a type` error. This error message appears to have originated as a part of the `TypeInType` patch, since there's even a [test case](http://git.haskell.org/ghc.git/blob/58c781da4861faab11e4c5804e07e6892908ef72:/testsuite/tests/dependent/should_fail/PromotedClass.hs) checking for this behavior.
But is this a fundamental limitation of kind equalities? Or would it be possible to lift this restriction?
<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":"\"Illegal constraint in a type\" error - is it fixable?","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I recently sketched out a solution to #13327. Here is the type signature that I wanted to write:\r\n\r\n{{{#!hs\r\ndataCast1 :: forall (c :: Type -> Type) (t :: forall (k :: Type). k -> Type).\r\n Typeable t\r\n => (forall d. Data d => c (t d))\r\n -> Maybe (c a)\r\n}}}\r\n\r\nBut this doesn't typecheck:\r\n\r\n{{{\r\n • Could not deduce (Typeable (t k0))\r\n from the context: (Data a, Typeable (t k))\r\n bound by the type signature for:\r\n dataCast1 :: forall a.\r\n Data a =>\r\n forall k (c :: * -> *) (t :: forall k1. k1 -> *).\r\n Typeable (t k) =>\r\n (forall d. Data d => c (t * d)) -> Maybe (c a)\r\n at NewData.hs:(170,3)-(173,26)\r\n The type variable ‘k0’ is ambiguous\r\n • In the ambiguity check for ‘dataCast1’\r\n To defer the ambiguity check to use sites, enable AllowAmbiguousTypes\r\n When checking the class method:\r\n dataCast1 :: forall a.\r\n Data a =>\r\n forall k (c :: * -> *) (t :: forall k1. k1 -> *).\r\n Typeable (t k) =>\r\n (forall d. Data d => c (t * d)) -> Maybe (c a)\r\n In the class declaration for ‘Data’\r\n |\r\n170 | dataCast1 :: forall (c :: Type -> Type) (t :: forall (k :: Type). k -> Type).\r\n | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...\r\n}}}\r\n\r\nThis makes sense, since GHC has no way to conclude that the `k` in `t`'s kind is also `Typeable`. I tried to convince GHC of that fact:\r\n\r\n{{{#!hs\r\ndataCast1 :: forall (c :: Type -> Type) (t :: forall (k :: Type). Typeable k => k -> Type).\r\n Typeable t\r\n => (forall d. Data d => c (t d))\r\n -> Maybe (c a)\r\n}}}\r\n\r\nBut this also doesn't work:\r\n\r\n{{{\r\nNewData.hs:171:25: error:\r\n • Illegal constraint in a type: Typeable k0\r\n • In the first argument of ‘Typeable’, namely ‘t’\r\n In the type signature:\r\n dataCast1 :: forall (c :: Type -> Type)\r\n (t :: forall (k :: Type). Typeable k => k -> Type).\r\n Typeable t => (forall d. Data d => c (t d)) -> Maybe (c a)\r\n In the class declaration for ‘Data’\r\n |\r\n171 | Typeable t\r\n | ^\r\n\r\nNewData.hs:172:40: error:\r\n • Illegal constraint in a type: Typeable k0\r\n • In the first argument of ‘c’, namely ‘(t d)’\r\n In the type signature:\r\n dataCast1 :: forall (c :: Type -> Type)\r\n (t :: forall (k :: Type). Typeable k => k -> Type).\r\n Typeable t => (forall d. Data d => c (t d)) -> Maybe (c a)\r\n In the class declaration for ‘Data’\r\n |\r\n172 | => (forall d. Data d => c (t d))\r\n | ^^^\r\n}}}\r\n\r\nAt this point, I'm stuck, since I have no idea how to work around this `Illegal constraint in a type` error. This error message appears to have originated as a part of the `TypeInType` patch, since there's even a [http://git.haskell.org/ghc.git/blob/58c781da4861faab11e4c5804e07e6892908ef72:/testsuite/tests/dependent/should_fail/PromotedClass.hs test case] checking for this behavior.\r\n\r\nBut is this a fundamental limitation of kind equalities? Or would it be possible to lift this restriction?","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/13909Misleading error message when partially applying a data type with a visible q...2019-07-07T18:19:32ZRyan ScottMisleading error message when partially applying a data type with a visible quantifier in its kindI'm not sure if this is a bug or an intended design, so I'll ask here. I want this program to typecheck:
```hs
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
data Hm (k :: Type) (a :: k) :: Type
class HasName (a :: k) ...I'm not sure if this is a bug or an intended design, so I'll ask here. I want this program to typecheck:
```hs
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
data Hm (k :: Type) (a :: k) :: Type
class HasName (a :: k) where
getName :: proxy a -> String
instance HasName Hm where
getName _ = "Hm"
```
This is rejected, however:
```
$ /opt/ghc/8.2.1/bin/ghci Bug.hs
GHCi, version 8.2.0.20170623: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/ryanglscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:11:18: error:
• Expecting two more arguments to ‘Hm’
Expected kind ‘k0’, but ‘Hm’ has kind ‘forall k -> k -> *’
• In the first argument of ‘HasName’, namely ‘Hm’
In the instance declaration for ‘HasName Hm’
|
11 | instance HasName Hm where
| ^^
```
The culprit appears to be the fact that `Hm` has kind `forall k -> k -> *`, which uses a visible quantifier. Does this prevent partial applications of `Hm`? Or is this simply a GHC bug?
<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":"Can't partially apply a data type with a visible quantifier in its kind","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I'm not sure if this is a bug or an intended design, so I'll ask here. I want this program to typecheck:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE TypeInType #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ndata Hm (k :: Type) (a :: k) :: Type\r\n\r\nclass HasName (a :: k) where\r\n getName :: proxy a -> String\r\n\r\ninstance HasName Hm where\r\n getName _ = \"Hm\"\r\n}}}\r\n\r\nThis is rejected, however:\r\n\r\n{{{\r\n$ /opt/ghc/8.2.1/bin/ghci Bug.hs\r\nGHCi, version 8.2.0.20170623: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/ryanglscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\n\r\nBug.hs:11:18: error:\r\n • Expecting two more arguments to ‘Hm’\r\n Expected kind ‘k0’, but ‘Hm’ has kind ‘forall k -> k -> *’\r\n • In the first argument of ‘HasName’, namely ‘Hm’\r\n In the instance declaration for ‘HasName Hm’\r\n |\r\n11 | instance HasName Hm where\r\n | ^^\r\n}}}\r\n\r\nThe culprit appears to be the fact that `Hm` has kind `forall k -> k -> *`, which uses a visible quantifier. Does this prevent partial applications of `Hm`? Or is this simply a GHC bug?","type_of_failure":"OtherFailure","blocking":[]} -->8.4.1https://gitlab.haskell.org/ghc/ghc/-/issues/13910Inlining a definition causes GHC to panic (repSplitTyConApp_maybe)2019-07-07T18:19:31ZRyan ScottInlining a definition causes GHC to panic (repSplitTyConApp_maybe)Here is a program which I believe //should// typecheck:
```hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-} ...Here is a program which I believe //should// typecheck:
```hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Kind
import Data.Type.Equality
data family Sing (a :: k)
class SingKind k where
type Demote k = (r :: *) | r -> k
fromSing :: Sing (a :: k) -> Demote k
toSing :: Demote k -> SomeSing k
data SomeSing k where
SomeSing :: Sing (a :: k) -> SomeSing k
withSomeSing :: forall k r
. SingKind k
=> Demote k
-> (forall (a :: k). Sing a -> r)
-> r
withSomeSing x f =
case toSing x of
SomeSing x' -> f x'
data TyFun :: * -> * -> *
type a ~> b = TyFun a b -> *
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
data instance Sing (z :: a :~: b) where
SRefl :: Sing Refl
instance SingKind (a :~: b) where
type Demote (a :~: b) = a :~: b
fromSing SRefl = Refl
toSing Refl = SomeSing SRefl
(~>:~:) :: forall (k :: Type) (a :: k) (b :: k) (r :: a :~: b) (p :: forall (y :: k). a :~: y ~> Type).
Sing r
-> p @@ Refl
-> p @@ r
(~>:~:) SRefl pRefl = pRefl
type WhyReplacePoly (arr :: FunArrow) (from :: t) (p :: (t -?> Type) arr)
(y :: t) (e :: from :~: y) = App t arr Type p y
data WhyReplacePolySym (arr :: FunArrow) (from :: t) (p :: (t -?> Type) arr)
:: forall (y :: t). from :~: y ~> Type
type instance Apply (WhyReplacePolySym arr from p :: from :~: y ~> Type) x
= WhyReplacePoly arr from p y x
replace :: forall (t :: Type) (from :: t) (to :: t) (p :: t -> Type).
p from
-> from :~: to
-> p to
replace = replacePoly @(:->)
replaceTyFun :: forall (t :: Type) (from :: t) (to :: t) (p :: t ~> Type).
p @@ from
-> from :~: to
-> p @@ to
replaceTyFun = replacePoly @(:~>) @_ @_ @_ @p
replacePoly :: forall (arr :: FunArrow) (t :: Type) (from :: t) (to :: t)
(p :: (t -?> Type) arr).
FunApp arr
=> App t arr Type p from
-> from :~: to
-> App t arr Type p to
replacePoly from eq =
withSomeSing eq $ \(singEq :: Sing r) ->
(~>:~:) @t @from @to @r @(WhyReplacePolySym arr from p) singEq from
type WhyLeibnizPoly (arr :: FunArrow) (f :: (t -?> Type) arr) (a :: t) (z :: t)
= App t arr Type f a -> App t arr Type f z
data WhyLeibnizPolySym (arr :: FunArrow) (f :: (t -?> Type) arr) (a :: t)
:: t ~> Type
type instance Apply (WhyLeibnizPolySym arr f a) z = WhyLeibnizPoly arr f a z
leibnizPoly :: forall (arr :: FunArrow) (t :: Type) (f :: (t -?> Type) arr)
(a :: t) (b :: t).
FunApp arr
=> a :~: b
-> App t arr Type f a
-> App t arr Type f b
leibnizPoly = replaceTyFun @t @a @b @(WhyLeibnizPolySym arr f a) id
leibniz :: forall (t :: Type) (f :: t -> Type) (a :: t) (b :: t).
a :~: b
-> f a
-> f b
leibniz = replaceTyFun @t @a @b @(WhyLeibnizPolySym (:->) f a) id
-- The line above is what you get if you inline the definition of leibnizPoly.
-- It causes a panic, however.
--
-- An equivalent implementation is commented out below, which does *not*
-- cause GHC to panic.
--
-- leibniz = leibnizPoly @(:->)
leibnizTyFun :: forall (t :: Type) (f :: t ~> Type) (a :: t) (b :: t).
a :~: b
-> f @@ a
-> f @@ b
leibnizTyFun = leibnizPoly @(:~>) @_ @f
```
GHC 8.2.1 and HEAD panic on the definition of `leibniz`, however:
```
$ /opt/ghc/8.2.1/bin/ghci Bug.hs
GHCi, version 8.2.0.20170623: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
ghc: panic! (the 'impossible' happened)
(GHC version 8.2.0.20170623 for x86_64-unknown-linux):
repSplitTyConApp_maybe
(f_a5vT[sk:2] |> Sym (Trans
(Sym (D:R:Funk1:->k2[0] <k1>_N <k2>_N))
(D:R:Funk1:->k2[0] <t>_N <*>_N))) a_a5vU[sk:2]
(f_a5vT[sk:2] |> Sym (Trans
(Sym (D:R:Funk1:->k2[0] <k1>_N <k2>_N))
(D:R:Funk1:->k2[0] <t>_N <*>_N))) a_a5vU[sk:2]
k2_a5l0
Call stack:
CallStack (from HasCallStack):
prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1133:58 in ghc:Outputable
callStackDoc, called at compiler/utils/Outputable.hs:1137:37 in ghc:Outputable
pprPanic, called at compiler/types/Type.hs:1122:5 in ghc:Type
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
```
Interestingly, GHC 8.0.1 and 8.0.2 do not give the same panic—they give the panic from #13877:
```
$ /opt/ghc/8.0.2/bin/ghci Bug.hs
GHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:134:64: error:ghc: panic! (the 'impossible' happened)
(GHC version 8.0.2 for x86_64-unknown-linux):
No skolem info: k2_a4KV
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.2.1-rc2 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | #13877 |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Inlining a definition causes GHC to panic (repSplitTyConApp_maybe)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[13877],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1-rc2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Here is a program which I believe //should// typecheck:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE AllowAmbiguousTypes #-} \r\n{-# LANGUAGE ConstraintKinds #-} \r\n{-# LANGUAGE GADTs #-} \r\n{-# LANGUAGE RankNTypes #-} \r\n{-# LANGUAGE ScopedTypeVariables #-} \r\n{-# LANGUAGE TemplateHaskell #-} \r\n{-# LANGUAGE Trustworthy #-} \r\n{-# LANGUAGE TypeApplications #-} \r\n{-# LANGUAGE TypeFamilyDependencies #-} \r\n{-# LANGUAGE TypeInType #-} \r\n{-# LANGUAGE TypeOperators #-} \r\nmodule Bug where \r\n \r\nimport Data.Kind \r\nimport Data.Type.Equality \r\n \r\ndata family Sing (a :: k)\r\n\r\nclass SingKind k where\r\n type Demote k = (r :: *) | r -> k\r\n fromSing :: Sing (a :: k) -> Demote k\r\n toSing :: Demote k -> SomeSing k\r\n\r\ndata SomeSing k where\r\n SomeSing :: Sing (a :: k) -> SomeSing k\r\n\r\nwithSomeSing :: forall k r\r\n . SingKind k\r\n => Demote k\r\n -> (forall (a :: k). Sing a -> r)\r\n -> r\r\nwithSomeSing x f =\r\n case toSing x of\r\n SomeSing x' -> f x'\r\n\r\ndata TyFun :: * -> * -> *\r\ntype a ~> b = TyFun a b -> *\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\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\ndata instance Sing (z :: a :~: b) where\r\n SRefl :: Sing Refl\r\n\r\ninstance SingKind (a :~: b) where\r\n type Demote (a :~: b) = a :~: b\r\n fromSing SRefl = Refl\r\n toSing Refl = SomeSing SRefl\r\n\r\n(~>:~:) :: forall (k :: Type) (a :: k) (b :: k) (r :: a :~: b) (p :: forall (y :: k). a :~: y ~> Type).\r\n Sing r\r\n -> p @@ Refl\r\n -> p @@ r\r\n(~>:~:) SRefl pRefl = pRefl\r\n\r\ntype WhyReplacePoly (arr :: FunArrow) (from :: t) (p :: (t -?> Type) arr)\r\n (y :: t) (e :: from :~: y) = App t arr Type p y\r\ndata WhyReplacePolySym (arr :: FunArrow) (from :: t) (p :: (t -?> Type) arr)\r\n :: forall (y :: t). from :~: y ~> Type\r\ntype instance Apply (WhyReplacePolySym arr from p :: from :~: y ~> Type) x\r\n = WhyReplacePoly arr from p y x\r\n\r\nreplace :: forall (t :: Type) (from :: t) (to :: t) (p :: t -> Type).\r\n p from\r\n -> from :~: to\r\n -> p to\r\nreplace = replacePoly @(:->)\r\n\r\nreplaceTyFun :: forall (t :: Type) (from :: t) (to :: t) (p :: t ~> Type).\r\n p @@ from\r\n -> from :~: to\r\n -> p @@ to\r\nreplaceTyFun = replacePoly @(:~>) @_ @_ @_ @p\r\n\r\nreplacePoly :: forall (arr :: FunArrow) (t :: Type) (from :: t) (to :: t)\r\n (p :: (t -?> Type) arr).\r\n FunApp arr\r\n => App t arr Type p from\r\n -> from :~: to\r\n -> App t arr Type p to\r\nreplacePoly from eq =\r\n withSomeSing eq $ \\(singEq :: Sing r) ->\r\n (~>:~:) @t @from @to @r @(WhyReplacePolySym arr from p) singEq from\r\n\r\ntype WhyLeibnizPoly (arr :: FunArrow) (f :: (t -?> Type) arr) (a :: t) (z :: t)\r\n = App t arr Type f a -> App t arr Type f z\r\ndata WhyLeibnizPolySym (arr :: FunArrow) (f :: (t -?> Type) arr) (a :: t)\r\n :: t ~> Type\r\ntype instance Apply (WhyLeibnizPolySym arr f a) z = WhyLeibnizPoly arr f a z\r\n\r\nleibnizPoly :: forall (arr :: FunArrow) (t :: Type) (f :: (t -?> Type) arr)\r\n (a :: t) (b :: t).\r\n FunApp arr\r\n => a :~: b\r\n -> App t arr Type f a\r\n -> App t arr Type f b\r\nleibnizPoly = replaceTyFun @t @a @b @(WhyLeibnizPolySym arr f a) id\r\n\r\nleibniz :: forall (t :: Type) (f :: t -> Type) (a :: t) (b :: t).\r\n a :~: b\r\n -> f a\r\n -> f b\r\nleibniz = replaceTyFun @t @a @b @(WhyLeibnizPolySym (:->) f a) id\r\n-- The line above is what you get if you inline the definition of leibnizPoly.\r\n-- It causes a panic, however.\r\n--\r\n-- An equivalent implementation is commented out below, which does *not*\r\n-- cause GHC to panic.\r\n--\r\n-- leibniz = leibnizPoly @(:->)\r\n\r\nleibnizTyFun :: forall (t :: Type) (f :: t ~> Type) (a :: t) (b :: t).\r\n a :~: b\r\n -> f @@ a\r\n -> f @@ b\r\nleibnizTyFun = leibnizPoly @(:~>) @_ @f\r\n}}}\r\n\r\nGHC 8.2.1 and HEAD panic on the definition of `leibniz`, however:\r\n\r\n{{{\r\n$ /opt/ghc/8.2.1/bin/ghci Bug.hs\r\nGHCi, version 8.2.0.20170623: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\nghc: panic! (the 'impossible' happened)\r\n (GHC version 8.2.0.20170623 for x86_64-unknown-linux):\r\n repSplitTyConApp_maybe\r\n (f_a5vT[sk:2] |> Sym (Trans\r\n (Sym (D:R:Funk1:->k2[0] <k1>_N <k2>_N))\r\n (D:R:Funk1:->k2[0] <t>_N <*>_N))) a_a5vU[sk:2]\r\n (f_a5vT[sk:2] |> Sym (Trans\r\n (Sym (D:R:Funk1:->k2[0] <k1>_N <k2>_N))\r\n (D:R:Funk1:->k2[0] <t>_N <*>_N))) a_a5vU[sk:2]\r\n k2_a5l0\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1133:58 in ghc:Outputable\r\n callStackDoc, called at compiler/utils/Outputable.hs:1137:37 in ghc:Outputable\r\n pprPanic, called at compiler/types/Type.hs:1122:5 in ghc:Type\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n}}}\r\n\r\nInterestingly, GHC 8.0.1 and 8.0.2 do not give the same panic—they give the panic from #13877:\r\n\r\n{{{\r\n$ /opt/ghc/8.0.2/bin/ghci Bug.hs\r\nGHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help \r\nLoaded GHCi configuration from /home/rgscott/.ghci \r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted ) \r\n \r\nBug.hs:134:64: error:ghc: panic! (the 'impossible' happened) \r\n (GHC version 8.0.2 for x86_64-unknown-linux): \r\n No skolem info: k2_a4KV \r\n \r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/13913Can't apply higher-ranked kind in type family2019-07-07T18:19:30ZRyan ScottCan't apply higher-ranked kind in type familyThis code doesn't typecheck due to `F2`:
```hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
f :: (forall (a :: Type). a -> a) -> Bool
f g = g True
type F1 (g ...This code doesn't typecheck due to `F2`:
```hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
f :: (forall (a :: Type). a -> a) -> Bool
f g = g True
type F1 (g :: forall (a :: Type). a -> a) = g True
type family F2 (g :: forall (a :: Type). a -> a) :: Bool where
F2 g = g True
```
```
$ /opt/ghc/8.2.1/bin/ghci Bug.hs
GHCi, version 8.2.0.20170623: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:14:6: error:
• Expected kind ‘forall a. a -> a’, but ‘g’ has kind ‘Bool -> Bool’
• In the first argument of ‘F2’, namely ‘g’
In the type family declaration for ‘F2’
|
14 | F2 g = g True
| ^
```
This is surprising to me, since `F2` seems like the type family counterpart to `f` and `F1`, both of which typecheck.
<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":"Can't apply higher-ranked kind in type family","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This code doesn't typecheck due to `F2`:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE RankNTypes #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\nf :: (forall (a :: Type). a -> a) -> Bool\r\nf g = g True\r\n\r\ntype F1 (g :: forall (a :: Type). a -> a) = g True\r\n\r\ntype family F2 (g :: forall (a :: Type). a -> a) :: Bool where\r\n F2 g = g True\r\n}}}\r\n\r\n{{{\r\n$ /opt/ghc/8.2.1/bin/ghci Bug.hs\r\nGHCi, version 8.2.0.20170623: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\n\r\nBug.hs:14:6: error:\r\n • Expected kind ‘forall a. a -> a’, but ‘g’ has kind ‘Bool -> Bool’\r\n • In the first argument of ‘F2’, namely ‘g’\r\n In the type family declaration for ‘F2’\r\n |\r\n14 | F2 g = g True\r\n | ^\r\n}}}\r\n\r\nThis is surprising to me, since `F2` seems like the type family counterpart to `f` and `F1`, both of which typecheck.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/13915GHC 8.2 regression: "Can't find interface-file declaration" for promoted data...2019-07-07T18:19:30ZRyan ScottGHC 8.2 regression: "Can't find interface-file declaration" for promoted data family instanceDue to #12088, you can't define a data family instance and promote it in the same module. One could, up until GHC 8.2, work around this using (somewhat obscure) wisdom: define the data family instance in a separate module from where it's...Due to #12088, you can't define a data family instance and promote it in the same module. One could, up until GHC 8.2, work around this using (somewhat obscure) wisdom: define the data family instance in a separate module from where it's promoted. For example, `Bug` typechecks in GHC 8.0.1 and 8.0.2:
```hs
{-# LANGUAGE TypeFamilies #-}
module Foo where
data family T a
data instance T Int = MkT
```
```hs
{-# LANGUAGE TypeInType #-}
module Bug where
import Foo
data Proxy (a :: k)
data S = MkS (Proxy 'MkT)
```
However, this stopped typechecking in GHC 8.2:
```
$ /opt/ghc/8.2.1/bin/ghci Bug.hs
GHCi, version 8.2.0.20170623: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 2] Compiling Foo ( Foo.hs, interpreted )
[2 of 2] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:1:1: error:
Can't find interface-file declaration for variable Foo.$tc'MkT
Probable cause: bug in .hi-boot file, or inconsistent .hi file
Use -ddump-if-trace to get an idea of which file caused the error
|
1 | {-# LANGUAGE TypeInType #-}
| ^
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.2.1-rc2 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | high |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC 8.2 regression: \"Can't find interface-file declaration\" for promoted data family instance","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.2.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1-rc2","keywords":["TypeFamilies","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Due to #12088, you can't define a data family instance and promote it in the same module. One could, up until GHC 8.2, work around this using (somewhat obscure) wisdom: define the data family instance in a separate module from where it's promoted. For example, `Bug` typechecks in GHC 8.0.1 and 8.0.2:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE TypeFamilies #-}\r\nmodule Foo where\r\n\r\ndata family T a\r\ndata instance T Int = MkT\r\n}}}\r\n{{{#!hs\r\n{-# LANGUAGE TypeInType #-}\r\nmodule Bug where\r\n\r\nimport Foo\r\n\r\ndata Proxy (a :: k)\r\ndata S = MkS (Proxy 'MkT)\r\n}}}\r\n\r\nHowever, this stopped typechecking in GHC 8.2:\r\n\r\n{{{\r\n$ /opt/ghc/8.2.1/bin/ghci Bug.hs\r\nGHCi, version 8.2.0.20170623: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 2] Compiling Foo ( Foo.hs, interpreted )\r\n[2 of 2] Compiling Bug ( Bug.hs, interpreted )\r\n\r\nBug.hs:1:1: error:\r\n Can't find interface-file declaration for variable Foo.$tc'MkT\r\n Probable cause: bug in .hi-boot file, or inconsistent .hi file\r\n Use -ddump-if-trace to get an idea of which file caused the error\r\n |\r\n1 | {-# LANGUAGE TypeInType #-}\r\n | ^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.2.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.1https://gitlab.haskell.org/ghc/ghc/-/issues/13972GHC 8.2 error message around indexes for associated type instances is baffling2019-07-07T18:19:06ZRyan ScottGHC 8.2 error message around indexes for associated type instances is bafflingThis program doesn't typecheck (only in GHC 8.2 and later):
```hs
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
class C (a :: k) where
type T k :: Type
instan...This program doesn't typecheck (only in GHC 8.2 and later):
```hs
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
class C (a :: k) where
type T k :: Type
instance C Left where
type T (a -> Either a b) = Int
```
```
$ /opt/ghc/8.2.1/bin/ghci Bug.hs
GHCi, version 8.2.0.20170704: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:12:8: error:
• Type indexes must match class instance head
Expected: T (a -> Either a b)
Actual: T (a -> Either a b)
• In the type instance declaration for ‘T’
In the instance declaration for ‘C Left’
|
12 | type T (a -> Either a b) = Int
| ^^^^^^^^^^^^^^^^^^^^^^^^^
```
Well those expected and actual types look pretty darn similar to me!
Note that the problem can be worked around by giving an explicit kind annotation for `Left`:
```hs
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
class C (a :: k) where
type T k :: Type
instance C (Left :: a -> Either a b) where
type T (a -> Either a b) = Int
```
I see two things we could do here:
1. Relax the "Type indexes must match class instance head" check so that it doesn't apply to invisible kind variables like `a` and `b`.
1. Clarify the error message. At the very least, we could say `Expected: T (a1 -> Either a1 b1)` as a hint that `a` and `b` aren't the same type variables as `a1` and `b1`. In an ideal world, we'd even indicate where `a1` and `b1` should be coming from (the kind of `Left`).
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.2.1-rc2 |
| 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":"GHC 8.2 error message around indexes for associated type instances is baffling","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1-rc2","keywords":["TypeFamilies,","TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This program doesn't typecheck (only in GHC 8.2 and later):\r\n\r\n{{{#!hs\r\n{-# LANGUAGE PolyKinds #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\nclass C (a :: k) where\r\n type T k :: Type\r\n\r\ninstance C Left where\r\n type T (a -> Either a b) = Int\r\n}}}\r\n\r\n{{{\r\n$ /opt/ghc/8.2.1/bin/ghci Bug.hs\r\nGHCi, version 8.2.0.20170704: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\n\r\nBug.hs:12:8: error:\r\n • Type indexes must match class instance head\r\n Expected: T (a -> Either a b)\r\n Actual: T (a -> Either a b)\r\n • In the type instance declaration for ‘T’\r\n In the instance declaration for ‘C Left’\r\n |\r\n12 | type T (a -> Either a b) = Int\r\n | ^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nWell those expected and actual types look pretty darn similar to me!\r\n\r\nNote that the problem can be worked around by giving an explicit kind annotation for `Left`:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE PolyKinds #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\nclass C (a :: k) where\r\n type T k :: Type\r\n\r\ninstance C (Left :: a -> Either a b) where\r\n type T (a -> Either a b) = Int\r\n}}}\r\n\r\nI see two things we could do here:\r\n\r\n1. Relax the \"Type indexes must match class instance head\" check so that it doesn't apply to invisible kind variables like `a` and `b`.\r\n2. Clarify the error message. At the very least, we could say `Expected: T (a1 -> Either a1 b1)` as a hint that `a` and `b` aren't the same type variables as `a1` and `b1`. In an ideal world, we'd even indicate where `a1` and `b1` should be coming from (the kind of `Left`).","type_of_failure":"OtherFailure","blocking":[]} -->8.4.1https://gitlab.haskell.org/ghc/ghc/-/issues/13988GADT constructor with kind equality constraint quantifies unused existential ...2019-07-07T18:18:58ZRyan ScottGADT constructor with kind equality constraint quantifies unused existential type variablesReproducible with GHC 8.0.1., 8.0.2, 8.2.1, or HEAD (but I'll use GHC 8.2.1 to show the results of `:type +v`):
```
$ /opt/ghc/8.2.1/bin/ghci
GHCi, version 8.2.0.20170704: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configurati...Reproducible with GHC 8.0.1., 8.0.2, 8.2.1, or HEAD (but I'll use GHC 8.2.1 to show the results of `:type +v`):
```
$ /opt/ghc/8.2.1/bin/ghci
GHCi, version 8.2.0.20170704: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
λ> :set -XTypeInType -XGADTs -fprint-explicit-foralls
λ> import Data.Kind
λ> data Foo (a :: k) where MkFoo :: (k ~ Type) => Foo (a :: k)
λ> :type +v MkFoo
MkFoo :: forall k1 (a :: k1) k2 (k3 :: k2). k1 ~ * => Foo a
```
Note that `MkFoo` quantifies two extra existential type variables, `k2` and `k3` which are completely unused!
Note that this does not occur if the `MkFoo` constructor uses an explicit `forall`:
```
λ> :set -XScopedTypeVariables
λ> data Foo (a :: k) where MkFoo :: forall k (a :: k). (k ~ Type) => Foo (a :: k)
λ> :type +v MkFoo
MkFoo :: forall k (a :: k). k ~ * => Foo a
```
<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":"GADT constructor with kind equality constraint quantifies unused existential type variables","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Reproducible with GHC 8.0.1., 8.0.2, 8.2.1, or HEAD (but I'll use GHC 8.2.1 to show the results of `:type +v`):\r\n\r\n{{{\r\n$ /opt/ghc/8.2.1/bin/ghci\r\nGHCi, version 8.2.0.20170704: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\nλ> :set -XTypeInType -XGADTs -fprint-explicit-foralls \r\nλ> import Data.Kind\r\nλ> data Foo (a :: k) where MkFoo :: (k ~ Type) => Foo (a :: k)\r\nλ> :type +v MkFoo\r\nMkFoo :: forall k1 (a :: k1) k2 (k3 :: k2). k1 ~ * => Foo a\r\n}}}\r\n\r\nNote that `MkFoo` quantifies two extra existential type variables, `k2` and `k3` which are completely unused!\r\n\r\nNote that this does not occur if the `MkFoo` constructor uses an explicit `forall`:\r\n\r\n{{{\r\nλ> :set -XScopedTypeVariables \r\nλ> data Foo (a :: k) where MkFoo :: forall k (a :: k). (k ~ Type) => Foo (a :: k)\r\nλ> :type +v MkFoo\r\nMkFoo :: forall k (a :: k). k ~ * => Foo a\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.4.1https://gitlab.haskell.org/ghc/ghc/-/issues/14162Core Lint error2019-07-07T18:18:12ZIcelandjackCore Lint error```hs
{-# Options_GHC -dcore-lint #-}
{-# Language TypeOperators, KindSignatures, DataKinds, PolyKinds, TypeFamilies, GADTs, TypeInType #-}
import Data.Kind
data family Sing (a :: k)
data
SubList :: [a] -> [a] -> Type where
SubN...```hs
{-# Options_GHC -dcore-lint #-}
{-# Language TypeOperators, KindSignatures, DataKinds, PolyKinds, TypeFamilies, GADTs, TypeInType #-}
import Data.Kind
data family Sing (a :: k)
data
SubList :: [a] -> [a] -> Type where
SubNil :: SubList '[] '[]
Keep :: SubList xs ys -> SubList (x ': xs) (x ': ys)
Drop :: SubList xs ys -> SubList xs (x ': ys)
data instance
Sing (x :: SubList ys xs) where
SSubNil :: Sing SubNil
SKeep :: Sing x -> Sing (Keep x)
SDrop :: Sing x -> Sing (Drop x)
```
running it gives a massive core lint error, attached as `lint.log`.8.2.2https://gitlab.haskell.org/ghc/ghc/-/issues/14174GHC panic with TypeInType and type family2019-07-07T18:18:09ZDavid FeuerGHC panic with TypeInType and type familyThis rather simple type family,
```hs
{-# LANGUAGE TypeFamilies, TypeOperators, TypeInType #-}
module GenWhoops where
import GHC.Generics
type family GenComp k (x :: k) (y :: k) :: Ordering where
GenComp ((x :+: y) p) ('L1 x) ('L1 y...This rather simple type family,
```hs
{-# LANGUAGE TypeFamilies, TypeOperators, TypeInType #-}
module GenWhoops where
import GHC.Generics
type family GenComp k (x :: k) (y :: k) :: Ordering where
GenComp ((x :+: y) p) ('L1 x) ('L1 y) = GenComp (x p) x y
```
produces the following panic:
```
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.3.20170828 for x86_64-unknown-linux):
piResultTy
k_a1LK[tau:1]
p_a1Lz[sk:1]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1138:37 in ghc:Outputable
pprPanic, called at compiler/types/Type.hs:949:35 in ghc:Type
```
This happens with both GHC 8.2.1 and something very close to HEAD.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.2.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | goldfire |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC panic with TypeInType and type family","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.2.2","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":["goldfire"],"type":"Bug","description":"This rather simple type family,\r\n\r\n{{{#!hs\r\n{-# LANGUAGE TypeFamilies, TypeOperators, TypeInType #-}\r\n\r\nmodule GenWhoops where\r\nimport GHC.Generics\r\n\r\ntype family GenComp k (x :: k) (y :: k) :: Ordering where\r\n GenComp ((x :+: y) p) ('L1 x) ('L1 y) = GenComp (x p) x y\r\n}}}\r\n\r\nproduces the following panic:\r\n\r\n{{{\r\nghc-stage2: panic! (the 'impossible' happened)\r\n (GHC version 8.3.20170828 for x86_64-unknown-linux):\r\n piResultTy\r\n k_a1LK[tau:1]\r\n p_a1Lz[sk:1]\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1138:37 in ghc:Outputable\r\n pprPanic, called at compiler/types/Type.hs:949:35 in ghc:Type\r\n}}}\r\n\r\nThis happens with both GHC 8.2.1 and something very close to HEAD.","type_of_failure":"OtherFailure","blocking":[]} -->8.2.3https://gitlab.haskell.org/ghc/ghc/-/issues/14175Panic repSplitTyConApp_maybe2019-07-07T18:18:08ZDavid FeuerPanic repSplitTyConApp_maybeThis definition panics!
```hs
{-# LANGUAGE TypeFamilies, TypeInType #-}
module Whoops where
import Data.Kind
type family PComp (k :: j -> Type) (x :: k) :: ()
```
```
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.3....This definition panics!
```hs
{-# LANGUAGE TypeFamilies, TypeInType #-}
module Whoops where
import Data.Kind
type family PComp (k :: j -> Type) (x :: k) :: ()
```
```
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.3.20170828 for x86_64-unknown-linux):
repSplitTyConApp_maybe
j_aon[sk:1]
*
*
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1138:37 in ghc:Outputable
pprPanic, called at compiler/types/Type.hs:1123:5 in ghc:Type
```
If I make it a type synonym instead, I get a proper error as expected.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.2.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | goldfire |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Panic repSplitTyConApp_maybe","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.2.2","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":["goldfire"],"type":"Bug","description":"This definition panics!\r\n\r\n{{{#!hs\r\n{-# LANGUAGE TypeFamilies, TypeInType #-}\r\n\r\nmodule Whoops where\r\nimport Data.Kind\r\n\r\ntype family PComp (k :: j -> Type) (x :: k) :: ()\r\n}}}\r\n\r\n{{{\r\nghc-stage2: panic! (the 'impossible' happened)\r\n (GHC version 8.3.20170828 for x86_64-unknown-linux):\r\n repSplitTyConApp_maybe\r\n j_aon[sk:1]\r\n *\r\n *\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1138:37 in ghc:Outputable\r\n pprPanic, called at compiler/types/Type.hs:1123:5 in ghc:Type\r\n}}}\r\n\r\nIf I make it a type synonym instead, I get a proper error as expected.","type_of_failure":"OtherFailure","blocking":[]} -->8.2.2https://gitlab.haskell.org/ghc/ghc/-/issues/14203GHC-inferred type signature doesn't actually typecheck2019-07-07T18:17:58ZRyan ScottGHC-inferred type signature doesn't actually typecheckThis code typechecks:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Kind
data TyFun :: * -> * ->...This code typechecks:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Kind
data TyFun :: * -> * -> *
type a ~> b = TyFun a b -> *
infixr 0 ~>
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
data family Sing :: k -> *
data Sigma (a :: *) :: (a ~> *) -> * where
MkSigma :: forall (a :: *) (p :: a ~> *) (x :: a).
Sing x -> Apply p x -> Sigma a p
data instance Sing (z :: Sigma a p) where
SMkSigma :: Sing sx -> Sing px -> Sing (MkSigma sx px)
```
I was curious to know what the full type signature of `SMkSigma` was, so I asked GHCi what the inferred type is:
```
λ> :i SMkSigma
data instance Sing z where
SMkSigma :: forall a (p :: a ~> *) (x :: a) (sx :: Sing
x) (px :: Apply p x).
(Sing sx) -> (Sing px) -> Sing ('MkSigma sx px)
```
I attempted to incorporate this newfound knowledge into the program:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Kind
data TyFun :: * -> * -> *
type a ~> b = TyFun a b -> *
infixr 0 ~>
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
data family Sing :: k -> *
data Sigma (a :: *) :: (a ~> *) -> * where
MkSigma :: forall (a :: *) (p :: a ~> *) (x :: a).
Sing x -> Apply p x -> Sigma a p
data instance Sing (z :: Sigma a p) where
SMkSigma :: forall a (p :: a ~> *) (x :: a) (sx :: Sing x) (px :: Apply p x).
Sing sx -> Sing px -> Sing (MkSigma sx px)
```
But to my surprise, adding this inferred type signature causes the program to no longer typecheck!
```
GHCi, version 8.3.20170907: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:23:31: error:
• Expected kind ‘Apply p0 x’, but ‘px’ has kind ‘Apply p1 x’
• In the first argument of ‘Sing’, namely ‘px’
In the type ‘Sing px’
In the definition of data constructor ‘SMkSigma’
|
23 | Sing sx -> Sing px -> Sing (MkSigma sx px)
| ^^
```
I'm showing the output of GHC HEAD here, but this bug can be reproduced all the way back to GHC 8.0.1.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.2.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":"GHC-inferred type signature doesn't actually typecheck","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["TypeFamilies","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This code typechecks:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE ScopedTypeVariables #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# LANGUAGE TypeOperators #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ndata TyFun :: * -> * -> *\r\ntype a ~> b = TyFun a b -> *\r\ninfixr 0 ~>\r\n\r\ntype family Apply (f :: k1 ~> k2) (x :: k1) :: k2\r\ndata family Sing :: k -> *\r\n\r\ndata Sigma (a :: *) :: (a ~> *) -> * where\r\n MkSigma :: forall (a :: *) (p :: a ~> *) (x :: a).\r\n Sing x -> Apply p x -> Sigma a p\r\n\r\ndata instance Sing (z :: Sigma a p) where\r\n SMkSigma :: Sing sx -> Sing px -> Sing (MkSigma sx px)\r\n}}}\r\n\r\nI was curious to know what the full type signature of `SMkSigma` was, so I asked GHCi what the inferred type is:\r\n\r\n{{{\r\nλ> :i SMkSigma\r\ndata instance Sing z where\r\n SMkSigma :: forall a (p :: a ~> *) (x :: a) (sx :: Sing\r\n x) (px :: Apply p x).\r\n (Sing sx) -> (Sing px) -> Sing ('MkSigma sx px)\r\n}}}\r\n\r\nI attempted to incorporate this newfound knowledge into the program:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE ScopedTypeVariables #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# LANGUAGE TypeOperators #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ndata TyFun :: * -> * -> *\r\ntype a ~> b = TyFun a b -> *\r\ninfixr 0 ~>\r\n\r\ntype family Apply (f :: k1 ~> k2) (x :: k1) :: k2\r\ndata family Sing :: k -> *\r\n\r\ndata Sigma (a :: *) :: (a ~> *) -> * where\r\n MkSigma :: forall (a :: *) (p :: a ~> *) (x :: a).\r\n Sing x -> Apply p x -> Sigma a p\r\n\r\ndata instance Sing (z :: Sigma a p) where\r\n SMkSigma :: forall a (p :: a ~> *) (x :: a) (sx :: Sing x) (px :: Apply p x).\r\n Sing sx -> Sing px -> Sing (MkSigma sx px)\r\n}}}\r\n\r\nBut to my surprise, adding this inferred type signature causes the program to no longer typecheck!\r\n\r\n{{{\r\nGHCi, version 8.3.20170907: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\n\r\nBug.hs:23:31: error:\r\n • Expected kind ‘Apply p0 x’, but ‘px’ has kind ‘Apply p1 x’\r\n • In the first argument of ‘Sing’, namely ‘px’\r\n In the type ‘Sing px’\r\n In the definition of data constructor ‘SMkSigma’\r\n |\r\n23 | Sing sx -> Sing px -> Sing (MkSigma sx px)\r\n | ^^\r\n}}}\r\n\r\nI'm showing the output of GHC HEAD here, but this bug can be reproduced all the way back to GHC 8.0.1.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/14209GHC 8.2.1 regression involving telescoping kind signature2019-07-07T18:17:56ZRyan ScottGHC 8.2.1 regression involving telescoping kind signatureThe following program typechecks in GHC 8.0.1 and 8.0.2:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeInType #-}
module Bug where
data MyProxy k (a :: k) = MyProxy
data Foo (z :: MyProxy k (a :: k))
```
But in GHC 8.2.1, it's rejecte...The following program typechecks in GHC 8.0.1 and 8.0.2:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeInType #-}
module Bug where
data MyProxy k (a :: k) = MyProxy
data Foo (z :: MyProxy k (a :: k))
```
But in GHC 8.2.1, it's rejected:
```
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:6:1: error:
Kind variable ‘k’ is implicitly bound in datatype
‘Foo’, but does not appear as the kind of any
of its type variables. Perhaps you meant
to bind it explicitly somewhere?
Type variables with inferred kinds:
(k :: *) (a :: k) (z :: MyProxy k a)
|
6 | data Foo (z :: MyProxy k (a :: k))
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.2.1 |
| 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":"GHC 8.2.1 regression involving telescoping kind signature","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.2.2","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program typechecks in GHC 8.0.1 and 8.0.2:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE TypeInType #-}\r\nmodule Bug where\r\n\r\ndata MyProxy k (a :: k) = MyProxy\r\ndata Foo (z :: MyProxy k (a :: k))\r\n}}}\r\n\r\nBut in GHC 8.2.1, it's rejected:\r\n\r\n{{{\r\nGHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\n\r\nBug.hs:6:1: error:\r\n Kind variable ‘k’ is implicitly bound in datatype\r\n ‘Foo’, but does not appear as the kind of any\r\n of its type variables. Perhaps you meant\r\n to bind it explicitly somewhere?\r\n Type variables with inferred kinds:\r\n (k :: *) (a :: k) (z :: MyProxy k a)\r\n |\r\n6 | data Foo (z :: MyProxy k (a :: k))\r\n | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.4.1https://gitlab.haskell.org/ghc/ghc/-/issues/14230Gruesome kind mismatch errors for associated data family instances2019-07-07T18:17:51ZRyan ScottGruesome kind mismatch errors for associated data family instancesSpun off from #14175\##14230. This program, which can only really be compiled on GHC HEAD at the moment:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where
...Spun off from #14175\##14230. This program, which can only really be compiled on GHC HEAD at the moment:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where
class C k where
data CD :: k -> k -> *
instance C (Maybe a) where
data CD :: (k -> *) -> (k -> *) -> *
```
Gives a heinous error message:
```
Bug.hs:11:3: error:
• Expected kind ‘(k -> *) -> (k -> *) -> *’,
but ‘CD :: (k -> *) -> (k -> *) -> *’ has kind ‘Maybe a
-> Maybe a -> *’
• In the data instance declaration for ‘CD’
In the instance declaration for ‘C (Maybe a)’
|
11 | data CD :: (k -> *) -> (k -> *) -> *
| ^^^^^^^
```
- We shouldn't be expecting kind `(k -> *) -> (k -> *) -> *`, but rather kind `Maybe a -> Maybe a -> *`, due to the instance head itself.
- The phrase `‘CD :: (k -> *) -> (k -> *) -> *’ has kind ‘Maybe -> Maybe a -> *’` is similarly confusing. This doesn't point out that the real issue is the use of `(k -> *)`.
Another program in a similar vein:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
class C a where
data CD k (a :: k) :: k -> *
instance C (Maybe a) where
data CD k (a :: k -> *) :: (k -> *) -> *
```
```
Bug.hs:13:3: error:
• Expected kind ‘(k -> *) -> *’,
but ‘CD k (a :: k -> *) :: (k -> *) -> *’ has kind ‘k -> *’
• In the data instance declaration for ‘CD’
In the instance declaration for ‘C (Maybe a)’
|
13 | data CD k (a :: k -> *) :: (k -> *) -> *
| ^^^^^^^^^^^^^^^^^^^^^^^
```
This error message is further muddled by the incorrect use of `k` as the first type pattern (instead of `k -> *`, as subsequent kind signatures would suggest).
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.3 |
| 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":"Gruesome kind mismatch errors for associated data family instances","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.3","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Spun off from https://ghc.haskell.org/trac/ghc/ticket/14175#comment:9. This program, which can only really be compiled on GHC HEAD at the moment:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE PolyKinds #-}\r\n{-# LANGUAGE RankNTypes #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\nmodule Bug where\r\n\r\nclass C k where\r\n data CD :: k -> k -> *\r\n\r\ninstance C (Maybe a) where\r\n data CD :: (k -> *) -> (k -> *) -> *\r\n}}}\r\n\r\nGives a heinous error message:\r\n\r\n{{{\r\nBug.hs:11:3: error:\r\n • Expected kind ‘(k -> *) -> (k -> *) -> *’,\r\n but ‘CD :: (k -> *) -> (k -> *) -> *’ has kind ‘Maybe a\r\n -> Maybe a -> *’\r\n • In the data instance declaration for ‘CD’\r\n In the instance declaration for ‘C (Maybe a)’\r\n |\r\n11 | data CD :: (k -> *) -> (k -> *) -> *\r\n | ^^^^^^^\r\n}}}\r\n\r\n* We shouldn't be expecting kind `(k -> *) -> (k -> *) -> *`, but rather kind `Maybe a -> Maybe a -> *`, due to the instance head itself.\r\n* The phrase `‘CD :: (k -> *) -> (k -> *) -> *’ has kind ‘Maybe -> Maybe a -> *’` is similarly confusing. This doesn't point out that the real issue is the use of `(k -> *)`.\r\n\r\nAnother program in a similar vein:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE RankNTypes #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\nclass C a where\r\n data CD k (a :: k) :: k -> *\r\n\r\ninstance C (Maybe a) where\r\n data CD k (a :: k -> *) :: (k -> *) -> *\r\n}}}\r\n{{{\r\nBug.hs:13:3: error:\r\n • Expected kind ‘(k -> *) -> *’,\r\n but ‘CD k (a :: k -> *) :: (k -> *) -> *’ has kind ‘k -> *’\r\n • In the data instance declaration for ‘CD’\r\n In the instance declaration for ‘C (Maybe a)’\r\n |\r\n13 | data CD k (a :: k -> *) :: (k -> *) -> *\r\n | ^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nThis error message is further muddled by the incorrect use of `k` as the first type pattern (instead of `k -> *`, as subsequent kind signatures would suggest).","type_of_failure":"OtherFailure","blocking":[]} -->8.8.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/14238`:kind` suppresses visible dependent quantifiers by default in GHCi 8.2.12019-07-07T18:17:49ZRyan Scott`:kind` suppresses visible dependent quantifiers by default in GHCi 8.2.1Load this program into GHCi on 8.2.1 or later:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeInType #-}
import Data.Kind
data Foo (k :: Type) :: k -> Type where
MkFoo :: Foo (k1 -> k2) f -> Foo k1 a -> Foo k2 (f a)
```
And ask it w...Load this program into GHCi on 8.2.1 or later:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeInType #-}
import Data.Kind
data Foo (k :: Type) :: k -> Type where
MkFoo :: Foo (k1 -> k2) f -> Foo k1 a -> Foo k2 (f a)
```
And ask it what the kind of `Foo` is:
```
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main ( Bug.hs, interpreted )
Ok, 1 module loaded.
λ> :k Foo
Foo :: k -> *
```
This is just plain wrong: the actual kind of `Foo` should be `forall k -> k -> *`. Normally, one can omit `forall`s from a kind signature, but this is a special case where we're using a //visible// forall. In other words, `forall k -> k -> *` is not the same as `k -> *`, as the former takes two arguments, whereas the latter takes one.
A workaround is to force GHCi to come to its senses by explicitly enabling `-fprint-explicit-foralls`:
```
λ> :set -fprint-explicit-foralls
λ> :k Foo
Foo :: forall k -> k -> *
```
This is actually a regression since GHC 8.0.2, since GHCi did the right thing by default then:
```
GHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main ( Bug.hs, interpreted )
Ok, modules loaded: Main.
λ> :k Foo
Foo :: forall k -> k -> Type
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.2.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":"`:kind` suppresses visible dependent quantifiers by default in GHCi 8.2.1","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Load this program into GHCi on 8.2.1 or later:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE TypeInType #-}\r\n\r\nimport Data.Kind\r\n\r\ndata Foo (k :: Type) :: k -> Type where\r\n MkFoo :: Foo (k1 -> k2) f -> Foo k1 a -> Foo k2 (f a)\r\n}}}\r\n\r\nAnd ask it what the kind of `Foo` is:\r\n\r\n{{{\r\nGHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Main ( Bug.hs, interpreted )\r\nOk, 1 module loaded.\r\nλ> :k Foo\r\nFoo :: k -> *\r\n}}}\r\n\r\nThis is just plain wrong: the actual kind of `Foo` should be `forall k -> k -> *`. Normally, one can omit `forall`s from a kind signature, but this is a special case where we're using a //visible// forall. In other words, `forall k -> k -> *` is not the same as `k -> *`, as the former takes two arguments, whereas the latter takes one.\r\n\r\nA workaround is to force GHCi to come to its senses by explicitly enabling `-fprint-explicit-foralls`:\r\n\r\n{{{\r\nλ> :set -fprint-explicit-foralls \r\nλ> :k Foo\r\nFoo :: forall k -> k -> *\r\n}}}\r\n\r\nThis is actually a regression since GHC 8.0.2, since GHCi did the right thing by default then:\r\n\r\n{{{\r\nGHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Main ( Bug.hs, interpreted )\r\nOk, modules loaded: Main.\r\nλ> :k Foo\r\nFoo :: forall k -> k -> Type\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/14350Infinite loop when typechecking incorrect implementation (GHC HEAD only)2019-07-07T18:17:22ZRyan ScottInfinite loop when typechecking incorrect implementation (GHC HEAD only)On GHC HEAD, typechecking this program loops infinitely:
```hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ...On GHC HEAD, typechecking this program loops infinitely:
```hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Kind
data Proxy a = Proxy
data family Sing (a :: k)
data SomeSing k where
SomeSing :: Sing (a :: k) -> SomeSing k
class SingKind k where
type Demote k :: Type
fromSing :: Sing (a :: k) -> Demote k
toSing :: Demote k -> SomeSing k
data instance Sing (x :: Proxy k) where
SProxy :: Sing 'Proxy
instance SingKind (Proxy k) where
type Demote (Proxy k) = Proxy k
fromSing SProxy = Proxy
toSing Proxy = SomeSing SProxy
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 @@
newtype instance Sing (f :: k1 ~> k2) =
SLambda { applySing :: forall t. Sing t -> Sing (f @@ t) }
instance (SingKind k1, SingKind k2) => SingKind (k1 ~> k2) where
type Demote (k1 ~> k2) = Demote k1 -> Demote k2
fromSing sFun x = case toSing x of SomeSing y -> fromSing (applySing sFun y)
toSing = undefined
dcomp :: forall (a :: Type)
(b :: a ~> Type)
(c :: forall (x :: a). Proxy x ~> b @@ x ~> Type)
(f :: forall (x :: a) (y :: b @@ x). Proxy x ~> Proxy y ~> c @@ ('Proxy :: Proxy x) @@ y)
(g :: forall (x :: a). Proxy x ~> b @@ x)
(x :: a).
Sing f
-> Sing g
-> Sing x
-> c @@ ('Proxy :: Proxy x) @@ (g @@ ('Proxy :: Proxy x))
dcomp f g x = applySing f Proxy Proxy
```
This is a regression from GHC 8.2.1/8.2.2, where it gives a proper error message:
```
$ /opt/ghc/8.2.1/bin/ghci Bug.hs
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:59:15: error:
• Couldn't match expected type ‘Proxy a2
-> Apply (Apply (c x4) 'Proxy) (Apply (g x4) 'Proxy)’
with actual type ‘Sing (f x y @@ t0)’
• The function ‘applySing’ is applied to three arguments,
but its type ‘Sing (f x y) -> Sing t0 -> Sing (f x y @@ t0)’
has only two
In the expression: applySing f Proxy Proxy
In an equation for ‘dcomp’: dcomp f g x = applySing f Proxy Proxy
• Relevant bindings include
x :: Sing x4 (bound at Bug.hs:59:11)
g :: Sing (g x3) (bound at Bug.hs:59:9)
f :: Sing (f x2 y) (bound at Bug.hs:59:7)
dcomp :: Sing (f x2 y)
-> Sing (g x3) -> Sing x4 -> (c x4 @@ 'Proxy) @@ (g x4 @@ 'Proxy)
(bound at Bug.hs:59:1)
|
59 | dcomp f g x = applySing f Proxy Proxy
| ^^^^^^^^^^^^^^^^^^^^^^^
Bug.hs:59:27: error:
• Couldn't match expected type ‘Sing t0’
with actual type ‘Proxy a0’
• In the second argument of ‘applySing’, namely ‘Proxy’
In the expression: applySing f Proxy Proxy
In an equation for ‘dcomp’: dcomp f g x = applySing f Proxy Proxy
• Relevant bindings include
x :: Sing x4 (bound at Bug.hs:59:11)
g :: Sing (g x3) (bound at Bug.hs:59:9)
f :: Sing (f x2 y) (bound at Bug.hs:59:7)
dcomp :: Sing (f x2 y)
-> Sing (g x3) -> Sing x4 -> (c x4 @@ 'Proxy) @@ (g x4 @@ 'Proxy)
(bound at Bug.hs:59:1)
|
59 | dcomp f g x = applySing f Proxy Proxy
| ^^^^^
```8.4.1https://gitlab.haskell.org/ghc/ghc/-/issues/14352Higher-rank kind ascription oddities2019-07-07T18:17:21ZRyan ScottHigher-rank kind ascription odditiesGHC accepts these two definitions:
```hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Proxy
f :: forall (x :: forall a. a -> Int). Proxy x
f = Proxy
g :: forall (x :: forall a. a -> Int). Proxy...GHC accepts these two definitions:
```hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Proxy
f :: forall (x :: forall a. a -> Int). Proxy x
f = Proxy
g :: forall (x :: forall a. a -> Int). Proxy (x :: forall b. b -> Int)
g = Proxy
```
However, it does not accept this one, which (AFAICT) should be equivalent to the two above:
```hs
h :: forall x. Proxy (x :: forall b. b -> Int)
h = Proxy
```
```
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:13:23: error:
• Expected kind ‘forall b. b -> Int’, but ‘x’ has kind ‘k0’
• In the first argument of ‘Proxy’, namely
‘(x :: forall b. b -> Int)’
In the type signature:
h :: forall x. Proxy (x :: forall b. b -> Int)
|
13 | h :: forall x. Proxy (x :: forall b. b -> Int)
| ^
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.2.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":"Higher-rank kind ascription oddities","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"GHC accepts these two definitions:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE RankNTypes #-}\r\n{-# LANGUAGE TypeInType #-}\r\nmodule Bug where\r\n\r\nimport Data.Proxy\r\n\r\nf :: forall (x :: forall a. a -> Int). Proxy x\r\nf = Proxy\r\n\r\ng :: forall (x :: forall a. a -> Int). Proxy (x :: forall b. b -> Int)\r\ng = Proxy\r\n}}}\r\n\r\nHowever, it does not accept this one, which (AFAICT) should be equivalent to the two above:\r\n\r\n{{{#!hs\r\nh :: forall x. Proxy (x :: forall b. b -> Int)\r\nh = Proxy\r\n}}}\r\n\r\n{{{\r\nGHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\n\r\nBug.hs:13:23: error:\r\n • Expected kind ‘forall b. b -> Int’, but ‘x’ has kind ‘k0’\r\n • In the first argument of ‘Proxy’, namely\r\n ‘(x :: forall b. b -> Int)’\r\n In the type signature:\r\n h :: forall x. Proxy (x :: forall b. b -> Int)\r\n |\r\n13 | h :: forall x. Proxy (x :: forall b. b -> Int)\r\n | ^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/14366Type family equation refuses to unify wildcard type patterns2019-07-07T18:17:18ZRyan ScottType family equation refuses to unify wildcard type patternsThis typechecks:
```hs
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
import Data.Kind
import Data.Type.Equality
type family Cast (e :: a :~: b) (x :: a) :: b where
Cast Refl x = x
```
Howe...This typechecks:
```hs
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
import Data.Kind
import Data.Type.Equality
type family Cast (e :: a :~: b) (x :: a) :: b where
Cast Refl x = x
```
However, if you try to make the kinds `a` and `b` explicit arguments to `Cast`:
```hs
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
import Data.Kind
import Data.Type.Equality
type family Cast (a :: Type) (b :: Type) (e :: a :~: b) (x :: a) :: b where
Cast _ _ Refl x = x
```
Then GHC gets confused:
```
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/ryanglscott/.ghci
[1 of 1] Compiling Main ( Bug.hs, interpreted )
Bug.hs:9:12: error:
• Expected kind ‘_ :~: _1’, but ‘'Refl’ has kind ‘_ :~: _’
• In the third argument of ‘Cast’, namely ‘Refl’
In the type family declaration for ‘Cast’
|
9 | Cast _ _ Refl x = x
| ^^^^
```
A workaround is to explicitly write out what should be inferred by the underscores:
```hs
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
import Data.Kind
import Data.Type.Equality
type family Cast (a :: Type) (b :: Type) (e :: a :~: b) (x :: a) :: b where
Cast a a Refl x = x
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.2.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":"Type family equation refuses to unify wildcard type patterns","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["TypeFamilies,","TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This typechecks:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# LANGUAGE TypeOperators #-}\r\n\r\nimport Data.Kind\r\nimport Data.Type.Equality\r\n\r\ntype family Cast (e :: a :~: b) (x :: a) :: b where\r\n Cast Refl x = x\r\n}}}\r\n\r\nHowever, if you try to make the kinds `a` and `b` explicit arguments to `Cast`:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# LANGUAGE TypeOperators #-}\r\n\r\nimport Data.Kind\r\nimport Data.Type.Equality\r\n\r\ntype family Cast (a :: Type) (b :: Type) (e :: a :~: b) (x :: a) :: b where\r\n Cast _ _ Refl x = x\r\n}}}\r\n\r\nThen GHC gets confused:\r\n\r\n{{{\r\nGHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/ryanglscott/.ghci\r\n[1 of 1] Compiling Main ( Bug.hs, interpreted )\r\n\r\nBug.hs:9:12: error:\r\n • Expected kind ‘_ :~: _1’, but ‘'Refl’ has kind ‘_ :~: _’\r\n • In the third argument of ‘Cast’, namely ‘Refl’\r\n In the type family declaration for ‘Cast’\r\n |\r\n9 | Cast _ _ Refl x = x\r\n | ^^^^\r\n}}}\r\n\r\nA workaround is to explicitly write out what should be inferred by the underscores:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# LANGUAGE TypeOperators #-}\r\n\r\nimport Data.Kind\r\nimport Data.Type.Equality\r\n\r\ntype family Cast (a :: Type) (b :: Type) (e :: a :~: b) (x :: a) :: b where\r\n Cast a a Refl x = x\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.8.1https://gitlab.haskell.org/ghc/ghc/-/issues/14394Inferred type for pattern synonym has redundant equality constraint2019-07-07T18:17:11ZRyan ScottInferred type for pattern synonym has redundant equality constraintLoad this file into GHCi:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
module Bug where
import Data.Type.Equality
pattern Foo = HRefl
```
```
$ /opt/ghc/8.2.1/bin/ghci Bug.hs
GHCi, version 8.2.1: http://www.haskell.o...Load this file into GHCi:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
module Bug where
import Data.Type.Equality
pattern Foo = HRefl
```
```
$ /opt/ghc/8.2.1/bin/ghci Bug.hs
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Ok, 1 module loaded.
λ> :i Foo
pattern Foo :: () => (* ~ *, b ~ a) => a :~~: b
```
Notice that the type signature for `Foo` has an entirely redundant `* ~ *` constraint. The same does not happen if `TypeInType` is enabled.
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TypeInType #-}
module Works where
import Data.Type.Equality
pattern Foo = HRefl
```
```
λ> :i Foo
pattern Foo :: forall k2 k1 (a :: k1) (b :: k2). () => (k2 ~ k1,
(b :: k2) ~~ (a :: k1)) => a :~~: b
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.2.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":"Inferred type for pattern synonym has redundant equality constraint","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["PatternSynonyms,","TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Load this file into GHCi:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE PatternSynonyms #-}\r\nmodule Bug where\r\n\r\nimport Data.Type.Equality\r\n\r\npattern Foo = HRefl\r\n}}}\r\n{{{\r\n$ /opt/ghc/8.2.1/bin/ghci Bug.hs\r\nGHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\nOk, 1 module loaded.\r\nλ> :i Foo\r\npattern Foo :: () => (* ~ *, b ~ a) => a :~~: b\r\n}}}\r\n\r\nNotice that the type signature for `Foo` has an entirely redundant `* ~ *` constraint. The same does not happen if `TypeInType` is enabled.\r\n\r\n{{{#!hs\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE PatternSynonyms #-}\r\n{-# LANGUAGE TypeInType #-}\r\nmodule Works where\r\n\r\nimport Data.Type.Equality\r\n\r\npattern Foo = HRefl\r\n}}}\r\n{{{\r\nλ> :i Foo\r\npattern Foo :: forall k2 k1 (a :: k1) (b :: k2). () => (k2 ~ k1,\r\n (b :: k2) ~~ (a :: k1)) => a :~~: b\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->