GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2019-07-07T18:19:32Zhttps://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/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/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/13872Strange Typeable error message involving TypeInType2019-07-07T18:19:44ZRyan ScottStrange Typeable error message involving TypeInTypeI originally discovered this when tinkering with #13871. This program:
```hs
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Foo whe...I originally discovered this when tinkering with #13871. This program:
```hs
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Foo where
import Data.Kind
import Data.Typeable
data Foo (a :: Type) (b :: Type) where
MkFoo :: (a ~ Int, b ~ Char) => Foo a b
data family Sing (a :: k)
data SFoo (z :: Foo a b) where
SMkFoo :: SFoo MkFoo
f :: String
f = show $ typeOf SMkFoo
```
Fails in GHC 8.0.1, 8.0.2, and 8.2 (after applying [D3671](https://phabricator.haskell.org/D3671)) with a rather unsightly error message:
```
GHCi, version 8.3.20170624: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Foo ( Foo.hs, interpreted )
Foo.hs:19:12: error:
• No instance for (Typeable <>) arising from a use of ‘typeOf’
• In the second argument of ‘($)’, namely ‘typeOf SMkFoo’
In the expression: show $ typeOf SMkFoo
In an equation for ‘f’: f = show $ typeOf SMkFoo
|
19 | f = show $ typeOf SMkFoo
| ^^^^^^^^^^^^^
```
I'm not sure what this mysterious `<>` is, but I'm pretty sure it shouldn't be making an appearance here. (See also #13780, where `<>` also makes a surprise guest appearance.)
<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 Typeable error message involving TypeInType","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["TypeInType,","Typeable"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I originally discovered this when tinkering with #13871. This program:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE ConstraintKinds #-}\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# LANGUAGE TypeOperators #-}\r\nmodule Foo where\r\n\r\nimport Data.Kind\r\nimport Data.Typeable\r\n\r\ndata Foo (a :: Type) (b :: Type) where\r\n MkFoo :: (a ~ Int, b ~ Char) => Foo a b\r\n\r\ndata family Sing (a :: k)\r\ndata SFoo (z :: Foo a b) where\r\n SMkFoo :: SFoo MkFoo\r\n\r\nf :: String\r\nf = show $ typeOf SMkFoo\r\n}}}\r\n\r\nFails in GHC 8.0.1, 8.0.2, and 8.2 (after applying Phab:D3671) with a rather unsightly error message:\r\n\r\n{{{\r\nGHCi, version 8.3.20170624: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Foo ( Foo.hs, interpreted )\r\n\r\nFoo.hs:19:12: error:\r\n • No instance for (Typeable <>) arising from a use of ‘typeOf’\r\n • In the second argument of ‘($)’, namely ‘typeOf SMkFoo’\r\n In the expression: show $ typeOf SMkFoo\r\n In an equation for ‘f’: f = show $ typeOf SMkFoo\r\n |\r\n19 | f = show $ typeOf SMkFoo\r\n | ^^^^^^^^^^^^^\r\n}}}\r\n\r\nI'm not sure what this mysterious `<>` is, but I'm pretty sure it shouldn't be making an appearance here. (See also #13780, where `<>` also makes a surprise guest appearance.)","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/13871GHC panic in 8.2 only: typeIsTypeable(Coercion)2019-07-07T18:19:45ZRyan ScottGHC panic in 8.2 only: typeIsTypeable(Coercion)This code works fine in GHC 8.0.1 and 8.0.2:
```hs
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Foo where
import Data.Kind
data...This code works fine in GHC 8.0.1 and 8.0.2:
```hs
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Foo where
import Data.Kind
data Foo (a :: Type) (b :: Type) where
MkFoo :: (a ~ Int, b ~ Char) => Foo a b
data family Sing (a :: k)
data SFoo (z :: Foo a b) where
SMkFoo :: SFoo MkFoo
```
But in GHC 8.2 and HEAD, it panics:
```
$ /opt/ghc/8.2.1/bin/ghci Bug.hs
GHCi, version 8.2.0.20170622: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Foo ( Bug.hs, interpreted )
ghc: panic! (the 'impossible' happened)
(GHC version 8.2.0.20170622 for x86_64-unknown-linux):
typeIsTypeable(Coercion)
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.2.1-rc2 |
| 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 panic in 8.2 only: typeIsTypeable(Coercion)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.2.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1-rc2","keywords":["TypeInType,","Typeable"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This code works fine in GHC 8.0.1 and 8.0.2:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE ConstraintKinds #-}\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# LANGUAGE TypeOperators #-}\r\nmodule Foo where\r\n\r\nimport Data.Kind\r\n\r\ndata Foo (a :: Type) (b :: Type) where\r\n MkFoo :: (a ~ Int, b ~ Char) => Foo a b\r\n\r\ndata family Sing (a :: k)\r\ndata SFoo (z :: Foo a b) where\r\n SMkFoo :: SFoo MkFoo\r\n}}}\r\n\r\nBut in GHC 8.2 and HEAD, it panics:\r\n\r\n{{{\r\n$ /opt/ghc/8.2.1/bin/ghci Bug.hs\r\nGHCi, version 8.2.0.20170622: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Foo ( Bug.hs, interpreted )\r\nghc: panic! (the 'impossible' happened)\r\n (GHC version 8.2.0.20170622 for x86_64-unknown-linux):\r\n\ttypeIsTypeable(Coercion)\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.2.1Ben GamariBen Gamarihttps://gitlab.haskell.org/ghc/ghc/-/issues/13822GHC not using injectivity?2019-07-07T18:19:56ZIcelandjackGHC not using injectivity?This may be normal behavior but.. (Example from [System FC with Explicit Kind Equality](http://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1014&context=compsci_pubs))
```hs
{-# LANGUAGE GADTs, TypeOperators, PolyKinds, DataKinds...This may be normal behavior but.. (Example from [System FC with Explicit Kind Equality](http://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1014&context=compsci_pubs))
```hs
{-# LANGUAGE GADTs, TypeOperators, PolyKinds, DataKinds, TypeFamilyDependencies, TypeInType, RankNTypes, LambdaCase, EmptyCase #-}
import Data.Kind
data KIND = STAR | KIND :> KIND
data Ty :: KIND -> Type where
TInt :: Ty STAR
TBool :: Ty STAR
TMaybe :: Ty (STAR :> STAR)
TApp :: Ty (a :> b) -> (Ty a -> Ty b)
type family
IK (k :: KIND) = (res :: Type) | res -> k where
IK STAR = Type
IK (a:>b) = IK a -> IK b
type family
I (t :: Ty k) = (res :: IK k) | res -> t where
I TInt = Int
I TBool = Bool
I TMaybe = Maybe
I (TApp f a) = (I f) (I a)
data TyRep (k :: KIND) (t :: Ty k) where
TyInt :: TyRep STAR TInt
TyBool :: TyRep STAR TBool
TyMaybe :: TyRep (STAR:>STAR) TMaybe
TyApp :: TyRep (a:>b) f -> TyRep a x -> TyRep b (TApp f x)
zero :: TyRep STAR a -> I a
zero = \case
TyInt -> 0
TyBool -> False
TyApp TyMaybe _ -> Nothing
```
When I ask it to infer the representation for `Int` and `Bool` it does so with no surprises
```hs
-- Inferred type:
--
-- int :: TyRep STAR TInt -> Int
int rep = zero rep :: Int
-- bool:: TyRep STAR TBool -> Bool
bool rep = zero rep :: Bool
```
but inferring the representation for `Maybe Int` fails
```hs
-- v.hs:43:16: error:
-- • Couldn't match kind ‘k’ with ‘'STAR’
-- ‘k’ is a rigid type variable bound by
-- the inferred type of
-- maybeInt :: (I 'TInt ~ Int, I 'TMaybe ~ Maybe) =>
-- TyRep 'STAR ('TApp 'TMaybe 'TInt) -> Maybe Int
-- at v.hs:25:3
-- When matching the kind of ‘'TMaybe’
-- Expected type: Maybe Int
-- Actual type: I ('TApp 'TMaybe 'TInt)
-- • In the expression: zero rep :: Maybe Int
-- In an equation for ‘maybeInt’: maybeInt rep = zero rep :: Maybe Int
-- • Relevant bindings include
-- rep :: TyRep 'STAR ('TApp 'TMaybe 'TInt) (bound at v.hs:43:10)
-- maybeInt :: TyRep 'STAR ('TApp 'TMaybe 'TInt) -> Maybe Int
-- (bound at v.hs:43:1)
-- Failed, modules loaded: none.
maybeInt rep = zero rep :: Maybe Int
```
even though `I` is injective and GHC knows that `I (TMaybe `TApp` TMaybe) = Maybe Int`
```
>>> :kind! I (TMaybe `TApp` TInt)
I (TMaybe `TApp` TInt) :: IK 'STAR
= Maybe Int
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.0.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC not using injectivity?","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["InjectiveFamilies,","TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This may be normal behavior but.. (Example from [http://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1014&context=compsci_pubs System FC with Explicit Kind Equality])\r\n\r\n{{{#!hs\r\n{-# LANGUAGE GADTs, TypeOperators, PolyKinds, DataKinds, TypeFamilyDependencies, TypeInType, RankNTypes, LambdaCase, EmptyCase #-}\r\n\r\nimport Data.Kind\r\n\r\ndata KIND = STAR | KIND :> KIND\r\n\r\ndata Ty :: KIND -> Type where\r\n TInt :: Ty STAR\r\n TBool :: Ty STAR\r\n TMaybe :: Ty (STAR :> STAR)\r\n TApp :: Ty (a :> b) -> (Ty a -> Ty b)\r\n\r\ntype family\r\n IK (k :: KIND) = (res :: Type) | res -> k where\r\n IK STAR = Type\r\n IK (a:>b) = IK a -> IK b\r\n\r\ntype family\r\n I (t :: Ty k) = (res :: IK k) | res -> t where\r\n I TInt = Int\r\n I TBool = Bool\r\n I TMaybe = Maybe\r\n I (TApp f a) = (I f) (I a)\r\n\r\ndata TyRep (k :: KIND) (t :: Ty k) where\r\n TyInt :: TyRep STAR TInt\r\n TyBool :: TyRep STAR TBool\r\n TyMaybe :: TyRep (STAR:>STAR) TMaybe\r\n TyApp :: TyRep (a:>b) f -> TyRep a x -> TyRep b (TApp f x)\r\n\r\nzero :: TyRep STAR a -> I a\r\nzero = \\case\r\n TyInt -> 0\r\n TyBool -> False\r\n TyApp TyMaybe _ -> Nothing\r\n}}}\r\n\r\nWhen I ask it to infer the representation for `Int` and `Bool` it does so with no surprises\r\n\r\n{{{#!hs\r\n-- Inferred type: \r\n-- \r\n-- int :: TyRep STAR TInt -> Int\r\nint rep = zero rep :: Int\r\n\r\n\r\n-- bool:: TyRep STAR TBool -> Bool\r\nbool rep = zero rep :: Bool\r\n}}}\r\n\r\nbut inferring the representation for `Maybe Int` fails\r\n\r\n{{{#!hs\r\n-- v.hs:43:16: error:\r\n-- • Couldn't match kind ‘k’ with ‘'STAR’\r\n-- ‘k’ is a rigid type variable bound by\r\n-- the inferred type of\r\n-- maybeInt :: (I 'TInt ~ Int, I 'TMaybe ~ Maybe) =>\r\n-- TyRep 'STAR ('TApp 'TMaybe 'TInt) -> Maybe Int\r\n-- at v.hs:25:3\r\n-- When matching the kind of ‘'TMaybe’\r\n-- Expected type: Maybe Int\r\n-- Actual type: I ('TApp 'TMaybe 'TInt)\r\n-- • In the expression: zero rep :: Maybe Int\r\n-- In an equation for ‘maybeInt’: maybeInt rep = zero rep :: Maybe Int\r\n-- • Relevant bindings include\r\n-- rep :: TyRep 'STAR ('TApp 'TMaybe 'TInt) (bound at v.hs:43:10)\r\n-- maybeInt :: TyRep 'STAR ('TApp 'TMaybe 'TInt) -> Maybe Int\r\n-- (bound at v.hs:43:1)\r\n-- Failed, modules loaded: none.\r\nmaybeInt rep = zero rep :: Maybe Int\r\n}}}\r\n\r\neven though `I` is injective and GHC knows that `I (TMaybe `TApp` TMaybe) = Maybe Int`\r\n\r\n{{{\r\n>>> :kind! I (TMaybe `TApp` TInt)\r\nI (TMaybe `TApp` TInt) :: IK 'STAR\r\n= Maybe Int\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.2.1https://gitlab.haskell.org/ghc/ghc/-/issues/13790GHC doesn't reduce type family in kind signature unless its arm is twisted2019-07-07T18:20:04ZRyan ScottGHC doesn't reduce type family in kind signature unless its arm is twistedHere's some code (inspired by Richard's musings [here](https://github.com/goldfirere/singletons/issues/150#issuecomment-306088297)) which typechecks with GHC 8.2.1 or HEAD:
```hs
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}...Here's some code (inspired by Richard's musings [here](https://github.com/goldfirere/singletons/issues/150#issuecomment-306088297)) which typechecks with GHC 8.2.1 or HEAD:
```hs
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
data family Sing (a :: k)
data SomeSing (k :: Type) where
SomeSing :: Sing (a :: k) -> SomeSing k
type family Promote k :: Type
class (Promote (Demote k) ~ k) => SingKind (k :: Type) where
type Demote k :: Type
fromSing :: Sing (a :: k) -> Demote k
toSing :: Demote k -> SomeSing k
type family DemoteX (a :: k) :: Demote k
type instance DemoteX (a :: Type) = Demote a
type instance Promote Type = Type
instance SingKind Type where
type Demote Type = Type
fromSing = error "fromSing Type"
toSing = error "toSing Type"
-----
data N = Z | S N
data instance Sing (z :: N) where
SZ :: Sing Z
SS :: Sing n -> Sing (S n)
type instance Promote N = N
instance SingKind N where
type Demote N = N
fromSing SZ = Z
fromSing (SS n) = S (fromSing n)
toSing Z = SomeSing SZ
toSing (S n) = case toSing n of
SomeSing sn -> SomeSing (SS sn)
```
Things get more interesting if you try to add this type instance at the end of this file:
```hs
type instance DemoteX (n :: N) = n
```
Now GHC will complain:
```
GHCi, version 8.2.0.20170522: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:49:34: error:
• Expected kind ‘Demote N’, but ‘n’ has kind ‘N’
• In the type ‘n’
In the type instance declaration for ‘DemoteX’
|
49 | type instance DemoteX (n :: N) = n
| ^
```
That error message smells funny, since we do have a type family instance that says `Demote N = N`! In fact, if you use Template Haskell to split up the declarations manually:
```hs
...
instance SingKind N where
type Demote N = N
fromSing SZ = Z
fromSing (SS n) = S (fromSing n)
toSing Z = SomeSing SZ
toSing (S n) = case toSing n of
SomeSing sn -> SomeSing (SS sn)
$(return [])
type instance DemoteX (n :: N) = n
```
Then the file typechecks without issue.
<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 doesn't reduce type family in kind signature unless its arm is twisted","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":"Here's some code (inspired by Richard's musings [https://github.com/goldfirere/singletons/issues/150#issuecomment-306088297 here]) which typechecks with GHC 8.2.1 or HEAD:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE FlexibleInstances #-}\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE TemplateHaskell #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ndata family Sing (a :: k)\r\n\r\ndata SomeSing (k :: Type) where\r\n SomeSing :: Sing (a :: k) -> SomeSing k\r\n\r\ntype family Promote k :: Type\r\n\r\nclass (Promote (Demote k) ~ k) => SingKind (k :: Type) where\r\n type Demote k :: Type\r\n fromSing :: Sing (a :: k) -> Demote k\r\n toSing :: Demote k -> SomeSing k\r\n\r\ntype family DemoteX (a :: k) :: Demote k\r\ntype instance DemoteX (a :: Type) = Demote a\r\n\r\ntype instance Promote Type = Type\r\n\r\ninstance SingKind Type where\r\n type Demote Type = Type\r\n fromSing = error \"fromSing Type\"\r\n toSing = error \"toSing Type\"\r\n\r\n-----\r\n\r\ndata N = Z | S N\r\n\r\ndata instance Sing (z :: N) where\r\n SZ :: Sing Z\r\n SS :: Sing n -> Sing (S n)\r\ntype instance Promote N = N\r\n\r\ninstance SingKind N where\r\n type Demote N = N\r\n fromSing SZ = Z\r\n fromSing (SS n) = S (fromSing n)\r\n toSing Z = SomeSing SZ\r\n toSing (S n) = case toSing n of\r\n SomeSing sn -> SomeSing (SS sn)\r\n}}}\r\n\r\nThings get more interesting if you try to add this type instance at the end of this file:\r\n\r\n{{{#!hs\r\ntype instance DemoteX (n :: N) = n\r\n}}}\r\n\r\nNow GHC will complain:\r\n\r\n{{{\r\nGHCi, version 8.2.0.20170522: 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:49:34: error:\r\n • Expected kind ‘Demote N’, but ‘n’ has kind ‘N’\r\n • In the type ‘n’\r\n In the type instance declaration for ‘DemoteX’\r\n |\r\n49 | type instance DemoteX (n :: N) = n\r\n | ^\r\n}}}\r\n\r\nThat error message smells funny, since we do have a type family instance that says `Demote N = N`! In fact, if you use Template Haskell to split up the declarations manually:\r\n\r\n{{{#!hs\r\n...\r\n\r\ninstance SingKind N where\r\n type Demote N = N\r\n fromSing SZ = Z\r\n fromSing (SS n) = S (fromSing n)\r\n toSing Z = SomeSing SZ\r\n toSing (S n) = case toSing n of\r\n SomeSing sn -> SomeSing (SS sn)\r\n$(return [])\r\ntype instance DemoteX (n :: N) = n\r\n}}}\r\n\r\nThen the file typechecks without issue.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/13781(a :: (k :: Type)) is too exotic for Template Haskell2019-07-07T18:20:06ZRyan Scott(a :: (k :: Type)) is too exotic for Template HaskellOn GHC 8.0.1 or later, GHC will choke on this code:
```hs
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
import Data.Proxy
$([d| f :: Proxy (a :: (k :: Type))
f = Proxy
|])
```...On GHC 8.0.1 or later, GHC will choke on this code:
```hs
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
import Data.Proxy
$([d| f :: Proxy (a :: (k :: Type))
f = Proxy
|])
```
```
GHCi, version 8.2.0.20170522: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:8:3: error:
Exotic form of kind not (yet) handled by Template Haskell
(k :: Type)
|
8 | $([d| f :: Proxy (a :: (k :: Type))
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
```
I don't think this would be too hard to support, though. I'll take a shot at fixing this.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ---------------- |
| Version | 8.0.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Template Haskell |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"(a :: (k :: Type)) is too exotic for Template Haskell","status":"New","operating_system":"","component":"Template Haskell","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"On GHC 8.0.1 or later, GHC will choke on this code:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE TemplateHaskell #-}\r\n{-# LANGUAGE TypeInType #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\nimport Data.Proxy\r\n\r\n$([d| f :: Proxy (a :: (k :: Type))\r\n f = Proxy\r\n |])\r\n}}}\r\n\r\n{{{\r\nGHCi, version 8.2.0.20170522: 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:8:3: error:\r\n Exotic form of kind not (yet) handled by Template Haskell\r\n (k :: Type)\r\n |\r\n8 | $([d| f :: Proxy (a :: (k :: Type))\r\n | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...\r\n}}}\r\n\r\nI don't think this would be too hard to support, though. I'll take a shot at fixing this.","type_of_failure":"OtherFailure","blocking":[]} -->8.4.1Ryan ScottRyan Scotthttps://gitlab.haskell.org/ghc/ghc/-/issues/13780Nightmarish pretty-printing of equality type in GHC 8.2 error message2019-07-07T18:20:06ZRyan ScottNightmarish pretty-printing of equality type in GHC 8.2 error messageI originally spotted this in #12102\##13780, but I happened to stumble upon it again recently in a separate context, so I though it deserved its own ticket. Here's some code which does not typecheck:
```hs
{-# LANGUAGE ExistentialQuanti...I originally spotted this in #12102\##13780, but I happened to stumble upon it again recently in a separate context, so I though it deserved its own ticket. Here's some code which does not typecheck:
```hs
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Foo where
data family Sing (a :: k)
data Foo a = a ~ Bool => MkFoo
data instance Sing (z :: Foo a) = (z ~ MkFoo) => SMkFoo
```
In GHC 8.0.1 and 8.0.2, the error message you'd get from this program was reasonable enough:
```
GHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Foo ( Bug.hs, interpreted )
Bug.hs:9:40: error:
• Expected kind ‘Foo a’, but ‘'MkFoo’ has kind ‘Foo Bool’
• In the second argument of ‘~’, namely ‘MkFoo’
In the definition of data constructor ‘SMkFoo’
In the data instance declaration for ‘Sing’
```
But in GHC 8.2.1 and HEAD, it's hair-raisingly bad:
```
GHCi, version 8.2.0.20170522: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Foo ( Bug.hs, interpreted )
Bug.hs:9:40: error:
• Expected kind ‘Foo a’,
but ‘'MkFoo
('Data.Type.Equality.C:~ ('GHC.Types.Eq# <>))’ has kind ‘Foo Bool’
• In the second argument of ‘~’, namely ‘MkFoo’
In the definition of data constructor ‘SMkFoo’
In the data instance declaration for ‘Sing’
|
9 | data instance Sing (z :: Foo a) = (z ~ MkFoo) => SMkFoo
| ^^^^^
```
- \*WAT.\*\*
<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":"Nightmarish pretty-printing of equality type in GHC 8.2 error message","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1-rc2","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I originally spotted this in https://ghc.haskell.org/trac/ghc/ticket/12102#comment:1, but I happened to stumble upon it again recently in a separate context, so I though it deserved its own ticket. Here's some code which does not typecheck:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE ExistentialQuantification #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\nmodule Foo where\r\n\r\ndata family Sing (a :: k)\r\n\r\ndata Foo a = a ~ Bool => MkFoo\r\ndata instance Sing (z :: Foo a) = (z ~ MkFoo) => SMkFoo\r\n}}}\r\n\r\nIn GHC 8.0.1 and 8.0.2, the error message you'd get from this program was reasonable enough:\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 Foo ( Bug.hs, interpreted )\r\n\r\nBug.hs:9:40: error:\r\n • Expected kind ‘Foo a’, but ‘'MkFoo’ has kind ‘Foo Bool’\r\n • In the second argument of ‘~’, namely ‘MkFoo’\r\n In the definition of data constructor ‘SMkFoo’\r\n In the data instance declaration for ‘Sing’\r\n}}}\r\n\r\nBut in GHC 8.2.1 and HEAD, it's hair-raisingly bad:\r\n\r\n{{{\r\nGHCi, version 8.2.0.20170522: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Foo ( Bug.hs, interpreted )\r\n\r\nBug.hs:9:40: error:\r\n • Expected kind ‘Foo a’,\r\n but ‘'MkFoo\r\n ('Data.Type.Equality.C:~ ('GHC.Types.Eq# <>))’ has kind ‘Foo Bool’\r\n • In the second argument of ‘~’, namely ‘MkFoo’\r\n In the definition of data constructor ‘SMkFoo’\r\n In the data instance declaration for ‘Sing’\r\n |\r\n9 | data instance Sing (z :: Foo a) = (z ~ MkFoo) => SMkFoo\r\n | ^^^^^\r\n}}}\r\n\r\n**WAT.**","type_of_failure":"OtherFailure","blocking":[]} -->8.4.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/13777Poor error message around CUSKs2019-07-07T18:20:07ZRichard Eisenbergrae@richarde.devPoor error message around CUSKsWhile typing up [ticket:13761\#comment:137502](https://gitlab.haskell.org//ghc/ghc/issues/13761#note_137502), I came across a poor error message around CUSKs.
```
data Proxy (a :: k) = P
data S :: forall k. Proxy k -> Type where
MkS :...While typing up [ticket:13761\#comment:137502](https://gitlab.haskell.org//ghc/ghc/issues/13761#note_137502), I came across a poor error message around CUSKs.
```
data Proxy (a :: k) = P
data S :: forall k. Proxy k -> Type where
MkS :: S (P :: Proxy Maybe)
```
produces
```
You have written a *complete user-suppled kind signature*,
but the following variable is undetermined: k0 :: *
Perhaps add a kind signature.
Inferred kinds of user-written variables:
```
That promised list of the kinds of user-written variables is empty. Either GHC should find something to print (like `k :: k0`, perhaps) or omit the header.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.2.1-rc2 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Poor error message around CUSKs","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1-rc2","keywords":["CUSKs","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"While typing up comment:7:ticket:13761, I came across a poor error message around CUSKs.\r\n\r\n{{{\r\ndata Proxy (a :: k) = P\r\ndata S :: forall k. Proxy k -> Type where\r\n MkS :: S (P :: Proxy Maybe)\r\n}}}\r\n\r\nproduces\r\n\r\n{{{\r\n You have written a *complete user-suppled kind signature*,\r\n but the following variable is undetermined: k0 :: *\r\n Perhaps add a kind signature.\r\n Inferred kinds of user-written variables:\r\n}}}\r\n\r\nThat promised list of the kinds of user-written variables is empty. Either GHC should find something to print (like `k :: k0`, perhaps) or omit the header.","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/13762TypeInType is not documented in the users' guide flag reference2019-07-07T18:20:12ZRyan ScottTypeInType is not documented in the users' guide flag referenceAt least, not as of http://git.haskell.org/ghc.git/blob/09d5c993aae208e3d34a9e715297922b6ea42b3f:/utils/mkUserGuidePart/Options/Language.hs. We should fix this.
<details><summary>Trac metadata</summary>
| Trac field | Value...At least, not as of http://git.haskell.org/ghc.git/blob/09d5c993aae208e3d34a9e715297922b6ea42b3f:/utils/mkUserGuidePart/Options/Language.hs. We should fix this.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------- |
| Version | 8.0.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Documentation |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"TypeInType is not documented in the users' guide flag reference","status":"New","operating_system":"","component":"Documentation","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"At least, not as of http://git.haskell.org/ghc.git/blob/09d5c993aae208e3d34a9e715297922b6ea42b3f:/utils/mkUserGuidePart/Options/Language.hs. We should fix this.","type_of_failure":"OtherFailure","blocking":[]} -->8.2.1https://gitlab.haskell.org/ghc/ghc/-/issues/13761Can't create poly-kinded GADT with TypeInType enabled, but can without2019-07-07T18:20:12ZRyan ScottCan't create poly-kinded GADT with TypeInType enabled, but can withoutSurprisingly, this compiles without `TypeInType`:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
module Works where
import Data.Kind
data T :: k -> Type where
MkT :...Surprisingly, this compiles without `TypeInType`:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
module Works where
import Data.Kind
data T :: k -> Type where
MkT :: T Int
```
But once you add `TypeInType`:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
data T :: k -> Type where
MkT :: T Int
```
then it stops working!
```
GHCi, version 8.3.20170516: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:11:12: error:
• Expected kind ‘k’, but ‘Int’ has kind ‘*’
• In the first argument of ‘T’, namely ‘Int’
In the type ‘T Int’
In the definition of data constructor ‘MkT’
|
11 | MkT :: T Int
| ^^^
```
This bug is present in GHC 8.0.1, 8.0.2, 8.2.1, and HEAD.
What's strange about this bug is that is requires that you write `T` with an explicit kind signature. If you write `T` like this:
```hs
data T (a :: k) where
MkT :: T Int
```
Then it will work with `TypeInType` enabled.
<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 create poly-kinded GADT with TypeInType enabled, but can without","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":"Surprisingly, this compiles without `TypeInType`:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE DataKinds #-}\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE KindSignatures #-}\r\n{-# LANGUAGE PolyKinds #-}\r\nmodule Works where\r\n\r\nimport Data.Kind\r\n\r\ndata T :: k -> Type where\r\n MkT :: T Int\r\n}}}\r\n\r\nBut once you add `TypeInType`:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE DataKinds #-}\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE KindSignatures #-}\r\n{-# LANGUAGE PolyKinds #-}\r\n{-# LANGUAGE TypeInType #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ndata T :: k -> Type where\r\n MkT :: T Int\r\n}}}\r\n\r\nthen it stops working!\r\n\r\n{{{\r\nGHCi, version 8.3.20170516: 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:11:12: error:\r\n • Expected kind ‘k’, but ‘Int’ has kind ‘*’\r\n • In the first argument of ‘T’, namely ‘Int’\r\n In the type ‘T Int’\r\n In the definition of data constructor ‘MkT’\r\n |\r\n11 | MkT :: T Int\r\n | ^^^\r\n}}}\r\n\r\nThis bug is present in GHC 8.0.1, 8.0.2, 8.2.1, and HEAD.\r\n\r\nWhat's strange about this bug is that is requires that you write `T` with an explicit kind signature. If you write `T` like this:\r\n\r\n{{{#!hs\r\ndata T (a :: k) where\r\n MkT :: T Int\r\n}}}\r\n\r\nThen it will work with `TypeInType` enabled.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/13674Poor error message which masks occurs-check failure2019-07-07T18:20:39ZRyan ScottPoor error message which masks occurs-check failureHere's some code, reduced from an example in https://github.com/ekmett/constraints/issues/55:
```hs
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-...Here's some code, reduced from an example in https://github.com/ekmett/constraints/issues/55:
```hs
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
import Data.Proxy
import GHC.Exts (Constraint)
import GHC.TypeLits
import Unsafe.Coerce (unsafeCoerce)
data Dict :: Constraint -> * where
Dict :: a => Dict a
infixr 9 :-
newtype a :- b = Sub (a => Dict b)
-- | Given that @a :- b@, derive something that needs a context @b@, using the context @a@
(\\) :: a => (b => r) -> (a :- b) -> r
r \\ Sub Dict = r
newtype Magic n = Magic (KnownNat n => Dict (KnownNat n))
magic :: forall n m o. (Integer -> Integer -> Integer) -> (KnownNat n, KnownNat m) :- KnownNat o
magic f = Sub $ unsafeCoerce (Magic Dict) (natVal (Proxy :: Proxy n) `f` natVal (Proxy :: Proxy m))
type family Lcm :: Nat -> Nat -> Nat where
axiom :: forall a b. Dict (a ~ b)
axiom = unsafeCoerce (Dict :: Dict (a ~ a))
lcmNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (Lcm n m)
lcmNat = magic lcm
lcmIsIdempotent :: forall n. Dict (n ~ Lcm n n)
lcmIsIdempotent = axiom
newtype GF (n :: Nat) = GF Integer
instance KnownNat n => Num (GF n) where
xf@(GF x) + GF y = GF $ (x+y) `mod` (natVal xf)
xf@(GF x) - GF y = GF $ (x-y) `mod` (natVal xf)
xf@(GF x) * GF y = GF $ (x*y) `mod` (natVal xf)
abs = id
signum xf@(GF x) | x==0 = xf
| otherwise = GF 1
fromInteger = GF
x :: GF 5
x = GF 3
y :: GF 5
y = GF 4
foo :: (KnownNat m, KnownNat n) => GF m -> GF n -> GF (Lcm m n)
foo m@(GF x) n@(GF y) = GF $ (x*y) `mod` (lcm (natVal m) (natVal n))
bar :: (KnownNat m) => GF m -> GF m -> GF m
bar (x :: GF m) y = foo x y - foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)
```
Compiling this (with either GHC 8.0.1, 8.0.2, 8.2.1, or HEAD) gives you a downright puzzling type error:
```
$ /opt/ghc/head/bin/ghci Bug.hs
GHCi, version 8.3.20170509: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main ( Bug.hs, interpreted )
Bug.hs:63:21: error:
• Couldn't match type ‘m’ with ‘Lcm m m’
‘m’ is a rigid type variable bound by
the type signature for:
bar :: forall (m :: Nat). KnownNat m => GF m -> GF m -> GF m
at Bug.hs:62:1-44
Expected type: GF m
Actual type: GF (Lcm m m)
• In the first argument of ‘(-)’, namely ‘foo x y’
In the expression:
foo x y - foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)
In an equation for ‘bar’:
bar (x :: GF m) y
= foo x y - foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)
• Relevant bindings include
y :: GF m (bound at Bug.hs:63:17)
x :: GF m (bound at Bug.hs:63:6)
bar :: GF m -> GF m -> GF m (bound at Bug.hs:63:1)
|
63 | bar (x :: GF m) y = foo x y - foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)
| ^^^^^^^
Bug.hs:63:31: error:
• Could not deduce: m ~ Lcm m m
from the context: m ~ Lcm m m
bound by a type expected by the context:
m ~ Lcm m m => GF m
at Bug.hs:63:31-85
‘m’ is a rigid type variable bound by
the type signature for:
bar :: forall (m :: Nat). KnownNat m => GF m -> GF m -> GF m
at Bug.hs:62:1-44
Expected type: GF m
Actual type: GF (Lcm m m)
• In the first argument of ‘(\\)’, namely ‘foo y x’
In the first argument of ‘(\\)’, namely ‘foo y x \\ lcmNat @m @m’
In the second argument of ‘(-)’, namely
‘foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)’
• Relevant bindings include
y :: GF m (bound at Bug.hs:63:17)
x :: GF m (bound at Bug.hs:63:6)
bar :: GF m -> GF m -> GF m (bound at Bug.hs:63:1)
|
63 | bar (x :: GF m) y = foo x y - foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)
| ^^^^^^^
```
In particular, I'd like to emphasize this part:
```
• Could not deduce: m ~ Lcm m m
from the context: m ~ Lcm m m
```
Wat!? Surely, GHC can deduce `m ~ Lcm m m` from `m ~ Lcm m m`? I decided to flip on `-fprint-explicit-kinds` and see if there was some other issue lurking beneath the surface:
```
$ /opt/ghc/head/bin/ghci Bug.hs -fprint-explicit-kinds
GHCi, version 8.3.20170509: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main ( Bug.hs, interpreted )
Bug.hs:63:21: error:
• Couldn't match type ‘m’ with ‘Lcm m m’
‘m’ is a rigid type variable bound by
the type signature for:
bar :: forall (m :: Nat). KnownNat m => GF m -> GF m -> GF m
at Bug.hs:62:1-44
Expected type: GF m
Actual type: GF (Lcm m m)
• In the first argument of ‘(-)’, namely ‘foo x y’
In the expression:
foo x y - foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)
In an equation for ‘bar’:
bar (x :: GF m) y
= foo x y - foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)
• Relevant bindings include
y :: GF m (bound at Bug.hs:63:17)
x :: GF m (bound at Bug.hs:63:6)
bar :: GF m -> GF m -> GF m (bound at Bug.hs:63:1)
|
63 | bar (x :: GF m) y = foo x y - foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)
| ^^^^^^^
Bug.hs:63:31: error:
• Could not deduce: (m :: Nat) ~~ (Lcm m m :: Nat)
from the context: m ~ Lcm m m
bound by a type expected by the context:
m ~ Lcm m m => GF m
at Bug.hs:63:31-85
‘m’ is a rigid type variable bound by
the type signature for:
bar :: forall (m :: Nat). KnownNat m => GF m -> GF m -> GF m
at Bug.hs:62:1-44
Expected type: GF m
Actual type: GF (Lcm m m)
• In the first argument of ‘(\\)’, namely ‘foo y x’
In the first argument of ‘(\\)’, namely ‘foo y x \\ lcmNat @m @m’
In the second argument of ‘(-)’, namely
‘foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)’
• Relevant bindings include
y :: GF m (bound at Bug.hs:63:17)
x :: GF m (bound at Bug.hs:63:6)
bar :: GF m -> GF m -> GF m (bound at Bug.hs:63:1)
|
63 | bar (x :: GF m) y = foo x y - foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)
|
```
Well, not a whole lot changed. We now have this, slightly more specific error instead:
```
• Could not deduce: (m :: Nat) ~~ (Lcm m m :: Nat)
from the context: m ~ Lcm m m
```
Huh, this is flummoxing. Surely `(m :: Nat) ~~ (Lcm m m :: Nat)` ought to be the same thing as `m ~ Lcm m m`, right?https://gitlab.haskell.org/ghc/ghc/-/issues/13650Implement KPush in types2021-10-04T14:41:09ZRichard Eisenbergrae@richarde.devImplement KPush in typesA recent commit contributed a Note (https://gitlab.haskell.org/ghc/ghc/-/commit/ef0ff34d462e3780210567a13d58b868ec3399e0#07ce9a046fb8ea6659690020b0a8551d94cfdf1c_1175_1163) that explains why we need the dreaded KPush rule to be implement...A recent commit contributed a Note (https://gitlab.haskell.org/ghc/ghc/-/commit/ef0ff34d462e3780210567a13d58b868ec3399e0#07ce9a046fb8ea6659690020b0a8551d94cfdf1c_1175_1163) that explains why we need the dreaded KPush rule to be implemented in `splitTyConApp`. Without KPush there, it's possible that we can have two types t1 and t2 such that `t1 `eqType` t2` and yet they respond differently to `splitTyConApp`: t1 = `(T |> co1) (a |> co2)` and t2 = `T a`. Both t1 and t2 are well-kinded and can have the same kind. But one is a `TyConApp` and one is an `AppTy`. (Actually, looking at this, perhaps the magic will be in `mkAppTy`, not `splitTyConApp`.) But I have to look closer.
This ticket serves as a reminder to do so.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | |
| Type | Task |
| TypeOfFailure | OtherFailure |
| Priority | high |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Implement KPush in types","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.4.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Task","description":"A recent commit contributed a [https://phabricator.haskell.org/diffusion/GHC/browse/master/compiler/types/Type.hs;a483e711da7834bc952367f554ac4e877b4e157a$1191 Note] that explains why we need the dreaded KPush rule to be implemented in `splitTyConApp`. Without KPush there, it's possible that we can have two types t1 and t2 such that {{{t1 `eqType` t2}}} and yet they respond differently to `splitTyConApp`: t1 = `(T |> co1) (a |> co2)` and t2 = `T a`. Both t1 and t2 are well-kinded and can have the same kind. But one is a `TyConApp` and one is an `AppTy`. (Actually, looking at this, perhaps the magic will be in `mkAppTy`, not `splitTyConApp`.) But I have to look closer.\r\n\r\nThis ticket serves as a reminder to do so.","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/13643Core lint error with TypeInType and TypeFamilyDependencies2019-07-07T18:20:49ZIcelandjackCore lint error with TypeInType and TypeFamilyDependenciesIn the code
```hs
{-# Language TypeFamilyDependencies #-}
{-# Language RankNTypes #-}
{-# Language KindSignatures #-}
{-# Language DataKinds #-}
{-# Language TypeInType #-}
{-# Language GADTs...In the code
```hs
{-# Language TypeFamilyDependencies #-}
{-# Language RankNTypes #-}
{-# Language KindSignatures #-}
{-# Language DataKinds #-}
{-# Language TypeInType #-}
{-# Language GADTs #-}
import Data.Kind (Type)
data Code = I
type family
Interp (a :: Code) = (res :: Type) | res -> a where
Interp I = Bool
data T :: forall a. Interp a -> Type where
MkNat :: T False
instance Show (T a) where show _ = "MkNat"
main = do
print MkNat
```
but add `{-# Options_GHC -dcore-lint #-}` and we get the attached log from running `runghc /tmp/tPb2.hs > /tmp/tPb2.log`.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.0.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | #12102 |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Core lint error with TypeInType and TypeFamilyDependencies","status":"New","operating_system":"","component":"Compiler","related":[12102],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["InjectiveFamilies,","TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"In the code\r\n\r\n{{{#!hs\r\n{-# Language TypeFamilyDependencies #-}\r\n{-# Language RankNTypes #-}\r\n{-# Language KindSignatures #-}\r\n{-# Language DataKinds #-}\r\n{-# Language TypeInType #-}\r\n{-# Language GADTs #-}\r\n\r\nimport Data.Kind (Type)\r\n\r\ndata Code = I\r\n\r\ntype family\r\n Interp (a :: Code) = (res :: Type) | res -> a where\r\n Interp I = Bool\r\n\r\ndata T :: forall a. Interp a -> Type where\r\n MkNat :: T False\r\n\r\ninstance Show (T a) where show _ = \"MkNat\"\r\n\r\nmain = do\r\n print MkNat\r\n}}}\r\n\r\nbut add `{-# Options_GHC -dcore-lint #-}` and we get the attached log from running `runghc /tmp/tPb2.hs > /tmp/tPb2.log`.\r\n","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/13625GHC internal error: ‘Y’ is not in scope during type checking, but it passed t...2019-07-07T18:20:53ZMatthew PickeringGHC internal error: ‘Y’ is not in scope during type checking, but it passed the renamer```
{-# LANGUAGE TypeInType #-}
data X :: Y where Y :: X
```
The error message is:
```
Bug.hs:2:11: error: …
• GHC internal error: ‘Y’ is not in scope during type checking, but it passed the renamer
tcl_env of environment: [r...```
{-# LANGUAGE TypeInType #-}
data X :: Y where Y :: X
```
The error message is:
```
Bug.hs:2:11: error: …
• GHC internal error: ‘Y’ is not in scope during type checking, but it passed the renamer
tcl_env of environment: [r1cR :-> APromotionErr TyConPE]
• In the kind ‘Y’
```
Originally reported by \@mietek in #11821
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.0.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | mietek |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC internal error: ‘Y’ is not in scope during type checking, but it passed the renamer","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":["mietek"],"type":"Bug","description":"{{{\r\n{-# LANGUAGE TypeInType #-}\r\ndata X :: Y where Y :: X\r\n}}}\r\n\r\nThe error message is:\r\n\r\n{{{\r\nBug.hs:2:11: error: …\r\n • GHC internal error: ‘Y’ is not in scope during type checking, but it passed the renamer\r\n tcl_env of environment: [r1cR :-> APromotionErr TyConPE]\r\n • In the kind ‘Y’\r\n}}}\r\n\r\nOriginally reported by @mietek in #11821","type_of_failure":"OtherFailure","blocking":[]} -->8.2.1https://gitlab.haskell.org/ghc/ghc/-/issues/13603Can't resolve levity polymorphic superclass2019-07-07T18:21:04ZIcelandjackCan't resolve levity polymorphic superclassThis works
```hs
{-# Language PolyKinds, TypeInType #-}
import GHC.Exts (TYPE, RuntimeRep)
class A (a :: TYPE rep)
class A a => B (a :: TYPE rep)
instance A b => A (a -> (b :: TYPE rep))
instance B b => B (a -> b)
```
but the...This works
```hs
{-# Language PolyKinds, TypeInType #-}
import GHC.Exts (TYPE, RuntimeRep)
class A (a :: TYPE rep)
class A a => B (a :: TYPE rep)
instance A b => A (a -> (b :: TYPE rep))
instance B b => B (a -> b)
```
but the moment you add (`b :: TYPE rep`) to the last line it stops working
```hs
-- t3I7.hs:9:10-40: error: …
-- • Could not deduce (A b)
-- arising from the superclasses of an instance declaration
-- from the context: B b
-- bound by the instance declaration at /tmp/t3I7.hs:9:10-40
-- • In the instance declaration for ‘B (a -> b)’
-- Compilation failed.
{-# Language PolyKinds, TypeInType #-}
import GHC.Exts (TYPE, RuntimeRep)
class A (a :: TYPE rep)
class A a => B (a :: TYPE rep)
instance A b => A (a -> (b :: TYPE rep))
instance B b => B (a -> (b :: TYPE rep))
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.0.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Can't resolve levity polymorphic superclass","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["LevityPolymorphism,","TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This works\r\n\r\n{{{#!hs\r\n{-# Language PolyKinds, TypeInType #-}\r\n\r\nimport GHC.Exts (TYPE, RuntimeRep)\r\n\r\nclass A (a :: TYPE rep)\r\nclass A a => B (a :: TYPE rep)\r\n\r\ninstance A b => A (a -> (b :: TYPE rep))\r\ninstance B b => B (a -> b)\r\n}}}\r\n\r\nbut the moment you add (`b :: TYPE rep`) to the last line it stops working\r\n\r\n\r\n{{{#!hs\r\n-- t3I7.hs:9:10-40: error: …\r\n-- • Could not deduce (A b)\r\n-- arising from the superclasses of an instance declaration\r\n-- from the context: B b\r\n-- bound by the instance declaration at /tmp/t3I7.hs:9:10-40\r\n-- • In the instance declaration for ‘B (a -> b)’\r\n-- Compilation failed.\r\n\r\n{-# Language PolyKinds, TypeInType #-}\r\n\r\nimport GHC.Exts (TYPE, RuntimeRep)\r\n\r\nclass A (a :: TYPE rep)\r\nclass A a => B (a :: TYPE rep)\r\n\r\ninstance A b => A (a -> (b :: TYPE rep))\r\ninstance B b => B (a -> (b :: TYPE rep))\r\n}}}\r\n\r\n\r\n","type_of_failure":"OtherFailure","blocking":[]} -->8.2.1https://gitlab.haskell.org/ghc/ghc/-/issues/13585ala from Control.Lens.Wrapped panics2019-07-07T18:21:10ZFumiaki Kinoshitaala from Control.Lens.Wrapped panicsPanic.hs:
```
module Panic where
import Control.Lens.Wrapped
import Data.Monoid
foo :: Maybe String
foo = ala Last foldMap [Just "foo"]
```
main.hs:
```
module Main where
import Panic (foo)
main :: IO ()
main = print foo
```
```
$...Panic.hs:
```
module Panic where
import Control.Lens.Wrapped
import Data.Monoid
foo :: Maybe String
foo = ala Last foldMap [Just "foo"]
```
main.hs:
```
module Main where
import Panic (foo)
main :: IO ()
main = print foo
```
```
$ ghc -c -O2 Panic.hs
$ ghc -c -O2 main.hs
ghc: panic! (the 'impossible' happened)
(GHC version 8.2.0.20170404 for x86_64-unknown-linux):
splitTyConApp
(Exchange (Unwrapped (Last String)) (Unwrapped (Last String)) |> <*
-> * -> *>_N) (Maybe
[Char]) ((Identity |> <*
-> *>_N) (Maybe
[Char]))
Call stack:
CallStack (from HasCallStack):
prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1134:58 in ghc:Outputable
callStackDoc, called at compiler/utils/Outputable.hs:1138:37 in ghc:Outputable
pprPanic, called at compiler/types/Type.hs:1105:34 in ghc:Type
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
```
The GHC version is 8134f7d4ba2c14b2f24d2f4c1f5260fcaff3304a.
Control.Lens.Wrapped is from the latest version of lens on GitHub: https://github.com/ekmett/lens/blob/9c4447de7ef57f67dbe293320d45bd8a546be522/src/Control/Lens/Wrapped.hs8.2.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/13555Typechecker regression when combining PolyKinds and MonoLocalBinds2019-07-07T18:21:21ZRyan ScottTypechecker regression when combining PolyKinds and MonoLocalBinds`lol-0.6.0.0` from Hackage currently fails to build with GHC 8.2.1 because of this regression. Here is a minimized example:
```hs
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE MonoLocalBinds #-}
{-# LANGUA...`lol-0.6.0.0` from Hackage currently fails to build with GHC 8.2.1 because of this regression. Here is a minimized example:
```hs
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE MonoLocalBinds #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
module Crypto.Lol.Types.FiniteField (GF(..)) where
import Data.Functor.Identity (Identity(..))
data T a
type Polynomial a = T a
newtype GF fp d = GF (Polynomial fp)
type CRTInfo r = (Int -> r, r)
type Tagged s b = TaggedT s Identity b
newtype TaggedT s m b = TagT { untagT :: m b }
class Reflects a i where
value :: Tagged a i
class CRTrans mon r where
crtInfo :: Reflects m Int => TaggedT m mon (CRTInfo r)
instance CRTrans Maybe (GF fp d) where
crtInfo :: forall m . (Reflects m Int) => TaggedT m Maybe (CRTInfo (GF fp d))
crtInfo = undefined
```
This typechecks OK with GHC 8.0.2, but with 8.2.1, it complains:
```
$ /opt/ghc/8.2.1/bin/ghci Bug.hs
GHCi, version 8.2.0.20170403: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Crypto.Lol.Types.FiniteField ( Bug.hs, interpreted )
Bug.hs:25:14: error:
• Couldn't match type ‘k0’ with ‘k2’
because type variable ‘k2’ would escape its scope
This (rigid, skolem) type variable is bound by
the type signature for:
crtInfo :: forall k2 (m :: k2).
Reflects m Int =>
TaggedT m Maybe (CRTInfo (GF fp d))
at Bug.hs:25:14-79
Expected type: TaggedT m Maybe (CRTInfo (GF fp d))
Actual type: TaggedT m Maybe (CRTInfo (GF fp d))
• When checking that instance signature for ‘crtInfo’
is more general than its signature in the class
Instance sig: forall (m :: k0).
Reflects m Int =>
TaggedT m Maybe (CRTInfo (GF fp d))
Class sig: forall k2 (m :: k2).
Reflects m Int =>
TaggedT m Maybe (CRTInfo (GF fp d))
In the instance declaration for ‘CRTrans Maybe (GF fp d)’
|
25 | crtInfo :: forall m . (Reflects m Int) => TaggedT m Maybe (CRTInfo (GF fp d))
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Bug.hs:25:14: error:
• Could not deduce (Reflects m Int)
from the context: Reflects m Int
bound by the type signature for:
crtInfo :: forall k2 (m :: k2).
Reflects m Int =>
TaggedT m Maybe (CRTInfo (GF fp d))
at Bug.hs:25:14-79
The type variable ‘k0’ is ambiguous
• When checking that instance signature for ‘crtInfo’
is more general than its signature in the class
Instance sig: forall (m :: k0).
Reflects m Int =>
TaggedT m Maybe (CRTInfo (GF fp d))
Class sig: forall k2 (m :: k2).
Reflects m Int =>
TaggedT m Maybe (CRTInfo (GF fp d))
In the instance declaration for ‘CRTrans Maybe (GF fp d)’
|
25 | crtInfo :: forall m . (Reflects m Int) => TaggedT m Maybe (CRTInfo (GF fp d))
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
Notably, both `PolyKinds` and `MonoLocalBinds` are required to trigger this bug.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | highest |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Typechecker regression when combining PolyKinds and MonoLocalBinds","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.2.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"`lol-0.6.0.0` from Hackage currently fails to build with GHC 8.2.1 because of this regression. Here is a minimized example:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE FlexibleContexts #-}\r\n{-# LANGUAGE InstanceSigs #-}\r\n{-# LANGUAGE MonoLocalBinds #-}\r\n{-# LANGUAGE MultiParamTypeClasses #-}\r\n{-# LANGUAGE PolyKinds #-}\r\n{-# LANGUAGE RankNTypes #-}\r\nmodule Crypto.Lol.Types.FiniteField (GF(..)) where\r\n\r\nimport Data.Functor.Identity (Identity(..))\r\n\r\ndata T a\r\ntype Polynomial a = T a\r\nnewtype GF fp d = GF (Polynomial fp)\r\ntype CRTInfo r = (Int -> r, r)\r\ntype Tagged s b = TaggedT s Identity b\r\nnewtype TaggedT s m b = TagT { untagT :: m b }\r\n\r\nclass Reflects a i where\r\n value :: Tagged a i\r\n\r\nclass CRTrans mon r where\r\n crtInfo :: Reflects m Int => TaggedT m mon (CRTInfo r)\r\n\r\ninstance CRTrans Maybe (GF fp d) where\r\n crtInfo :: forall m . (Reflects m Int) => TaggedT m Maybe (CRTInfo (GF fp d))\r\n crtInfo = undefined\r\n}}}\r\n\r\nThis typechecks OK with GHC 8.0.2, but with 8.2.1, it complains:\r\n\r\n{{{\r\n$ /opt/ghc/8.2.1/bin/ghci Bug.hs\r\nGHCi, version 8.2.0.20170403: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Crypto.Lol.Types.FiniteField ( Bug.hs, interpreted )\r\n\r\nBug.hs:25:14: error:\r\n • Couldn't match type ‘k0’ with ‘k2’\r\n because type variable ‘k2’ would escape its scope\r\n This (rigid, skolem) type variable is bound by\r\n the type signature for:\r\n crtInfo :: forall k2 (m :: k2).\r\n Reflects m Int =>\r\n TaggedT m Maybe (CRTInfo (GF fp d))\r\n at Bug.hs:25:14-79\r\n Expected type: TaggedT m Maybe (CRTInfo (GF fp d))\r\n Actual type: TaggedT m Maybe (CRTInfo (GF fp d))\r\n • When checking that instance signature for ‘crtInfo’\r\n is more general than its signature in the class\r\n Instance sig: forall (m :: k0).\r\n Reflects m Int =>\r\n TaggedT m Maybe (CRTInfo (GF fp d))\r\n Class sig: forall k2 (m :: k2).\r\n Reflects m Int =>\r\n TaggedT m Maybe (CRTInfo (GF fp d))\r\n In the instance declaration for ‘CRTrans Maybe (GF fp d)’\r\n |\r\n25 | crtInfo :: forall m . (Reflects m Int) => TaggedT m Maybe (CRTInfo (GF fp d))\r\n | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n\r\nBug.hs:25:14: error:\r\n • Could not deduce (Reflects m Int)\r\n from the context: Reflects m Int\r\n bound by the type signature for:\r\n crtInfo :: forall k2 (m :: k2).\r\n Reflects m Int =>\r\n TaggedT m Maybe (CRTInfo (GF fp d))\r\n at Bug.hs:25:14-79\r\n The type variable ‘k0’ is ambiguous\r\n • When checking that instance signature for ‘crtInfo’\r\n is more general than its signature in the class\r\n Instance sig: forall (m :: k0).\r\n Reflects m Int =>\r\n TaggedT m Maybe (CRTInfo (GF fp d))\r\n Class sig: forall k2 (m :: k2).\r\n Reflects m Int =>\r\n TaggedT m Maybe (CRTInfo (GF fp d))\r\n In the instance declaration for ‘CRTrans Maybe (GF fp d)’\r\n |\r\n25 | crtInfo :: forall m . (Reflects m Int) => TaggedT m Maybe (CRTInfo (GF fp d))\r\n | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nNotably, both `PolyKinds` and `MonoLocalBinds` are required to trigger this bug.","type_of_failure":"OtherFailure","blocking":[]} -->8.2.1https://gitlab.haskell.org/ghc/ghc/-/issues/13549GHC 8.2.1's typechecker rejects code generated by singletons that 8.0 accepts2019-07-07T18:21:23ZRyan ScottGHC 8.2.1's typechecker rejects code generated by singletons that 8.0 acceptsI recently attempted to upgrade `singletons` to use GHC 8.2.1, but was thwarted when GHC's typechecker rejected code that was generated by Template Haskell. I was able to put all of this code in a single module (which I've attached), but...I recently attempted to upgrade `singletons` to use GHC 8.2.1, but was thwarted when GHC's typechecker rejected code that was generated by Template Haskell. I was able to put all of this code in a single module (which I've attached), but sadly, it's 1367 lines long. What's important is that GHC 8.0.1 and 8.0.2 accept this code, but neither 8.2.1-rc1 nor HEAD do. Here is the error message you get, in its full glory:
```
$ /opt/ghc/8.2.1/bin/ghci Bug.hs -fprint-explicit-kinds
GHCi, version 8.2.0.20170403: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:1328:59: error:
• Couldn't match type ‘c69895866216793215480’ with ‘[a_a337f]’
‘c69895866216793215480’ is untouchable
inside the constraints: (arg_a33hh ~ xs_a33fp, arg_a33hi ~ r_a33fq)
bound by the type signature for:
lambda_a33iH :: forall (xs_a33fp :: [a_a337f]) (r_a33fq :: [[a_a337f]]).
(arg_a33hh ~ xs_a33fp, arg_a33hi ~ r_a33fq) =>
Sing [a_a337f] xs_a33fp
-> Sing [[a_a337f]] r_a33fq
-> Sing
[[a_a337f]]
(Apply
[[a_a337f]]
[[a_a337f]]
(Apply
[a_a337f]
(TyFun [[a_a337f]] [[a_a337f]] -> *)
(Let6989586621679736980InterleaveSym4
[a_a337f]
[a_a337f]
a_a337f
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO)
arg_a33hh)
arg_a33hi)
at Bug.hs:(1289,35)-(1294,157)
Expected type: Sing (TyFun [a_a337f] [a_a337f] -> *) t
-> Sing [a_a337f] t1
-> Sing [[a_a337f]] t2
-> Sing
([a_a337f], [[a_a337f]])
((@@)
[[a_a337f]]
([a_a337f], [[a_a337f]])
((@@)
[a_a337f]
([[a_a337f]] ~> ([a_a337f], [[a_a337f]]))
((@@)
(TyFun [a_a337f] [a_a337f] -> *)
([a_a337f] ~> ([[a_a337f]] ~> ([a_a337f], [[a_a337f]])))
(Let6989586621679736980Interleave'Sym4
[a_a337f]
[a_a337f]
a_a337f
[a_a337f]
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO)
t)
t1)
t2)
Actual type: Sing (TyFun [a_a337f] c69895866216793215480 -> *) t
-> Sing [a_a337f] t1
-> Sing [c69895866216793215480] t2
-> Sing
([a_a337f], [c69895866216793215480])
(Apply
[c69895866216793215480]
([a_a337f], [c69895866216793215480])
(Apply
[a_a337f]
([c69895866216793215480] ~> ([a_a337f], [c69895866216793215480]))
(Apply
(TyFun [a_a337f] c69895866216793215480 -> *)
([a_a337f]
~> ([c69895866216793215480]
~> ([a_a337f], [c69895866216793215480])))
(Let6989586621679736980Interleave'Sym4
[a_a337f]
[a_a337f]
a_a337f
c69895866216793215480
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO)
t)
t1)
t2)
• In the second argument of ‘singFun3’, namely ‘sInterleave'’
In the first argument of ‘applySing’, namely
‘((singFun3
(Proxy ::
Proxy (Let6989586621679736980Interleave'Sym4 xs0_a33a0 t_a33aL ts_a33aM is_a33aO)))
sInterleave')’
In the first argument of ‘applySing’, namely
‘((applySing
((singFun3
(Proxy ::
Proxy (Let6989586621679736980Interleave'Sym4 xs0_a33a0 t_a33aL ts_a33aM is_a33aO)))
sInterleave'))
((singFun1 (Proxy :: Proxy IdSym0)) sId))’
• Relevant bindings include
sX_6989586621679737266 :: Sing
([a_a337f], [[a_a337f]])
(Let6989586621679737265X_6989586621679737266Sym6
[a_a337f]
[a_a337f]
a_a337f
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO
xs_a33fp
r_a33fq)
(bound at Bug.hs:1321:41)
r_a33iK :: Sing [[a_a337f]] r_a33fq (bound at Bug.hs:1295:57)
xs_a33iJ :: Sing [a_a337f] xs_a33fp (bound at Bug.hs:1295:48)
lambda_a33iH :: Sing [a_a337f] xs_a33fp
-> Sing [[a_a337f]] r_a33fq
-> Sing
[[a_a337f]]
(Apply
[[a_a337f]]
[[a_a337f]]
(Apply
[a_a337f]
(TyFun [[a_a337f]] [[a_a337f]] -> *)
(Let6989586621679736980InterleaveSym4
[a_a337f]
[a_a337f]
a_a337f
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO)
arg_a33hh)
arg_a33hi)
(bound at Bug.hs:1295:35)
sR :: Sing [[a_a337f]] arg_a33hi (bound at Bug.hs:1287:45)
sXs :: Sing [a_a337f] arg_a33hh (bound at Bug.hs:1287:41)
sInterleave' :: forall (arg_a33he :: TyFun
[a_a337f] c69895866216793215480
-> *) (arg_a33hf :: [a_a337f]) (arg_a33hg :: [c69895866216793215480]).
Sing (TyFun [a_a337f] c69895866216793215480 -> *) arg_a33he
-> Sing [a_a337f] arg_a33hf
-> Sing [c69895866216793215480] arg_a33hg
-> Sing
([a_a337f], [c69895866216793215480])
(Apply
[c69895866216793215480]
([a_a337f], [c69895866216793215480])
(Apply
[a_a337f]
([c69895866216793215480] ~> ([a_a337f], [c69895866216793215480]))
(Apply
(TyFun [a_a337f] c69895866216793215480 -> *)
([a_a337f]
~> ([c69895866216793215480]
~> ([a_a337f], [c69895866216793215480])))
(Let6989586621679736980Interleave'Sym4
[a_a337f]
[a_a337f]
a_a337f
c69895866216793215480
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO)
arg_a33he)
arg_a33hf)
arg_a33hg)
(bound at Bug.hs:1166:29)
lambda_a33ha :: Sing a_a337f t_a33aL
-> Sing [a_a337f] ts_a33aM
-> Sing [a_a337f] is_a33aO
-> Sing
[[a_a337f]]
(Apply
[a_a337f]
[[a_a337f]]
(Apply
[a_a337f]
([a_a337f] ~> [[a_a337f]])
(Let6989586621679736931PermsSym1 a_a337f xs0_a33a0)
arg_a33h0)
arg_a33h1)
(bound at Bug.hs:1153:23)
sTs :: Sing [a_a337f] n_a1kQd (bound at Bug.hs:1143:34)
sT :: Sing a_a337f n_a1kQc (bound at Bug.hs:1143:31)
lambda_a33gY :: Sing [a_a337f] xs0_a33a0
-> Sing
[[a_a337f]]
(Apply [a_a337f] [[a_a337f]] (PermutationsSym0 a_a337f) t_a33gX)
(bound at Bug.hs:1127:11)
(Some bindings suppressed; use -fmax-relevant-binds=N or -fno-max-relevant-binds)
|
1328 | sInterleave'))
| ^^^^^^^^^^^^
Bug.hs:1328:59: error:
• Could not deduce: (Let6989586621679736980Interleave'
[a_a337f]
[a_a337f]
a_a337f
c69895866216793215480
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO
t
t1
t2 :: ([a_a337f], [c69895866216793215480]))
~~
(Let6989586621679736980Interleave'
[a_a337f]
[a_a337f]
a_a337f
[a_a337f]
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO
t
t1
t2 :: ([a_a337f], [c69895866216793215480]))
from the context: t_a33gX ~ xs0_a33a0
bound by the type signature for:
lambda_a33gY :: forall (xs0_a33a0 :: [a_a337f]).
t_a33gX ~ xs0_a33a0 =>
Sing [a_a337f] xs0_a33a0
-> Sing
[[a_a337f]]
(Apply
[a_a337f] [[a_a337f]] (PermutationsSym0 a_a337f) t_a33gX)
at Bug.hs:(1122,11)-(1126,67)
or from: arg_a33h0 ~ (':) a_a337f n_a1kQc n_a1kQd
bound by a pattern with constructor:
SCons :: forall a_11 (z_a1kQb :: [a_11]) (n_a1kQc :: a_11) (n_a1kQd :: [a_11]).
z_a1kQb ~ (':) a_11 n_a1kQc n_a1kQd =>
Sing a_11 n_a1kQc -> Sing [a_11] n_a1kQd -> Sing [a_11] z_a1kQb,
in an equation for ‘sPerms’
at Bug.hs:1143:25-36
or from: (arg_a33h0
~
Apply
[a_a337f]
[a_a337f]
(Apply
a_a337f (TyFun [a_a337f] [a_a337f] -> *) ((:$) a_a337f) t_a33aL)
ts_a33aM,
arg_a33h1 ~ is_a33aO)
bound by the type signature for:
lambda_a33ha :: forall (t_a33aL :: a_a337f) (ts_a33aM :: [a_a337f]) (is_a33aO :: [a_a337f]).
(arg_a33h0
~
Apply
[a_a337f]
[a_a337f]
(Apply
a_a337f
(TyFun [a_a337f] [a_a337f] -> *)
((:$) a_a337f)
t_a33aL)
ts_a33aM,
arg_a33h1 ~ is_a33aO) =>
Sing a_a337f t_a33aL
-> Sing [a_a337f] ts_a33aM
-> Sing [a_a337f] is_a33aO
-> Sing
[[a_a337f]]
(Apply
[a_a337f]
[[a_a337f]]
(Apply
[a_a337f]
([a_a337f] ~> [[a_a337f]])
(Let6989586621679736931PermsSym1 a_a337f xs0_a33a0)
arg_a33h0)
arg_a33h1)
at Bug.hs:(1145,23)-(1152,117)
or from: (arg_a33hh ~ xs_a33fp, arg_a33hi ~ r_a33fq)
bound by the type signature for:
lambda_a33iH :: forall (xs_a33fp :: [a_a337f]) (r_a33fq :: [[a_a337f]]).
(arg_a33hh ~ xs_a33fp, arg_a33hi ~ r_a33fq) =>
Sing [a_a337f] xs_a33fp
-> Sing [[a_a337f]] r_a33fq
-> Sing
[[a_a337f]]
(Apply
[[a_a337f]]
[[a_a337f]]
(Apply
[a_a337f]
(TyFun [[a_a337f]] [[a_a337f]] -> *)
(Let6989586621679736980InterleaveSym4
[a_a337f]
[a_a337f]
a_a337f
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO)
arg_a33hh)
arg_a33hi)
at Bug.hs:(1289,35)-(1294,157)
Expected type: Sing (TyFun [a_a337f] [a_a337f] -> *) t
-> Sing [a_a337f] t1
-> Sing [[a_a337f]] t2
-> Sing
([a_a337f], [[a_a337f]])
((@@)
[[a_a337f]]
([a_a337f], [[a_a337f]])
((@@)
[a_a337f]
([[a_a337f]] ~> ([a_a337f], [[a_a337f]]))
((@@)
(TyFun [a_a337f] [a_a337f] -> *)
([a_a337f] ~> ([[a_a337f]] ~> ([a_a337f], [[a_a337f]])))
(Let6989586621679736980Interleave'Sym4
[a_a337f]
[a_a337f]
a_a337f
[a_a337f]
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO)
t)
t1)
t2)
Actual type: Sing (TyFun [a_a337f] c69895866216793215480 -> *) t
-> Sing [a_a337f] t1
-> Sing [c69895866216793215480] t2
-> Sing
([a_a337f], [c69895866216793215480])
(Apply
[c69895866216793215480]
([a_a337f], [c69895866216793215480])
(Apply
[a_a337f]
([c69895866216793215480] ~> ([a_a337f], [c69895866216793215480]))
(Apply
(TyFun [a_a337f] c69895866216793215480 -> *)
([a_a337f]
~> ([c69895866216793215480]
~> ([a_a337f], [c69895866216793215480])))
(Let6989586621679736980Interleave'Sym4
[a_a337f]
[a_a337f]
a_a337f
c69895866216793215480
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO)
t)
t1)
t2)
The type variable ‘c69895866216793215480’ is ambiguous
• In the second argument of ‘singFun3’, namely ‘sInterleave'’
In the first argument of ‘applySing’, namely
‘((singFun3
(Proxy ::
Proxy (Let6989586621679736980Interleave'Sym4 xs0_a33a0 t_a33aL ts_a33aM is_a33aO)))
sInterleave')’
In the first argument of ‘applySing’, namely
‘((applySing
((singFun3
(Proxy ::
Proxy (Let6989586621679736980Interleave'Sym4 xs0_a33a0 t_a33aL ts_a33aM is_a33aO)))
sInterleave'))
((singFun1 (Proxy :: Proxy IdSym0)) sId))’
• Relevant bindings include
sX_6989586621679737266 :: Sing
([a_a337f], [[a_a337f]])
(Let6989586621679737265X_6989586621679737266Sym6
[a_a337f]
[a_a337f]
a_a337f
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO
xs_a33fp
r_a33fq)
(bound at Bug.hs:1321:41)
r_a33iK :: Sing [[a_a337f]] r_a33fq (bound at Bug.hs:1295:57)
xs_a33iJ :: Sing [a_a337f] xs_a33fp (bound at Bug.hs:1295:48)
lambda_a33iH :: Sing [a_a337f] xs_a33fp
-> Sing [[a_a337f]] r_a33fq
-> Sing
[[a_a337f]]
(Apply
[[a_a337f]]
[[a_a337f]]
(Apply
[a_a337f]
(TyFun [[a_a337f]] [[a_a337f]] -> *)
(Let6989586621679736980InterleaveSym4
[a_a337f]
[a_a337f]
a_a337f
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO)
arg_a33hh)
arg_a33hi)
(bound at Bug.hs:1295:35)
sR :: Sing [[a_a337f]] arg_a33hi (bound at Bug.hs:1287:45)
sXs :: Sing [a_a337f] arg_a33hh (bound at Bug.hs:1287:41)
sInterleave' :: forall (arg_a33he :: TyFun
[a_a337f] c69895866216793215480
-> *) (arg_a33hf :: [a_a337f]) (arg_a33hg :: [c69895866216793215480]).
Sing (TyFun [a_a337f] c69895866216793215480 -> *) arg_a33he
-> Sing [a_a337f] arg_a33hf
-> Sing [c69895866216793215480] arg_a33hg
-> Sing
([a_a337f], [c69895866216793215480])
(Apply
[c69895866216793215480]
([a_a337f], [c69895866216793215480])
(Apply
[a_a337f]
([c69895866216793215480] ~> ([a_a337f], [c69895866216793215480]))
(Apply
(TyFun [a_a337f] c69895866216793215480 -> *)
([a_a337f]
~> ([c69895866216793215480]
~> ([a_a337f], [c69895866216793215480])))
(Let6989586621679736980Interleave'Sym4
[a_a337f]
[a_a337f]
a_a337f
c69895866216793215480
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO)
arg_a33he)
arg_a33hf)
arg_a33hg)
(bound at Bug.hs:1166:29)
lambda_a33ha :: Sing a_a337f t_a33aL
-> Sing [a_a337f] ts_a33aM
-> Sing [a_a337f] is_a33aO
-> Sing
[[a_a337f]]
(Apply
[a_a337f]
[[a_a337f]]
(Apply
[a_a337f]
([a_a337f] ~> [[a_a337f]])
(Let6989586621679736931PermsSym1 a_a337f xs0_a33a0)
arg_a33h0)
arg_a33h1)
(bound at Bug.hs:1153:23)
sTs :: Sing [a_a337f] n_a1kQd (bound at Bug.hs:1143:34)
sT :: Sing a_a337f n_a1kQc (bound at Bug.hs:1143:31)
lambda_a33gY :: Sing [a_a337f] xs0_a33a0
-> Sing
[[a_a337f]]
(Apply [a_a337f] [[a_a337f]] (PermutationsSym0 a_a337f) t_a33gX)
(bound at Bug.hs:1127:11)
(Some bindings suppressed; use -fmax-relevant-binds=N or -fno-max-relevant-binds)
|
1328 | sInterleave'))
| ^^^^^^^^^^^^
```8.4.1