GHC issueshttps://gitlab.haskell.org/ghc/ghc//issues20190707T18:28:14Zhttps://gitlab.haskell.org/ghc/ghc//issues/11964Without TypeInType, inconsistently accepts Data.Kind.Type but not type synonym20190707T18:28:14ZEdward Z. YangWithout TypeInType, inconsistently accepts Data.Kind.Type but not type synonymFor convenience, I'll use GHCi to demonstrate flag behavior. First, we define a file:
```
{# LANGUAGE TypeInType #}
import Data.Kind
type Star = Type
newtype T k (t :: k) = T ()
```
Next, we load it up in GHCi, WITHOUT `XTypeInType`. Now we observe strange behavior:
```
ezyang@sabre:~$ ghc8.0 interactive C.hs
GHCi, version 8.0.0.20160204: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( C.hs, interpreted )
Ok, modules loaded: Main.
*Main> :k T Type Int
T Type Int :: *
*Main> :k T Star Int
<interactive>:1:3: error:
• Data constructor ‘Star’ cannot be used here
(Perhaps you intended to use DataKinds)
• In the first argument of ‘T’, namely ‘Star’
In the type ‘T Star Int’
```
Of course, if we pass `TypeInType` to GHCi that fixes the problem (BTW, `DataKinds` does NOT solve the problem.)For convenience, I'll use GHCi to demonstrate flag behavior. First, we define a file:
```
{# LANGUAGE TypeInType #}
import Data.Kind
type Star = Type
newtype T k (t :: k) = T ()
```
Next, we load it up in GHCi, WITHOUT `XTypeInType`. Now we observe strange behavior:
```
ezyang@sabre:~$ ghc8.0 interactive C.hs
GHCi, version 8.0.0.20160204: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( C.hs, interpreted )
Ok, modules loaded: Main.
*Main> :k T Type Int
T Type Int :: *
*Main> :k T Star Int
<interactive>:1:3: error:
• Data constructor ‘Star’ cannot be used here
(Perhaps you intended to use DataKinds)
• In the first argument of ‘T’, namely ‘Star’
In the type ‘T Star Int’
```
Of course, if we pass `TypeInType` to GHCi that fixes the problem (BTW, `DataKinds` does NOT solve the problem.)Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/11672Poor error message20190707T18:29:09ZAdam GundryPoor error message[Daniel Díaz recently pointed out](https://mail.haskell.org/pipermail/haskellcafe/2016February/123262.html) a particularly terrible error message. Here's a reduced example:
```hs
{# LANGUAGE DataKinds #}
{# LANGUAGE KindSignatures #}
module BadError where
import GHC.TypeLits
import Data.Proxy
f :: Proxy (a :: Symbol) > Int
f _ = f (Proxy :: Proxy (Int > Bool))
```
With GHC 8.0 RC2, this leads to the following error:
```
• Expected kind ‘Proxy ((>) Int Bool)’,
but ‘Data.Proxy.Proxy :: Proxy (Int > Bool)’ has kind ‘Proxy
(Int > Bool)’
• In the first argument of ‘f’, namely
‘(Proxy :: Proxy (Int > Bool))’
In the expression: f (Proxy :: Proxy (Int > Bool))
In an equation for ‘f’: f _ = f (Proxy :: Proxy (Int > Bool))
```
or with `fprintexplicitkinds fprintexplicitcoercions`:
```
• Expected kind ‘Proxy
Symbol
(((>) > <*>_N > <*>_N > U(hole:{aCy}, *, Symbol)_N) Int Bool)’,
but ‘(Data.Proxy.Proxy) @ k_aCv @ t_aCw ::
Proxy (Int > Bool)’ has kind ‘Proxy * (Int > Bool)’
```
As Iavor, Richard and I discussed, this message has at least three separate problems:
 It says `kind` when it should say `type`.
 `((>) Int Bool)` is printed instead of `Int > Bool` (because there is a coercion hiding in the type).
 The real error is the insoluble constraint `Symbol ~ *`, which is not reported at all!
The first two should be fairly easy to fix. For the third, when reporting insoluble constraints, we should prefer to report those on which no other constraints depend. (In this case, the presence of `hole:{aCy}` in the constraint is an explicit dependency on the other constraint.)
I'll try to take a look at this. It is no doubt related to #11198.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.1rc2 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  diatchki, goldfire 
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Poor error message","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"adamgundry"},"version":"8.0.1rc2","keywords":["ErrorMessages"],"differentials":[],"test_case":"","architecture":"","cc":["diatchki","goldfire"],"type":"Bug","description":"[https://mail.haskell.org/pipermail/haskellcafe/2016February/123262.html Daniel Díaz recently pointed out] a particularly terrible error message. Here's a reduced example:\r\n{{{#!hs\r\n{# LANGUAGE DataKinds #}\r\n{# LANGUAGE KindSignatures #}\r\nmodule BadError where\r\n\r\nimport GHC.TypeLits\r\nimport Data.Proxy\r\n\r\nf :: Proxy (a :: Symbol) > Int\r\nf _ = f (Proxy :: Proxy (Int > Bool))\r\n}}}\r\n\r\nWith GHC 8.0 RC2, this leads to the following error:\r\n{{{\r\n • Expected kind ‘Proxy ((>) Int Bool)’,\r\n but ‘Data.Proxy.Proxy :: Proxy (Int > Bool)’ has kind ‘Proxy\r\n (Int > Bool)’\r\n • In the first argument of ‘f’, namely\r\n ‘(Proxy :: Proxy (Int > Bool))’\r\n In the expression: f (Proxy :: Proxy (Int > Bool))\r\n In an equation for ‘f’: f _ = f (Proxy :: Proxy (Int > Bool))\r\n}}}\r\nor with `fprintexplicitkinds fprintexplicitcoercions`:\r\n{{{\r\n • Expected kind ‘Proxy\r\n Symbol\r\n (((>) > <*>_N > <*>_N > U(hole:{aCy}, *, Symbol)_N) Int Bool)’,\r\n but ‘(Data.Proxy.Proxy) @ k_aCv @ t_aCw ::\r\n Proxy (Int > Bool)’ has kind ‘Proxy * (Int > Bool)’\r\n}}}\r\n\r\nAs Iavor, Richard and I discussed, this message has at least three separate problems:\r\n\r\n * It says `kind` when it should say `type`.\r\n\r\n * `((>) Int Bool)` is printed instead of `Int > Bool` (because there is a coercion hiding in the type).\r\n\r\n * The real error is the insoluble constraint `Symbol ~ *`, which is not reported at all!\r\n\r\nThe first two should be fairly easy to fix. For the third, when reporting insoluble constraints, we should prefer to report those on which no other constraints depend. (In this case, the presence of `hole:{aCy}` in the constraint is an explicit dependency on the other constraint.)\r\n\r\nI'll try to take a look at this. It is no doubt related to #11198.","type_of_failure":"OtherFailure","blocking":[]} >[Daniel Díaz recently pointed out](https://mail.haskell.org/pipermail/haskellcafe/2016February/123262.html) a particularly terrible error message. Here's a reduced example:
```hs
{# LANGUAGE DataKinds #}
{# LANGUAGE KindSignatures #}
module BadError where
import GHC.TypeLits
import Data.Proxy
f :: Proxy (a :: Symbol) > Int
f _ = f (Proxy :: Proxy (Int > Bool))
```
With GHC 8.0 RC2, this leads to the following error:
```
• Expected kind ‘Proxy ((>) Int Bool)’,
but ‘Data.Proxy.Proxy :: Proxy (Int > Bool)’ has kind ‘Proxy
(Int > Bool)’
• In the first argument of ‘f’, namely
‘(Proxy :: Proxy (Int > Bool))’
In the expression: f (Proxy :: Proxy (Int > Bool))
In an equation for ‘f’: f _ = f (Proxy :: Proxy (Int > Bool))
```
or with `fprintexplicitkinds fprintexplicitcoercions`:
```
• Expected kind ‘Proxy
Symbol
(((>) > <*>_N > <*>_N > U(hole:{aCy}, *, Symbol)_N) Int Bool)’,
but ‘(Data.Proxy.Proxy) @ k_aCv @ t_aCw ::
Proxy (Int > Bool)’ has kind ‘Proxy * (Int > Bool)’
```
As Iavor, Richard and I discussed, this message has at least three separate problems:
 It says `kind` when it should say `type`.
 `((>) Int Bool)` is printed instead of `Int > Bool` (because there is a coercion hiding in the type).
 The real error is the insoluble constraint `Symbol ~ *`, which is not reported at all!
The first two should be fairly easy to fix. For the third, when reporting insoluble constraints, we should prefer to report those on which no other constraints depend. (In this case, the presence of `hole:{aCy}` in the constraint is an explicit dependency on the other constraint.)
I'll try to take a look at this. It is no doubt related to #11198.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.1rc2 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  diatchki, goldfire 
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Poor error message","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"adamgundry"},"version":"8.0.1rc2","keywords":["ErrorMessages"],"differentials":[],"test_case":"","architecture":"","cc":["diatchki","goldfire"],"type":"Bug","description":"[https://mail.haskell.org/pipermail/haskellcafe/2016February/123262.html Daniel Díaz recently pointed out] a particularly terrible error message. Here's a reduced example:\r\n{{{#!hs\r\n{# LANGUAGE DataKinds #}\r\n{# LANGUAGE KindSignatures #}\r\nmodule BadError where\r\n\r\nimport GHC.TypeLits\r\nimport Data.Proxy\r\n\r\nf :: Proxy (a :: Symbol) > Int\r\nf _ = f (Proxy :: Proxy (Int > Bool))\r\n}}}\r\n\r\nWith GHC 8.0 RC2, this leads to the following error:\r\n{{{\r\n • Expected kind ‘Proxy ((>) Int Bool)’,\r\n but ‘Data.Proxy.Proxy :: Proxy (Int > Bool)’ has kind ‘Proxy\r\n (Int > Bool)’\r\n • In the first argument of ‘f’, namely\r\n ‘(Proxy :: Proxy (Int > Bool))’\r\n In the expression: f (Proxy :: Proxy (Int > Bool))\r\n In an equation for ‘f’: f _ = f (Proxy :: Proxy (Int > Bool))\r\n}}}\r\nor with `fprintexplicitkinds fprintexplicitcoercions`:\r\n{{{\r\n • Expected kind ‘Proxy\r\n Symbol\r\n (((>) > <*>_N > <*>_N > U(hole:{aCy}, *, Symbol)_N) Int Bool)’,\r\n but ‘(Data.Proxy.Proxy) @ k_aCv @ t_aCw ::\r\n Proxy (Int > Bool)’ has kind ‘Proxy * (Int > Bool)’\r\n}}}\r\n\r\nAs Iavor, Richard and I discussed, this message has at least three separate problems:\r\n\r\n * It says `kind` when it should say `type`.\r\n\r\n * `((>) Int Bool)` is printed instead of `Int > Bool` (because there is a coercion hiding in the type).\r\n\r\n * The real error is the insoluble constraint `Symbol ~ *`, which is not reported at all!\r\n\r\nThe first two should be fairly easy to fix. For the third, when reporting insoluble constraints, we should prefer to report those on which no other constraints depend. (In this case, the presence of `hole:{aCy}` in the constraint is an explicit dependency on the other constraint.)\r\n\r\nI'll try to take a look at this. It is no doubt related to #11198.","type_of_failure":"OtherFailure","blocking":[]} >Adam GundryAdam Gundryhttps://gitlab.haskell.org/ghc/ghc//issues/11560panic: isInjectiveTyCon sees a TcTyCon20190707T18:29:48Zrwbartonpanic: isInjectiveTyCon sees a TcTyConI typed this into ghci and it panicked. Not sure whether the declaration is really valid anyways, but ghci shouldn't panic on it.
```
rwbarton@morphism:~/ghcnewest$ ./inplace/bin/ghcstage2 interactive
GHCi, version 8.1.20160201: http://www.haskell.org/ghc/ :? for help
Prelude> :set XTypeFamilies XTypeInType
Prelude> :m +Data.Kind
Prelude Data.Kind> type family T (l :: *) (k :: l) :: * where { T * Int = * }
ghcstage2: panic! (the 'impossible' happened)
(GHC version 8.1.20160201 for x86_64unknownlinux):
isInjectiveTyCon sees a TcTyCon T
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.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":"panic: isInjectiveTyCon sees a TcTyCon","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I typed this into ghci and it panicked. Not sure whether the declaration is really valid anyways, but ghci shouldn't panic on it.\r\n{{{\r\nrwbarton@morphism:~/ghcnewest$ ./inplace/bin/ghcstage2 interactive\r\nGHCi, version 8.1.20160201: http://www.haskell.org/ghc/ :? for help\r\nPrelude> :set XTypeFamilies XTypeInType\r\nPrelude> :m +Data.Kind\r\nPrelude Data.Kind> type family T (l :: *) (k :: l) :: * where { T * Int = * }\r\nghcstage2: panic! (the 'impossible' happened)\r\n (GHC version 8.1.20160201 for x86_64unknownlinux):\r\n\tisInjectiveTyCon sees a TcTyCon T\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >I typed this into ghci and it panicked. Not sure whether the declaration is really valid anyways, but ghci shouldn't panic on it.
```
rwbarton@morphism:~/ghcnewest$ ./inplace/bin/ghcstage2 interactive
GHCi, version 8.1.20160201: http://www.haskell.org/ghc/ :? for help
Prelude> :set XTypeFamilies XTypeInType
Prelude> :m +Data.Kind
Prelude Data.Kind> type family T (l :: *) (k :: l) :: * where { T * Int = * }
ghcstage2: panic! (the 'impossible' happened)
(GHC version 8.1.20160201 for x86_64unknownlinux):
isInjectiveTyCon sees a TcTyCon T
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.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":"panic: isInjectiveTyCon sees a TcTyCon","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I typed this into ghci and it panicked. Not sure whether the declaration is really valid anyways, but ghci shouldn't panic on it.\r\n{{{\r\nrwbarton@morphism:~/ghcnewest$ ./inplace/bin/ghcstage2 interactive\r\nGHCi, version 8.1.20160201: http://www.haskell.org/ghc/ :? for help\r\nPrelude> :set XTypeFamilies XTypeInType\r\nPrelude> :m +Data.Kind\r\nPrelude Data.Kind> type family T (l :: *) (k :: l) :: * where { T * Int = * }\r\nghcstage2: panic! (the 'impossible' happened)\r\n (GHC version 8.1.20160201 for x86_64unknownlinux):\r\n\tisInjectiveTyCon sees a TcTyCon T\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/11554Self quantification in GADT data declarations20200919T20:01:19ZRafbillSelf quantification in GADT data declarationsGHC hangs on this (it was panicking on the same code before : [https://github.com/goldfirere/ghc/issues/56](https://github.com/goldfirere/ghc/issues/56)(https://github.com/goldfirere/ghc/issues/56) :
```hs
{# LANGUAGE GADTs, TypeInType #}
import Data.Kind
data A :: Type where
B :: forall (a :: A). A
```
I guess the typechecker tries to infer the kind of A from the type of the constructors and hangs. Maybe recursive occurrences of a type as a kind in its constructors should only be allowed when its kind signature is specified and can be used to typecheck the constructors.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.1rc2 
 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":"Self quantification in GADT data declarations","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1rc2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"GHC hangs on this (it was panicking on the same code before : [https://github.com/goldfirere/ghc/issues/56](https://github.com/goldfirere/ghc/issues/56) :\r\n{{{#!hs\r\n{# LANGUAGE GADTs, TypeInType #}\r\nimport Data.Kind\r\ndata A :: Type where\r\n B :: forall (a :: A). A\r\n}}}\r\n\r\nI guess the typechecker tries to infer the kind of A from the type of the constructors and hangs. Maybe recursive occurrences of a type as a kind in its constructors should only be allowed when its kind signature is specified and can be used to typecheck the constructors.\r\n\r\n","type_of_failure":"OtherFailure","blocking":[]} >GHC hangs on this (it was panicking on the same code before : [https://github.com/goldfirere/ghc/issues/56](https://github.com/goldfirere/ghc/issues/56)(https://github.com/goldfirere/ghc/issues/56) :
```hs
{# LANGUAGE GADTs, TypeInType #}
import Data.Kind
data A :: Type where
B :: forall (a :: A). A
```
I guess the typechecker tries to infer the kind of A from the type of the constructors and hangs. Maybe recursive occurrences of a type as a kind in its constructors should only be allowed when its kind signature is specified and can be used to typecheck the constructors.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.1rc2 
 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":"Self quantification in GADT data declarations","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1rc2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"GHC hangs on this (it was panicking on the same code before : [https://github.com/goldfirere/ghc/issues/56](https://github.com/goldfirere/ghc/issues/56) :\r\n{{{#!hs\r\n{# LANGUAGE GADTs, TypeInType #}\r\nimport Data.Kind\r\ndata A :: Type where\r\n B :: forall (a :: A). A\r\n}}}\r\n\r\nI guess the typechecker tries to infer the kind of A from the type of the constructors and hangs. Maybe recursive occurrences of a type as a kind in its constructors should only be allowed when its kind signature is specified and can be used to typecheck the constructors.\r\n\r\n","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/11453Kinds in type synonym/data declarations can unexpectedly unify20190707T18:30:21ZRyan ScottKinds in type synonym/data declarations can unexpectedly unifyWhile trying out ideas to fix [this lens issue](https://github.com/ekmett/lens/issues/626), I noticed a couple of peculiar things about kinds in type synonym and data declarations. For example:
```
$ /opt/ghc/head/bin/ghci XTypeInType XRankNTypes XTypeOperators
GHCi, version 8.1.20160113: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/xnux/.ghci
λ> import Data.Kind
λ> type Wat (a :: k2) (b :: k3) = forall (f :: k1 > *). Either (f a) (f b)
λ> :i Wat
type Wat (a :: k1) (b :: k1) =
forall (f :: k1 > *). Either (f a) (f b)
 Defined at <interactive>:2:1
```
This is pretty odd for two reasons. One, the kind `k1` was never specified (either existentially or as a visible kind binder), so that definition should have been rejected. But even if we do use an existential kind:
```
λ> type Wat (a :: k2) (b :: k3) = forall k1 (f :: k1 > *). Either (f a) (f b)
λ> :i Wat
type Wat (a :: k1) (b :: k1) =
forall k2 (f :: k2 > *). Either (f a) (f b)
 Defined at <interactive>:4:1
```
We still see the second issue: GHC thinks that the type variables `a` and `b` have the same kind `k1`, when they should have separate kinds `k1` and `k2`! That behavior is very surprising to me, since it seems like GHC is choosing to unify two kind variables that should be rigid.
Note that this doesn't happen if you use explicit kind binders:
```
type Wat k2 k3 (a :: k2) (b :: k3) = forall k1 (f :: k1 > *). Either (f a) (f b)
<interactive>:6:74: error:
• Expected kind ‘k1’, but ‘a’ has kind ‘k2’
• In the first argument of ‘f’, namely ‘a’
In the first argument of ‘Either’, namely ‘f a’
In the type ‘forall k1 (f :: k1 > *). Either (f a) (f b)’
<interactive>:6:80: error:
• Expected kind ‘k1’, but ‘b’ has kind ‘k3’
• In the first argument of ‘f’, namely ‘b’
In the second argument of ‘Either’, namely ‘f b’
In the type ‘forall k1 (f :: k1 > *). Either (f a) (f b)’
```
only when the kinds are specified but not visible.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.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":"Kinds in type synonym/data declarations can unexpectedly unify","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":["goldfire"],"type":"Bug","description":"While trying out ideas to fix [https://github.com/ekmett/lens/issues/626 this lens issue], I noticed a couple of peculiar things about kinds in type synonym and data declarations. For example:\r\n\r\n{{{\r\n$ /opt/ghc/head/bin/ghci XTypeInType XRankNTypes XTypeOperators\r\nGHCi, version 8.1.20160113: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/xnux/.ghci\r\nλ> import Data.Kind\r\nλ> type Wat (a :: k2) (b :: k3) = forall (f :: k1 > *). Either (f a) (f b)\r\nλ> :i Wat\r\ntype Wat (a :: k1) (b :: k1) =\r\n forall (f :: k1 > *). Either (f a) (f b)\r\n  Defined at <interactive>:2:1\r\n}}}\r\n\r\nThis is pretty odd for two reasons. One, the kind {{{k1}}} was never specified (either existentially or as a visible kind binder), so that definition should have been rejected. But even if we do use an existential kind:\r\n\r\n{{{\r\nλ> type Wat (a :: k2) (b :: k3) = forall k1 (f :: k1 > *). Either (f a) (f b)\r\nλ> :i Wat\r\ntype Wat (a :: k1) (b :: k1) =\r\n forall k2 (f :: k2 > *). Either (f a) (f b)\r\n  Defined at <interactive>:4:1\r\n}}}\r\n\r\nWe still see the second issue: GHC thinks that the type variables `a` and `b` have the same kind `k1`, when they should have separate kinds `k1` and `k2`! That behavior is very surprising to me, since it seems like GHC is choosing to unify two kind variables that should be rigid.\r\n\r\nNote that this doesn't happen if you use explicit kind binders:\r\n\r\n{{{\r\ntype Wat k2 k3 (a :: k2) (b :: k3) = forall k1 (f :: k1 > *). Either (f a) (f b)\r\n\r\n<interactive>:6:74: error:\r\n • Expected kind ‘k1’, but ‘a’ has kind ‘k2’\r\n • In the first argument of ‘f’, namely ‘a’\r\n In the first argument of ‘Either’, namely ‘f a’\r\n In the type ‘forall k1 (f :: k1 > *). Either (f a) (f b)’\r\n\r\n<interactive>:6:80: error:\r\n • Expected kind ‘k1’, but ‘b’ has kind ‘k3’\r\n • In the first argument of ‘f’, namely ‘b’\r\n In the second argument of ‘Either’, namely ‘f b’\r\n In the type ‘forall k1 (f :: k1 > *). Either (f a) (f b)’\r\n}}}\r\n\r\nonly when the kinds are specified but not visible.","type_of_failure":"OtherFailure","blocking":[]} >While trying out ideas to fix [this lens issue](https://github.com/ekmett/lens/issues/626), I noticed a couple of peculiar things about kinds in type synonym and data declarations. For example:
```
$ /opt/ghc/head/bin/ghci XTypeInType XRankNTypes XTypeOperators
GHCi, version 8.1.20160113: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/xnux/.ghci
λ> import Data.Kind
λ> type Wat (a :: k2) (b :: k3) = forall (f :: k1 > *). Either (f a) (f b)
λ> :i Wat
type Wat (a :: k1) (b :: k1) =
forall (f :: k1 > *). Either (f a) (f b)
 Defined at <interactive>:2:1
```
This is pretty odd for two reasons. One, the kind `k1` was never specified (either existentially or as a visible kind binder), so that definition should have been rejected. But even if we do use an existential kind:
```
λ> type Wat (a :: k2) (b :: k3) = forall k1 (f :: k1 > *). Either (f a) (f b)
λ> :i Wat
type Wat (a :: k1) (b :: k1) =
forall k2 (f :: k2 > *). Either (f a) (f b)
 Defined at <interactive>:4:1
```
We still see the second issue: GHC thinks that the type variables `a` and `b` have the same kind `k1`, when they should have separate kinds `k1` and `k2`! That behavior is very surprising to me, since it seems like GHC is choosing to unify two kind variables that should be rigid.
Note that this doesn't happen if you use explicit kind binders:
```
type Wat k2 k3 (a :: k2) (b :: k3) = forall k1 (f :: k1 > *). Either (f a) (f b)
<interactive>:6:74: error:
• Expected kind ‘k1’, but ‘a’ has kind ‘k2’
• In the first argument of ‘f’, namely ‘a’
In the first argument of ‘Either’, namely ‘f a’
In the type ‘forall k1 (f :: k1 > *). Either (f a) (f b)’
<interactive>:6:80: error:
• Expected kind ‘k1’, but ‘b’ has kind ‘k3’
• In the first argument of ‘f’, namely ‘b’
In the second argument of ‘Either’, namely ‘f b’
In the type ‘forall k1 (f :: k1 > *). Either (f a) (f b)’
```
only when the kinds are specified but not visible.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.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":"Kinds in type synonym/data declarations can unexpectedly unify","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":["goldfire"],"type":"Bug","description":"While trying out ideas to fix [https://github.com/ekmett/lens/issues/626 this lens issue], I noticed a couple of peculiar things about kinds in type synonym and data declarations. For example:\r\n\r\n{{{\r\n$ /opt/ghc/head/bin/ghci XTypeInType XRankNTypes XTypeOperators\r\nGHCi, version 8.1.20160113: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/xnux/.ghci\r\nλ> import Data.Kind\r\nλ> type Wat (a :: k2) (b :: k3) = forall (f :: k1 > *). Either (f a) (f b)\r\nλ> :i Wat\r\ntype Wat (a :: k1) (b :: k1) =\r\n forall (f :: k1 > *). Either (f a) (f b)\r\n  Defined at <interactive>:2:1\r\n}}}\r\n\r\nThis is pretty odd for two reasons. One, the kind {{{k1}}} was never specified (either existentially or as a visible kind binder), so that definition should have been rejected. But even if we do use an existential kind:\r\n\r\n{{{\r\nλ> type Wat (a :: k2) (b :: k3) = forall k1 (f :: k1 > *). Either (f a) (f b)\r\nλ> :i Wat\r\ntype Wat (a :: k1) (b :: k1) =\r\n forall k2 (f :: k2 > *). Either (f a) (f b)\r\n  Defined at <interactive>:4:1\r\n}}}\r\n\r\nWe still see the second issue: GHC thinks that the type variables `a` and `b` have the same kind `k1`, when they should have separate kinds `k1` and `k2`! That behavior is very surprising to me, since it seems like GHC is choosing to unify two kind variables that should be rigid.\r\n\r\nNote that this doesn't happen if you use explicit kind binders:\r\n\r\n{{{\r\ntype Wat k2 k3 (a :: k2) (b :: k3) = forall k1 (f :: k1 > *). Either (f a) (f b)\r\n\r\n<interactive>:6:74: error:\r\n • Expected kind ‘k1’, but ‘a’ has kind ‘k2’\r\n • In the first argument of ‘f’, namely ‘a’\r\n In the first argument of ‘Either’, namely ‘f a’\r\n In the type ‘forall k1 (f :: k1 > *). Either (f a) (f b)’\r\n\r\n<interactive>:6:80: error:\r\n • Expected kind ‘k1’, but ‘b’ has kind ‘k3’\r\n • In the first argument of ‘f’, namely ‘b’\r\n In the second argument of ‘Either’, namely ‘f b’\r\n In the type ‘forall k1 (f :: k1 > *). Either (f a) (f b)’\r\n}}}\r\n\r\nonly when the kinds are specified but not visible.","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/11410Quantification over unlifted type variable20190707T18:30:32ZRichard Eisenbergrae@richarde.devQuantification over unlifted type variableThis silliness is accepted:
```
data X (a :: TYPE 'Unlifted) = X
```
I will fix.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.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":"Quantification over unlifted type variable","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"goldfire"},"version":"8.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This silliness is accepted:\r\n\r\n{{{\r\ndata X (a :: TYPE 'Unlifted) = X\r\n}}}\r\n\r\nI will fix.","type_of_failure":"OtherFailure","blocking":[]} >This silliness is accepted:
```
data X (a :: TYPE 'Unlifted) = X
```
I will fix.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.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":"Quantification over unlifted type variable","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"goldfire"},"version":"8.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This silliness is accepted:\r\n\r\n{{{\r\ndata X (a :: TYPE 'Unlifted) = X\r\n}}}\r\n\r\nI will fix.","type_of_failure":"OtherFailure","blocking":[]} >Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/17674Kill EQ120200518T17:02:46ZRichard Eisenbergrae@richarde.devKill EQ1Note [Respecting definitional equality] introduces invariant EQ1:
```
(EQ1) No decomposable CastTy to the left of an AppTy, where a decomposable
cast is one that relates either a FunTy to a FunTy or a
ForAllTy to a ForAllTy.
```
This invariant is a small pain to uphold. And perhaps we don't need to. If, instead, we modified `eqType` to look at the kind of arguments to `AppTy`s, then we wouldn't need EQ1, significantly simplifying `mkAppTy`. (Actually, it will just remove 2 lines. But it removes two calls to `decomposePiCos`. This will allow the one remaining call to this function to have more sway in the design of `decomposePiCos`, simplifying that bit of code, as well.)
Another nice benefit: by removing this invariant, we have an opportunity to explore different solutions to #17644, which hit a dead end in EQ1. See https://gitlab.haskell.org/ghc/ghc/issues/17644#note_245757.Note [Respecting definitional equality] introduces invariant EQ1:
```
(EQ1) No decomposable CastTy to the left of an AppTy, where a decomposable
cast is one that relates either a FunTy to a FunTy or a
ForAllTy to a ForAllTy.
```
This invariant is a small pain to uphold. And perhaps we don't need to. If, instead, we modified `eqType` to look at the kind of arguments to `AppTy`s, then we wouldn't need EQ1, significantly simplifying `mkAppTy`. (Actually, it will just remove 2 lines. But it removes two calls to `decomposePiCos`. This will allow the one remaining call to this function to have more sway in the design of `decomposePiCos`, simplifying that bit of code, as well.)
Another nice benefit: by removing this invariant, we have an opportunity to explore different solutions to #17644, which hit a dead end in EQ1. See https://gitlab.haskell.org/ghc/ghc/issues/17644#note_245757.Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/17567Never `Any`ify during kind inference20210111T13:09:30ZRichard Eisenbergrae@richarde.devNever `Any`ify during kind inference#14198 concludes with a new plan: never `Any`ify during kind inference. This ticket tracks this particular problem, separate from #14198.
Here are some examples of `Any`ification during kind inference:
#17301:
```hs
data B a
data TySing ty where
SB :: TySing (B a)
data ATySing where
MkATySing :: TySing ty > ATySing
type family Forget ty :: ATySing where
Forget (B a) = MkATySing SB
```
The RHS of that type family equation is really `MkATySing @alpha (SB @alpha)`, and the `alpha` gets zonked to `Any`.
#14198:
```hs
type T = forall a. Proxy a
```
The RHS of the type synonym is really `forall (a :: kappa). Proxy @kappa a`, and the `kappa` gets zonked to `Any`.
#17562:
```hs
class (forall a. a b ~ a c) => C b c
```
The superclass constraint is really `forall (a :: Type > kappa). (~) @kappa (a b) (a c))`, and the `kappa` gets zonked to `Any`.
We want to stop zonking to `Any`, preferring to error instead. But how should we implement?
* Option A: Use a new variant of `ZonkFlexi`, a choice carried around in a `ZonkEnv` that says what to do with empty metavariables. The new choice would cause an error. This new form of `ZonkFlexi` would be used in the final zonks in e.g. TcTyClsDecls. Open question: how to get a decent error message? I think we'd have to pass around the original, toplevel type in order to report it. By the time we have just the unbound metavariable, we have no context to report.
* Option B: Similar to (A), but don't report an error in the zonker. Instead, the new variant of `ZonkFlexi` would insert some magical error type. Then, the validity checker could do an early pass, looking for the error type; it can then report a nice error message.
* Option C: Look for all cases where `Any`ification might happen, and detect each one separately. This can produce lovely error messages. The solution for #17562 in !2313 does this. Perhaps we can pair this choice with a new `ZonkFlexi` that panics. That way, we'll know if we've missed a case.
* Simon below proposes Option D: Zap to `Type` instead of `Any`. I (Richard) view D as an addon to any of the above plans. Because `Type` is not always wellkinded, we can only zap to `Type` sometimes, and we still need to decide what we do at other times. Personally, I prefer not to treat `Type` specially with XPolyKinds` enabled, and so I'd prefer that we don't do this.
* EDIT: Also, we can consider Option E: Report poor error messages, saying something about an unconstrained kind variable. Users would be helped only via the context (the "In the data declaration for `Wurble`" bits). This would mean building up useful contexts in the zonker.
* Option F: The new constructor for `ZonkFlexi` could carry the toplevel type we are trying to zonk. If we encounter an unconstrained metavariable, we just look at this bit of context to produce the error message. Perhaps this could be combined with the contextbuilding in Option E for good effect. This is the first solution I'm actually happy with.
Thoughts?#14198 concludes with a new plan: never `Any`ify during kind inference. This ticket tracks this particular problem, separate from #14198.
Here are some examples of `Any`ification during kind inference:
#17301:
```hs
data B a
data TySing ty where
SB :: TySing (B a)
data ATySing where
MkATySing :: TySing ty > ATySing
type family Forget ty :: ATySing where
Forget (B a) = MkATySing SB
```
The RHS of that type family equation is really `MkATySing @alpha (SB @alpha)`, and the `alpha` gets zonked to `Any`.
#14198:
```hs
type T = forall a. Proxy a
```
The RHS of the type synonym is really `forall (a :: kappa). Proxy @kappa a`, and the `kappa` gets zonked to `Any`.
#17562:
```hs
class (forall a. a b ~ a c) => C b c
```
The superclass constraint is really `forall (a :: Type > kappa). (~) @kappa (a b) (a c))`, and the `kappa` gets zonked to `Any`.
We want to stop zonking to `Any`, preferring to error instead. But how should we implement?
* Option A: Use a new variant of `ZonkFlexi`, a choice carried around in a `ZonkEnv` that says what to do with empty metavariables. The new choice would cause an error. This new form of `ZonkFlexi` would be used in the final zonks in e.g. TcTyClsDecls. Open question: how to get a decent error message? I think we'd have to pass around the original, toplevel type in order to report it. By the time we have just the unbound metavariable, we have no context to report.
* Option B: Similar to (A), but don't report an error in the zonker. Instead, the new variant of `ZonkFlexi` would insert some magical error type. Then, the validity checker could do an early pass, looking for the error type; it can then report a nice error message.
* Option C: Look for all cases where `Any`ification might happen, and detect each one separately. This can produce lovely error messages. The solution for #17562 in !2313 does this. Perhaps we can pair this choice with a new `ZonkFlexi` that panics. That way, we'll know if we've missed a case.
* Simon below proposes Option D: Zap to `Type` instead of `Any`. I (Richard) view D as an addon to any of the above plans. Because `Type` is not always wellkinded, we can only zap to `Type` sometimes, and we still need to decide what we do at other times. Personally, I prefer not to treat `Type` specially with XPolyKinds` enabled, and so I'd prefer that we don't do this.
* EDIT: Also, we can consider Option E: Report poor error messages, saying something about an unconstrained kind variable. Users would be helped only via the context (the "In the data declaration for `Wurble`" bits). This would mean building up useful contexts in the zonker.
* Option F: The new constructor for `ZonkFlexi` could carry the toplevel type we are trying to zonk. If we encounter an unconstrained metavariable, we just look at this bit of context to produce the error message. Perhaps this could be combined with the contextbuilding in Option E for good effect. This is the first solution I'm actually happy with.
Thoughts?https://gitlab.haskell.org/ghc/ghc//issues/17368Implement homogeneous equality20200310T14:21:59ZRichard Eisenbergrae@richarde.devImplement homogeneous equalityAs observed in [two](https://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1076&context=compsci_pubs) [papers](https://richarde.dev/papers/2019/deproles/deproles.pdf), the primitive equality type in GHC can be made homogeneous. This is both a simplification over the status quo (heterogeneous equality) and an important step toward implementing dependent types.
This ticket is to track this change.
Step 1: Modify the typechecker to use predicates instead of types internally. This will essentially be a glorification of `PredTree` (renamed `Pred`), and a `CtEvidence` will now store a `Pred`, not a `PredType`.
See also https://gitlab.haskell.org/ghc/ghc/wikis/dependenthaskell/phase2, which has much discussion.As observed in [two](https://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1076&context=compsci_pubs) [papers](https://richarde.dev/papers/2019/deproles/deproles.pdf), the primitive equality type in GHC can be made homogeneous. This is both a simplification over the status quo (heterogeneous equality) and an important step toward implementing dependent types.
This ticket is to track this change.
Step 1: Modify the typechecker to use predicates instead of types internally. This will essentially be a glorification of `PredTree` (renamed `Pred`), and a `CtEvidence` will now store a `Pred`, not a `PredType`.
See also https://gitlab.haskell.org/ghc/ghc/wikis/dependenthaskell/phase2, which has much discussion.Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/15497Coercion Quantification20190707T18:04:29ZNingning XieCoercion QuantificationAs described in [https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Phase2](https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Phase2).
We would like to have coercion quantifications back in Haskell Core language.
This means in Core we can define types like
```hs
\/ (a: k1) .
\/ (co : k1 ~ k2)  an explicit quantification for the coercion
> (a > co)  use the name for an explicit cast
> ...
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  
 Type  Task 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Coercion Quantification","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Task","description":"As described in [https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Phase2].\r\n\r\nWe would like to have coercion quantifications back in Haskell Core language.\r\n\r\nThis means in Core we can define types like\r\n\r\n{{{#!hs\r\n\\/ (a: k1) . \r\n \\/ (co : k1 ~ k2)  an explicit quantification for the coercion\r\n > (a > co)  use the name for an explicit cast\r\n > ...\r\n}}}\r\n","type_of_failure":"OtherFailure","blocking":[]} >As described in [https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Phase2](https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Phase2).
We would like to have coercion quantifications back in Haskell Core language.
This means in Core we can define types like
```hs
\/ (a: k1) .
\/ (co : k1 ~ k2)  an explicit quantification for the coercion
> (a > co)  use the name for an explicit cast
> ...
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  
 Type  Task 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Coercion Quantification","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Task","description":"As described in [https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Phase2].\r\n\r\nWe would like to have coercion quantifications back in Haskell Core language.\r\n\r\nThis means in Core we can define types like\r\n\r\n{{{#!hs\r\n\\/ (a: k1) . \r\n \\/ (co : k1 ~ k2)  an explicit quantification for the coercion\r\n > (a > co)  use the name for an explicit cast\r\n > ...\r\n}}}\r\n","type_of_failure":"OtherFailure","blocking":[]} >Ningning XieNingning Xiehttps://gitlab.haskell.org/ghc/ghc//issues/14119Refactor type patterns20190707T18:18:23ZRichard Eisenbergrae@richarde.devRefactor type patternsType patterns are used in instance heads: class instances, type instances, and data/newtype instances. These type patterns differ from ordinary types in several ways:
 They must never mention a `forall`.
 They must never mention a context. (The context in a class instance head is a different part of the instance construct.)
 They must never mention a type family.
Types that appear as arguments on the LHS of a RULE should also be type patterns.
Type patterns are used in GHC differently than types as well: we should match only against patterns, never ordinary types.
I thus propose that a new datatype within GHC to store type patterns. I'll call it `TyPat` here, but perhaps a longer name is better. The matcher (in the `Unify` module) would then take a `TyPat` parameter, making clear which type is the template and which is the concrete instantiation.
We could have a new algorithm to typecheck/desugar source syntax into patterns. This new algorithm could accommodate issues like those mentioned in [ticket:14038\#comment:140786](https://gitlab.haskell.org//ghc/ghc/issues/14038#note_140786). It could also avoid ever putting a type family in a kind parameter, which would fix #12564. Separating out checking type patterns from proper types could also improve GADT pattern matching in types, which is currently more like "wobbly types" than OutsideIn.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1 
 Type  Task 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  #12564, #14038 
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Refactor type patterns","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Task","description":"Type patterns are used in instance heads: class instances, type instances, and data/newtype instances. These type patterns differ from ordinary types in several ways:\r\n\r\n * They must never mention a `forall`.\r\n * They must never mention a context. (The context in a class instance head is a different part of the instance construct.)\r\n * They must never mention a type family.\r\n\r\nTypes that appear as arguments on the LHS of a RULE should also be type patterns.\r\n\r\nType patterns are used in GHC differently than types as well: we should match only against patterns, never ordinary types.\r\n\r\nI thus propose that a new datatype within GHC to store type patterns. I'll call it `TyPat` here, but perhaps a longer name is better. The matcher (in the `Unify` module) would then take a `TyPat` parameter, making clear which type is the template and which is the concrete instantiation.\r\n\r\nWe could have a new algorithm to typecheck/desugar source syntax into patterns. This new algorithm could accommodate issues like those mentioned in comment:6:ticket:14038. It could also avoid ever putting a type family in a kind parameter, which would fix #12564. Separating out checking type patterns from proper types could also improve GADT pattern matching in types, which is currently more like \"wobbly types\" than OutsideIn.","type_of_failure":"OtherFailure","blocking":[12564,14038]} >Type patterns are used in instance heads: class instances, type instances, and data/newtype instances. These type patterns differ from ordinary types in several ways:
 They must never mention a `forall`.
 They must never mention a context. (The context in a class instance head is a different part of the instance construct.)
 They must never mention a type family.
Types that appear as arguments on the LHS of a RULE should also be type patterns.
Type patterns are used in GHC differently than types as well: we should match only against patterns, never ordinary types.
I thus propose that a new datatype within GHC to store type patterns. I'll call it `TyPat` here, but perhaps a longer name is better. The matcher (in the `Unify` module) would then take a `TyPat` parameter, making clear which type is the template and which is the concrete instantiation.
We could have a new algorithm to typecheck/desugar source syntax into patterns. This new algorithm could accommodate issues like those mentioned in [ticket:14038\#comment:140786](https://gitlab.haskell.org//ghc/ghc/issues/14038#note_140786). It could also avoid ever putting a type family in a kind parameter, which would fix #12564. Separating out checking type patterns from proper types could also improve GADT pattern matching in types, which is currently more like "wobbly types" than OutsideIn.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1 
 Type  Task 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  #12564, #14038 
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Refactor type patterns","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Task","description":"Type patterns are used in instance heads: class instances, type instances, and data/newtype instances. These type patterns differ from ordinary types in several ways:\r\n\r\n * They must never mention a `forall`.\r\n * They must never mention a context. (The context in a class instance head is a different part of the instance construct.)\r\n * They must never mention a type family.\r\n\r\nTypes that appear as arguments on the LHS of a RULE should also be type patterns.\r\n\r\nType patterns are used in GHC differently than types as well: we should match only against patterns, never ordinary types.\r\n\r\nI thus propose that a new datatype within GHC to store type patterns. I'll call it `TyPat` here, but perhaps a longer name is better. The matcher (in the `Unify` module) would then take a `TyPat` parameter, making clear which type is the template and which is the concrete instantiation.\r\n\r\nWe could have a new algorithm to typecheck/desugar source syntax into patterns. This new algorithm could accommodate issues like those mentioned in comment:6:ticket:14038. It could also avoid ever putting a type family in a kind parameter, which would fix #12564. Separating out checking type patterns from proper types could also improve GADT pattern matching in types, which is currently more like \"wobbly types\" than OutsideIn.","type_of_failure":"OtherFailure","blocking":[12564,14038]} >Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/13408Consider inferring a higherrank kind for type synonyms20200925T17:22:29ZRichard Eisenbergrae@richarde.devConsider inferring a higherrank kind for type synonymsIn terms, a definition comprising one nonrecursive equation may have a higherrank type inferred. For example:
```hs
f :: (forall a. a > a > a) > Int
f z = z 0 1
g = f
```
`g` gets an inferred type equal to `f`'s. However, this fails at the type level:
```hs
type F (z :: forall a. a > a > a) = z 0 1
type G = F
```
If anything is strange here, it's that the termlevel definition is accepted. GHC should not be in the business of inferring higherrank types. But there is an exception for definitions comprising one nonrecursive equation.
This ticket proposes expanding this behavior to the type level, allowing `G` to be accepted.
This is spun off from #13399, but is not tightly coupled to that ticket.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.1 
 Type  FeatureRequest 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Consider inferring a higherrank kind for type synonyms","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"In terms, a definition comprising one nonrecursive equation may have a higherrank type inferred. For example:\r\n\r\n{{{#!hs\r\nf :: (forall a. a > a > a) > Int\r\nf z = z 0 1\r\n\r\ng = f\r\n}}}\r\n\r\n`g` gets an inferred type equal to `f`'s. However, this fails at the type level:\r\n\r\n{{{#!hs\r\ntype F (z :: forall a. a > a > a) = z 0 1\r\n\r\ntype G = F\r\n}}}\r\n\r\nIf anything is strange here, it's that the termlevel definition is accepted. GHC should not be in the business of inferring higherrank types. But there is an exception for definitions comprising one nonrecursive equation.\r\n\r\nThis ticket proposes expanding this behavior to the type level, allowing `G` to be accepted.\r\n\r\nThis is spun off from #13399, but is not tightly coupled to that ticket.","type_of_failure":"OtherFailure","blocking":[]} >In terms, a definition comprising one nonrecursive equation may have a higherrank type inferred. For example:
```hs
f :: (forall a. a > a > a) > Int
f z = z 0 1
g = f
```
`g` gets an inferred type equal to `f`'s. However, this fails at the type level:
```hs
type F (z :: forall a. a > a > a) = z 0 1
type G = F
```
If anything is strange here, it's that the termlevel definition is accepted. GHC should not be in the business of inferring higherrank types. But there is an exception for definitions comprising one nonrecursive equation.
This ticket proposes expanding this behavior to the type level, allowing `G` to be accepted.
This is spun off from #13399, but is not tightly coupled to that ticket.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.1 
 Type  FeatureRequest 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Consider inferring a higherrank kind for type synonyms","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"In terms, a definition comprising one nonrecursive equation may have a higherrank type inferred. For example:\r\n\r\n{{{#!hs\r\nf :: (forall a. a > a > a) > Int\r\nf z = z 0 1\r\n\r\ng = f\r\n}}}\r\n\r\n`g` gets an inferred type equal to `f`'s. However, this fails at the type level:\r\n\r\n{{{#!hs\r\ntype F (z :: forall a. a > a > a) = z 0 1\r\n\r\ntype G = F\r\n}}}\r\n\r\nIf anything is strange here, it's that the termlevel definition is accepted. GHC should not be in the business of inferring higherrank types. But there is an exception for definitions comprising one nonrecursive equation.\r\n\r\nThis ticket proposes expanding this behavior to the type level, allowing `G` to be accepted.\r\n\r\nThis is spun off from #13399, but is not tightly coupled to that ticket.","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/12029Notify user to import * from Data.Kind with TypeInType on20190707T18:27:55ZIcelandjackNotify user to import * from Data.Kind with TypeInType onWith `TypeInType` asking for the kind of `*` gives the user a warning to import it
```
ghci> :set XTypeInType
ghci> :k *
<interactive>:1:1: error:
Not in scope: type constructor or class ‘*’
NB: With TypeInType, you must import * from Data.Kind
<interactive>:1:1: error:
Illegal operator ‘*’ in type ‘*’
Use TypeOperators to allow operators in types
<interactive>:1:1: error: Operator applied to too few arguments: *
```
Should a similar warning be issued when she asks for information on it
```
ghci> :i *
class Num a where
...
(*) :: a > a > a
...
 Defined in ‘GHC.Num’
infixl 7 *
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.1 
 Type  FeatureRequest 
 TypeOfFailure  OtherFailure 
 Priority  lowest 
 Resolution  Unresolved 
 Component  GHCi 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Notify user to import * from Data.Kind with TypeInType on","status":"New","operating_system":"","component":"GHCi","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"With `TypeInType` asking for the kind of `*` gives the user a warning to import it\r\n\r\n{{{\r\nghci> :set XTypeInType \r\nghci> :k *\r\n\r\n<interactive>:1:1: error:\r\n Not in scope: type constructor or class ‘*’\r\n NB: With TypeInType, you must import * from Data.Kind\r\n\r\n<interactive>:1:1: error:\r\n Illegal operator ‘*’ in type ‘*’\r\n Use TypeOperators to allow operators in types\r\n\r\n<interactive>:1:1: error: Operator applied to too few arguments: *\r\n}}}\r\n\r\nShould a similar warning be issued when she asks for information on it\r\n\r\n{{{\r\nghci> :i *\r\nclass Num a where\r\n ...\r\n (*) :: a > a > a\r\n ...\r\n  Defined in ‘GHC.Num’\r\ninfixl 7 *\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >With `TypeInType` asking for the kind of `*` gives the user a warning to import it
```
ghci> :set XTypeInType
ghci> :k *
<interactive>:1:1: error:
Not in scope: type constructor or class ‘*’
NB: With TypeInType, you must import * from Data.Kind
<interactive>:1:1: error:
Illegal operator ‘*’ in type ‘*’
Use TypeOperators to allow operators in types
<interactive>:1:1: error: Operator applied to too few arguments: *
```
Should a similar warning be issued when she asks for information on it
```
ghci> :i *
class Num a where
...
(*) :: a > a > a
...
 Defined in ‘GHC.Num’
infixl 7 *
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.1 
 Type  FeatureRequest 
 TypeOfFailure  OtherFailure 
 Priority  lowest 
 Resolution  Unresolved 
 Component  GHCi 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Notify user to import * from Data.Kind with TypeInType on","status":"New","operating_system":"","component":"GHCi","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"With `TypeInType` asking for the kind of `*` gives the user a warning to import it\r\n\r\n{{{\r\nghci> :set XTypeInType \r\nghci> :k *\r\n\r\n<interactive>:1:1: error:\r\n Not in scope: type constructor or class ‘*’\r\n NB: With TypeInType, you must import * from Data.Kind\r\n\r\n<interactive>:1:1: error:\r\n Illegal operator ‘*’ in type ‘*’\r\n Use TypeOperators to allow operators in types\r\n\r\n<interactive>:1:1: error: Operator applied to too few arguments: *\r\n}}}\r\n\r\nShould a similar warning be issued when she asks for information on it\r\n\r\n{{{\r\nghci> :i *\r\nclass Num a where\r\n ...\r\n (*) :: a > a > a\r\n ...\r\n  Defined in ‘GHC.Num’\r\ninfixl 7 *\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >johnleojohnleohttps://gitlab.haskell.org/ghc/ghc//issues/11962Support induction recursion20200106T11:26:23ZRichard Eisenbergrae@richarde.devSupport induction recursionNow that we have `XTypeInType`, let's take it a step further and allow induction recursion. This feature exists in Agda and Idris. Here is a short example of what can be done in Agda:
```
mutual
 Codes for types.
data U : Set where
nat : U
pi : (a : U) → (El a → U) → U
 A function that interprets codes as actual types.
El : U → Set
El nat = ℕ
El (pi a b) = (x : El a) → El (b x)
```
Note that the `U` datatype and the `El` function depend on each other. But if you look more closely, the header for `U` does not depend on `El`; only the constructors of `U` depend on `El`. So if we typecheck `U : Set` first, then `El : U → Set`, then the constructors of `U`, then the equations of `El`, we're OK.
Translation into Haskell:
```
import Data.Kind
data family Sing (a :: k)  we still require singletons
data U :: Type where
Nat :: U
Pi :: Sing (a :: U) > (El a > U) > U
type family El (u :: U) :: Type where
El 'Nat = Int
El (Pi a b) = forall (x :: El a). Sing x > El (b x)
```
This currently errors with
```
• Type constructor ‘U’ cannot be used here
(it is defined and used in the same recursive group)
• In the kind ‘U’
```
It needn't error. (I'm cheating a bit here, because for unrelated reasons, we can't return a `forall` on the righthand side of a type family. But that's not the issue at hand.)
I have some very sketchy notes on how we might do this [here](https://gitlab.haskell.org/ghc/ghc/wikis/dependenthaskell/internal#separatingtypesignaturesfromdefinitions).
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.1 
 Type  FeatureRequest 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Support induction recursion","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"Now that we have `XTypeInType`, let's take it a step further and allow induction recursion. This feature exists in Agda and Idris. Here is a short example of what can be done in Agda:\r\n\r\n{{{\r\n mutual\r\n  Codes for types.\r\n\r\n data U : Set where\r\n nat : U\r\n pi : (a : U) → (El a → U) → U\r\n\r\n  A function that interprets codes as actual types.\r\n\r\n El : U → Set\r\n El nat = ℕ\r\n El (pi a b) = (x : El a) → El (b x)\r\n}}}\r\n\r\nNote that the `U` datatype and the `El` function depend on each other. But if you look more closely, the header for `U` does not depend on `El`; only the constructors of `U` depend on `El`. So if we typecheck `U : Set` first, then `El : U → Set`, then the constructors of `U`, then the equations of `El`, we're OK.\r\n\r\nTranslation into Haskell:\r\n\r\n{{{\r\nimport Data.Kind\r\n\r\ndata family Sing (a :: k)  we still require singletons\r\n\r\ndata U :: Type where\r\n Nat :: U\r\n Pi :: Sing (a :: U) > (El a > U) > U\r\n\r\ntype family El (u :: U) :: Type where\r\n El 'Nat = Int\r\n El (Pi a b) = forall (x :: El a). Sing x > El (b x)\r\n}}}\r\n\r\nThis currently errors with\r\n\r\n{{{\r\n • Type constructor ‘U’ cannot be used here\r\n (it is defined and used in the same recursive group)\r\n • In the kind ‘U’\r\n}}}\r\n\r\nIt needn't error. (I'm cheating a bit here, because for unrelated reasons, we can't return a `forall` on the righthand side of a type family. But that's not the issue at hand.)\r\n\r\nI have some very sketchy notes on how we might do this [wiki:DependentHaskell/Internal#Separatingtypesignaturesfromdefinitions here].","type_of_failure":"OtherFailure","blocking":[]} >Now that we have `XTypeInType`, let's take it a step further and allow induction recursion. This feature exists in Agda and Idris. Here is a short example of what can be done in Agda:
```
mutual
 Codes for types.
data U : Set where
nat : U
pi : (a : U) → (El a → U) → U
 A function that interprets codes as actual types.
El : U → Set
El nat = ℕ
El (pi a b) = (x : El a) → El (b x)
```
Note that the `U` datatype and the `El` function depend on each other. But if you look more closely, the header for `U` does not depend on `El`; only the constructors of `U` depend on `El`. So if we typecheck `U : Set` first, then `El : U → Set`, then the constructors of `U`, then the equations of `El`, we're OK.
Translation into Haskell:
```
import Data.Kind
data family Sing (a :: k)  we still require singletons
data U :: Type where
Nat :: U
Pi :: Sing (a :: U) > (El a > U) > U
type family El (u :: U) :: Type where
El 'Nat = Int
El (Pi a b) = forall (x :: El a). Sing x > El (b x)
```
This currently errors with
```
• Type constructor ‘U’ cannot be used here
(it is defined and used in the same recursive group)
• In the kind ‘U’
```
It needn't error. (I'm cheating a bit here, because for unrelated reasons, we can't return a `forall` on the righthand side of a type family. But that's not the issue at hand.)
I have some very sketchy notes on how we might do this [here](https://gitlab.haskell.org/ghc/ghc/wikis/dependenthaskell/internal#separatingtypesignaturesfromdefinitions).
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.1 
 Type  FeatureRequest 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Support induction recursion","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"Now that we have `XTypeInType`, let's take it a step further and allow induction recursion. This feature exists in Agda and Idris. Here is a short example of what can be done in Agda:\r\n\r\n{{{\r\n mutual\r\n  Codes for types.\r\n\r\n data U : Set where\r\n nat : U\r\n pi : (a : U) → (El a → U) → U\r\n\r\n  A function that interprets codes as actual types.\r\n\r\n El : U → Set\r\n El nat = ℕ\r\n El (pi a b) = (x : El a) → El (b x)\r\n}}}\r\n\r\nNote that the `U` datatype and the `El` function depend on each other. But if you look more closely, the header for `U` does not depend on `El`; only the constructors of `U` depend on `El`. So if we typecheck `U : Set` first, then `El : U → Set`, then the constructors of `U`, then the equations of `El`, we're OK.\r\n\r\nTranslation into Haskell:\r\n\r\n{{{\r\nimport Data.Kind\r\n\r\ndata family Sing (a :: k)  we still require singletons\r\n\r\ndata U :: Type where\r\n Nat :: U\r\n Pi :: Sing (a :: U) > (El a > U) > U\r\n\r\ntype family El (u :: U) :: Type where\r\n El 'Nat = Int\r\n El (Pi a b) = forall (x :: El a). Sing x > El (b x)\r\n}}}\r\n\r\nThis currently errors with\r\n\r\n{{{\r\n • Type constructor ‘U’ cannot be used here\r\n (it is defined and used in the same recursive group)\r\n • In the kind ‘U’\r\n}}}\r\n\r\nIt needn't error. (I'm cheating a bit here, because for unrelated reasons, we can't return a `forall` on the righthand side of a type family. But that's not the issue at hand.)\r\n\r\nI have some very sketchy notes on how we might do this [wiki:DependentHaskell/Internal#Separatingtypesignaturesfromdefinitions here].","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/19196TypeInType prevents Typeable from being resolved from a given20210111T03:19:52ZSerge KosyrevTypeInType prevents Typeable from being resolved from a givenThe following program is accepted without `TypeInType` by GHC 8.10.2:
```haskell
{# LANGUAGE DataKinds #}
{# LANGUAGE GADTs #}
{# LANGUAGE KindSignatures #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE UndecidableInstances #}
import Data.Dynamic
import Type.Reflection
data Liveness
= forall t. Live t
data IOA (l :: Liveness) where
IOE :: IOA (Live t)
data LTag (l :: Liveness) where
LLive :: Typeable t => TypeRep t > LTag (Live t)
reconstruct :: Dynamic > LTag l > ()
reconstruct dyn l@LLive{} =
case l of
(LLive tr :: LTag (Live t)) >
undefined $ withTypeable tr $
(fromDynamic dyn :: Maybe (IOA (Live t)))
main :: IO ()
main = undefined
```
It is, however, rejected with `TypeInType`, as follows:
```haskell
common/src/Dom/Pipe/IOA.hs:26:17: error:
• Could not deduce (Typeable t) arising from a use of ‘fromDynamic’
from the context: (l ~ 'Live t1, Typeable t1)
bound by a pattern with constructor:
LLive :: forall t1 (t2 :: t1).
Typeable t2 =>
TypeRep t2 > LTag ('Live t2),
in an equation for ‘reconstruct’
at common/src/Dom/Pipe/IOA.hs:22:1925
or from: ('Live t1 ~ 'Live t3, Typeable t3)
bound by a pattern with constructor:
LLive :: forall t1 (t2 :: t1).
Typeable t2 =>
TypeRep t2 > LTag ('Live t2),
in a case alternative
at common/src/Dom/Pipe/IOA.hs:24:1017
or from: Typeable t3
bound by a type expected by the context:
Typeable t3 => Maybe (IOA ('Live t1))
at common/src/Dom/Pipe/IOA.hs:26:1656
• In the second argument of ‘($)’, namely
‘(fromDynamic dyn :: Maybe (IOA (Live t)))’
In the second argument of ‘($)’, namely
‘withTypeable tr $ (fromDynamic dyn :: Maybe (IOA (Live t)))’
In the expression:
undefined
$ withTypeable tr $ (fromDynamic dyn :: Maybe (IOA (Live t)))

26  (fromDynamic dyn :: Maybe (IOA (Live t)))
 ^^^^^^^^^^^^^^^
```
Potentially related to #16627The following program is accepted without `TypeInType` by GHC 8.10.2:
```haskell
{# LANGUAGE DataKinds #}
{# LANGUAGE GADTs #}
{# LANGUAGE KindSignatures #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE UndecidableInstances #}
import Data.Dynamic
import Type.Reflection
data Liveness
= forall t. Live t
data IOA (l :: Liveness) where
IOE :: IOA (Live t)
data LTag (l :: Liveness) where
LLive :: Typeable t => TypeRep t > LTag (Live t)
reconstruct :: Dynamic > LTag l > ()
reconstruct dyn l@LLive{} =
case l of
(LLive tr :: LTag (Live t)) >
undefined $ withTypeable tr $
(fromDynamic dyn :: Maybe (IOA (Live t)))
main :: IO ()
main = undefined
```
It is, however, rejected with `TypeInType`, as follows:
```haskell
common/src/Dom/Pipe/IOA.hs:26:17: error:
• Could not deduce (Typeable t) arising from a use of ‘fromDynamic’
from the context: (l ~ 'Live t1, Typeable t1)
bound by a pattern with constructor:
LLive :: forall t1 (t2 :: t1).
Typeable t2 =>
TypeRep t2 > LTag ('Live t2),
in an equation for ‘reconstruct’
at common/src/Dom/Pipe/IOA.hs:22:1925
or from: ('Live t1 ~ 'Live t3, Typeable t3)
bound by a pattern with constructor:
LLive :: forall t1 (t2 :: t1).
Typeable t2 =>
TypeRep t2 > LTag ('Live t2),
in a case alternative
at common/src/Dom/Pipe/IOA.hs:24:1017
or from: Typeable t3
bound by a type expected by the context:
Typeable t3 => Maybe (IOA ('Live t1))
at common/src/Dom/Pipe/IOA.hs:26:1656
• In the second argument of ‘($)’, namely
‘(fromDynamic dyn :: Maybe (IOA (Live t)))’
In the second argument of ‘($)’, namely
‘withTypeable tr $ (fromDynamic dyn :: Maybe (IOA (Live t)))’
In the expression:
undefined
$ withTypeable tr $ (fromDynamic dyn :: Maybe (IOA (Live t)))

26  (fromDynamic dyn :: Maybe (IOA (Live t)))
 ^^^^^^^^^^^^^^^
```
Potentially related to #16627https://gitlab.haskell.org/ghc/ghc//issues/18753Tighten up the treatment of loose types in the solver20200930T16:21:20ZRichard Eisenbergrae@richarde.devTighten up the treatment of loose types in the solver`GHC.Tc.Solver.Monad` includes
```
Note [Use loose types in inert set]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Say we know (Eq (a > c1)) and we need (Eq (a > c2)). One is clearly
solvable from the other. So, we do lookup in the inert set using
loose types, which omits the kindcheck.
We must be careful when using the result of a lookup because it may
not match the requested info exactly!
```
There are several problems.
* We aren't always careful. For example, `lookupInInerts` tries `lookupSolvedDict` and then `lookupInertDict`, both of which use this "loose" lookup. Yet the result of `lookupInInerts` just uses the result, without any special handling to take the fact that the types might not match exactly.
* The Note doesn't actually make sense. The only difference between `Eq (a > c1)` and `Eq (a > c2)` is the coercion. But I sincerely hope we never care about the contents of a coercion. So even if we use evidence of type `Eq (a > c1)` where GHC is expecting `Eq (a > c2)` (assuming `c1` and `c2` have the same type), all will be well.
* What I think the Note is trying to say will never happen. That is, the actual implementation of the inertset lookup tries to match types while ignoring their kinds. (Normal type matching requires that the kind matches also.) So a better example would be something like comparing `Eq (a :: k1)` with `Eq (a :: k2)`. But that's impossible, even with casts: all type families and classes have *closed* kinds, meaning that any variables that appear in the kinds of arguments must themselves be earlier arguments. In other words, if I have welltyped `T blah1 (... :: kind1)` and `T blah2 (... :: kind2)`, then either `kind1` equals `kind2` or `blah1` and `blah2` must differ. We use this logic elsewhere  in particular, in the pure unifier.
Conclusions:
* Using "loose" matching (that is, ignoring kinds) in the solver is the right thing.
* We should update the Note with my argument above.
* No special care needs to be taken when using loose matching in this way. This means we can drop a few redundant equality checks (e.g. in `lookupFlatCache`).
I'm pretty confident about this all, but I'd like a doublecheck before I commit a fix.`GHC.Tc.Solver.Monad` includes
```
Note [Use loose types in inert set]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Say we know (Eq (a > c1)) and we need (Eq (a > c2)). One is clearly
solvable from the other. So, we do lookup in the inert set using
loose types, which omits the kindcheck.
We must be careful when using the result of a lookup because it may
not match the requested info exactly!
```
There are several problems.
* We aren't always careful. For example, `lookupInInerts` tries `lookupSolvedDict` and then `lookupInertDict`, both of which use this "loose" lookup. Yet the result of `lookupInInerts` just uses the result, without any special handling to take the fact that the types might not match exactly.
* The Note doesn't actually make sense. The only difference between `Eq (a > c1)` and `Eq (a > c2)` is the coercion. But I sincerely hope we never care about the contents of a coercion. So even if we use evidence of type `Eq (a > c1)` where GHC is expecting `Eq (a > c2)` (assuming `c1` and `c2` have the same type), all will be well.
* What I think the Note is trying to say will never happen. That is, the actual implementation of the inertset lookup tries to match types while ignoring their kinds. (Normal type matching requires that the kind matches also.) So a better example would be something like comparing `Eq (a :: k1)` with `Eq (a :: k2)`. But that's impossible, even with casts: all type families and classes have *closed* kinds, meaning that any variables that appear in the kinds of arguments must themselves be earlier arguments. In other words, if I have welltyped `T blah1 (... :: kind1)` and `T blah2 (... :: kind2)`, then either `kind1` equals `kind2` or `blah1` and `blah2` must differ. We use this logic elsewhere  in particular, in the pure unifier.
Conclusions:
* Using "loose" matching (that is, ignoring kinds) in the solver is the right thing.
* We should update the Note with my argument above.
* No special care needs to be taken when using loose matching in this way. This means we can drop a few redundant equality checks (e.g. in `lookupFlatCache`).
I'm pretty confident about this all, but I'd like a doublecheck before I commit a fix.https://gitlab.haskell.org/ghc/ghc//issues/18689Why check for fdefertypeerrors in metaTyVarUpdateOK?20201222T13:22:39ZRichard Eisenbergrae@richarde.devWhy check for fdefertypeerrors in metaTyVarUpdateOK?Function `checkTypeEq` changes its behavior depending on the presence of `fdefertypeerrors` in an obscure case around heterogeneous equalities; see the code in `go_co`. This is undocumented (in the code), and neither Simon nor I can figure out why it's done.
Task: figure this out, and either document or remove this behavior.Function `checkTypeEq` changes its behavior depending on the presence of `fdefertypeerrors` in an obscure case around heterogeneous equalities; see the code in `go_co`. This is undocumented (in the code), and neither Simon nor I can figure out why it's done.
Task: figure this out, and either document or remove this behavior.Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/17131Kind inference bug in type family declaration20200513T09:45:32ZSimon Peyton JonesKind inference bug in type family declarationConsider this (cut down from #17113)
```
{# LANGUAGE MagicHash, UnboxedTuples, TypeInType, TypeFamilies, TypeOperators #}
module Test where
import GHC.Exts
type family TypeReps xs where
TypeReps '[] = '[]
TypeReps ((a::TYPE k) ': as) = k ': TypeReps as
type family Tuple# xs = (t :: TYPE ('TupleRep (TypeReps xs))) where
Tuple# '[a] = (# a #)
```
This compiles fine with GHC 8.6.4, but fails thus with HEAD:
```
T17113.hs:14:34: error:
• Expected kind ‘TYPE ('TupleRep (TypeReps xs))’,
but ‘(# a #)’ has kind ‘TYPE ('TupleRep '[ 'LiftedRep])’
• In the type ‘(# a #)’
In the type family declaration for ‘Tuple#’

14  Tuple# '[a] = (# a #)
 ^^^^^^^
```
Notice that free `xs` in the error message which is completely bogus. Something is badly wrong.Consider this (cut down from #17113)
```
{# LANGUAGE MagicHash, UnboxedTuples, TypeInType, TypeFamilies, TypeOperators #}
module Test where
import GHC.Exts
type family TypeReps xs where
TypeReps '[] = '[]
TypeReps ((a::TYPE k) ': as) = k ': TypeReps as
type family Tuple# xs = (t :: TYPE ('TupleRep (TypeReps xs))) where
Tuple# '[a] = (# a #)
```
This compiles fine with GHC 8.6.4, but fails thus with HEAD:
```
T17113.hs:14:34: error:
• Expected kind ‘TYPE ('TupleRep (TypeReps xs))’,
but ‘(# a #)’ has kind ‘TYPE ('TupleRep '[ 'LiftedRep])’
• In the type ‘(# a #)’
In the type family declaration for ‘Tuple#’

14  Tuple# '[a] = (# a #)
 ^^^^^^^
```
Notice that free `xs` in the error message which is completely bogus. Something is badly wrong.