GHC issueshttps://gitlab.haskell.org/ghc/ghc//issues20200505T09:46:50Zhttps://gitlab.haskell.org/ghc/ghc//issues/16245GHC panic (No skolem info) with RankNTypes and strange scoping20200505T09:46:50ZRyan ScottGHC panic (No skolem info) with RankNTypes and strange scopingThe following program panics with GHC 8.6.3 and HEAD:
```hs
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE DataKinds #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE QuantifiedConstraints #}
module Bug where
import Data.Kind
type Const a b = a
type SameKind (a :: k) (b :: k) = (() :: Constraint)
class (forall (b :: k). SameKind a b) => C (k :: Const Type a)
```
```
$ /opt/ghc/8.6.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:11:36: error:ghc: panic! (the 'impossible' happened)
(GHC version 8.6.3 for x86_64unknownlinux):
No skolem info:
[k1_a1X4[sk:1]]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcErrors.hs:2891:5 in ghc:TcErrors
```
As with #16244, I imagine that the real culprit is that `SameKind a b` would force `a :: k`, which would be illscoped.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"GHC panic (No skolem info) with QuantifiedConstraints and strange scoping","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.3","keywords":["QuantifiedConstraints","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program panics with GHC 8.6.3 and HEAD:\r\n\r\n{{{#!hs\r\n{# LANGUAGE ConstraintKinds #}\r\n{# LANGUAGE DataKinds #}\r\n{# LANGUAGE PolyKinds #}\r\n{# LANGUAGE QuantifiedConstraints #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ntype Const a b = a\r\ntype SameKind (a :: k) (b :: k) = (() :: Constraint)\r\nclass (forall (b :: k). SameKind a b) => C (k :: Const Type a)\r\n}}}\r\n{{{\r\n$ /opt/ghc/8.6.3/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:11:36: error:ghc: panic! (the 'impossible' happened)\r\n (GHC version 8.6.3 for x86_64unknownlinux):\r\n No skolem info:\r\n [k1_a1X4[sk:1]]\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable\r\n pprPanic, called at compiler/typecheck/TcErrors.hs:2891:5 in ghc:TcErrors\r\n}}}\r\n\r\nAs with #16244, I imagine that the real culprit is that `SameKind a b` would force `a :: k`, which would be illscoped.","type_of_failure":"OtherFailure","blocking":[]} >The following program panics with GHC 8.6.3 and HEAD:
```hs
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE DataKinds #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE QuantifiedConstraints #}
module Bug where
import Data.Kind
type Const a b = a
type SameKind (a :: k) (b :: k) = (() :: Constraint)
class (forall (b :: k). SameKind a b) => C (k :: Const Type a)
```
```
$ /opt/ghc/8.6.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:11:36: error:ghc: panic! (the 'impossible' happened)
(GHC version 8.6.3 for x86_64unknownlinux):
No skolem info:
[k1_a1X4[sk:1]]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcErrors.hs:2891:5 in ghc:TcErrors
```
As with #16244, I imagine that the real culprit is that `SameKind a b` would force `a :: k`, which would be illscoped.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"GHC panic (No skolem info) with QuantifiedConstraints and strange scoping","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.3","keywords":["QuantifiedConstraints","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program panics with GHC 8.6.3 and HEAD:\r\n\r\n{{{#!hs\r\n{# LANGUAGE ConstraintKinds #}\r\n{# LANGUAGE DataKinds #}\r\n{# LANGUAGE PolyKinds #}\r\n{# LANGUAGE QuantifiedConstraints #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ntype Const a b = a\r\ntype SameKind (a :: k) (b :: k) = (() :: Constraint)\r\nclass (forall (b :: k). SameKind a b) => C (k :: Const Type a)\r\n}}}\r\n{{{\r\n$ /opt/ghc/8.6.3/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:11:36: error:ghc: panic! (the 'impossible' happened)\r\n (GHC version 8.6.3 for x86_64unknownlinux):\r\n No skolem info:\r\n [k1_a1X4[sk:1]]\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable\r\n pprPanic, called at compiler/typecheck/TcErrors.hs:2891:5 in ghc:TcErrors\r\n}}}\r\n\r\nAs with #16244, I imagine that the real culprit is that `SameKind a b` would force `a :: k`, which would be illscoped.","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/15942Associated type family can't be used at the kind level within other parts of ...20200110T19:59:15ZIcelandjackAssociated type family can't be used at the kind level within other parts of parent classI want to run the following past you (using [Visible Kind Applications](https://phabricator.haskell.org/D5229) but may be unrelated). The following compiles
```hs
{# Language DataKinds #}
{# Language KindSignatures #}
{# Language TypeFamilies #}
{# Language AllowAmbiguousTypes #}
import Data.Kind
type G = Bool > Type
data Fun :: G
class F (bool :: Bool) where
type Not bool :: Bool
foo :: Fun (Not bool)
```
but quantifying `Bool` invisibly all of a sudden I can't use `Not`
```hs
{# Language DataKinds #}
{# Language RankNTypes #}
{# Language TypeApplications #}
{# Language PolyKinds #}
{# Language KindSignatures #}
{# Language TypeFamilies #}
{# Language AllowAmbiguousTypes #}
import Data.Kind
type G = forall (b :: Bool). Type
data Fun :: G
class F (bool :: Bool) where
type Not bool :: Bool
foo :: Fun @(Not bool)
```
```
$ ghcstage2 interactive ignoredotghci 739_bug.hs
GHCi, version 8.7.20181017: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( 739_bug.hs, interpreted )
739_bug.hs:17:16: error:
• Type constructor ‘Not’ cannot be used here
(it is defined and used in the same recursive group)
• In the first argument of ‘Fun’, namely ‘(Not bool)’
In the type signature: foo :: Fun @(Not bool)
In the class declaration for ‘F’

17  foo :: Fun @(Not bool)
 ^^^
Failed, no modules loaded.
```
Is this restriction warrantedI want to run the following past you (using [Visible Kind Applications](https://phabricator.haskell.org/D5229) but may be unrelated). The following compiles
```hs
{# Language DataKinds #}
{# Language KindSignatures #}
{# Language TypeFamilies #}
{# Language AllowAmbiguousTypes #}
import Data.Kind
type G = Bool > Type
data Fun :: G
class F (bool :: Bool) where
type Not bool :: Bool
foo :: Fun (Not bool)
```
but quantifying `Bool` invisibly all of a sudden I can't use `Not`
```hs
{# Language DataKinds #}
{# Language RankNTypes #}
{# Language TypeApplications #}
{# Language PolyKinds #}
{# Language KindSignatures #}
{# Language TypeFamilies #}
{# Language AllowAmbiguousTypes #}
import Data.Kind
type G = forall (b :: Bool). Type
data Fun :: G
class F (bool :: Bool) where
type Not bool :: Bool
foo :: Fun @(Not bool)
```
```
$ ghcstage2 interactive ignoredotghci 739_bug.hs
GHCi, version 8.7.20181017: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( 739_bug.hs, interpreted )
739_bug.hs:17:16: error:
• Type constructor ‘Not’ cannot be used here
(it is defined and used in the same recursive group)
• In the first argument of ‘Fun’, namely ‘(Not bool)’
In the type signature: foo :: Fun @(Not bool)
In the class declaration for ‘F’

17  foo :: Fun @(Not bool)
 ^^^
Failed, no modules loaded.
```
Is this restriction warranted8.6.3https://gitlab.haskell.org/ghc/ghc//issues/15710Should GHC accept a type signature that needs coercion quantification?20200415T15:28:19ZSimon Peyton JonesShould GHC accept a type signature that needs coercion quantification?Consider
```
f :: forall k (f :: k) (x :: k1). (k ~ (k1 > *)) => f x
f = error "uk"
```
Should we accept it? Now that we have coercion quantification (Trac #15497), I think the answer should be yes, with the elaborated signature being
```
f :: forall k (f::k) (x::k1). forall (co :: k ~# (k1>*)). (f > co) x
```
But there is a problem: the user wrote `k ~ (k1 > *)`, and that's a boxed value that we can't take apart in types. I'm not sure what to do here.
These thoughts arose when contemplating `Note [Emitting the residual implication in simplifyInfer]` in `TcSimplify`; see [ticket:15710\#comment:161240](https://gitlab.haskell.org//ghc/ghc/issues/15710#note_161240) in #15497Consider
```
f :: forall k (f :: k) (x :: k1). (k ~ (k1 > *)) => f x
f = error "uk"
```
Should we accept it? Now that we have coercion quantification (Trac #15497), I think the answer should be yes, with the elaborated signature being
```
f :: forall k (f::k) (x::k1). forall (co :: k ~# (k1>*)). (f > co) x
```
But there is a problem: the user wrote `k ~ (k1 > *)`, and that's a boxed value that we can't take apart in types. I'm not sure what to do here.
These thoughts arose when contemplating `Note [Emitting the residual implication in simplifyInfer]` in `TcSimplify`; see [ticket:15710\#comment:161240](https://gitlab.haskell.org//ghc/ghc/issues/15710#note_161240) in #15497https://gitlab.haskell.org/ghc/ghc//issues/15589Always promoting metavariables during type inference may be wrong20190707T18:04:00ZRichard Eisenbergrae@richarde.devAlways promoting metavariables during type inference may be wrongCurrently, when checking a type signature, GHC promotes all the metavariables that arise during checking as soon as it's done checking the signature. This may be incorrect sometimes.
Consider
```hs
{# LANGUAGE ScopedTypeVariables, TypeInType, TypeOperators, TypeFamilies,
AllowAmbiguousTypes #}
import Data.Proxy
import Data.Type.Equality
import Data.Type.Bool
import Data.Kind
data SameKind :: forall k. k > k > Type
type family IfK (e :: Proxy (j :: Bool)) (f :: m) (g :: n) :: If j m n where
IfK (_ :: Proxy True) f _ = f
IfK (_ :: Proxy False) _ g = g
y :: forall (cb :: Bool) (c :: Proxy cb). cb :~: True > ()
y Refl = let x :: forall a b (d :: a). SameKind (IfK c b d) d
x = undefined
in ()
```
This panics currently (#15588), but I'm pretty sure it will erroneously be rejected even after the panic is fixed. Let's walk through it.
 We can derive `IfK :: forall (j :: Bool) (m :: Type) (n :: Type). Proxy j > m > n > If j m n`, where `If :: forall k. Bool > k > k > k` is imported from `Data.Type.Bool` and is a straightforward conditional choice operator.
 In the type of `x`, we see that we need the kind of `IfK c b d` to match the kind of `d`. That is, if `b :: kappa[3]`, we have `[W] If cb kappa[3] a ~ a`. Here, the `forall` in `x`'s type is at level 3; the RHS of `y` is at level 2.
 If we could reduce `If cb kappa[3] a` to `kappa[3]`, then we would solve `kappa[3] := a`, but we can't make this reduction, because `cb` is a skolem.
 Instead, we finish checking the type of `x` and promote `kappa[3]` to `kappa[2]`.
 Later, we'll make an implication constraint with `[G] cb ~ True`. When solving that implication constraint, we'll get `[W] If True kappa[2] a ~ a` and simplify to `[W] kappa[2] ~ a`, but that will be insoluble because we'll be solving at level 3, and now `kappa[2]` is at level 2. We're too late.
Yet, I claim that this program should be accepted, and it would be if GHC tracked a set of ambient givens and used them in local calls to the solver. With these "ambient givens" (instead of putting them only in implication constraints), we would know `cb ~ True` the first time we try to solve, and then we'll succeed.
An alternative story is to change how levels are used with variables. Currently, levels are, essentially, the number of type variables available from an outer scope. Accordingly, we must make sure that the level of a variable is never higher than the ambient level. (If it were, we wouldn't know what extra variable(s) were in scope.) Instead, we could just store the list of variables that were in scope. We wouldn't then need to promote in this case  promotion would happen only during floating. But tracking these lists is a real pain. (If we decide to pursue this further, I can add more details, but it's all in Chapter 6 in [my thesis](https://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1074&context=compsci_pubs)  section 6.5 to be specific.)
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Always promoting metavariables during type inference may be wrong","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Currently, when checking a type signature, GHC promotes all the metavariables that arise during checking as soon as it's done checking the signature. This may be incorrect sometimes.\r\n\r\nConsider\r\n\r\n{{{#!hs\r\n{# LANGUAGE ScopedTypeVariables, TypeInType, TypeOperators, TypeFamilies,\r\n AllowAmbiguousTypes #}\r\n\r\nimport Data.Proxy\r\nimport Data.Type.Equality\r\nimport Data.Type.Bool\r\nimport Data.Kind\r\n\r\ndata SameKind :: forall k. k > k > Type\r\ntype family IfK (e :: Proxy (j :: Bool)) (f :: m) (g :: n) :: If j m n where\r\n IfK (_ :: Proxy True) f _ = f\r\n IfK (_ :: Proxy False) _ g = g\r\n\r\ny :: forall (cb :: Bool) (c :: Proxy cb). cb :~: True > ()\r\ny Refl = let x :: forall a b (d :: a). SameKind (IfK c b d) d\r\n x = undefined\r\n in ()\r\n}}}\r\n\r\nThis panics currently (#15588), but I'm pretty sure it will erroneously be rejected even after the panic is fixed. Let's walk through it.\r\n\r\n* We can derive `IfK :: forall (j :: Bool) (m :: Type) (n :: Type). Proxy j > m > n > If j m n`, where `If :: forall k. Bool > k > k > k` is imported from `Data.Type.Bool` and is a straightforward conditional choice operator.\r\n\r\n* In the type of `x`, we see that we need the kind of `IfK c b d` to match the kind of `d`. That is, if `b :: kappa[3]`, we have `[W] If cb kappa[3] a ~ a`. Here, the `forall` in `x`'s type is at level 3; the RHS of `y` is at level 2.\r\n\r\n* If we could reduce `If cb kappa[3] a` to `kappa[3]`, then we would solve `kappa[3] := a`, but we can't make this reduction, because `cb` is a skolem.\r\n\r\n* Instead, we finish checking the type of `x` and promote `kappa[3]` to `kappa[2]`.\r\n\r\n* Later, we'll make an implication constraint with `[G] cb ~ True`. When solving that implication constraint, we'll get `[W] If True kappa[2] a ~ a` and simplify to `[W] kappa[2] ~ a`, but that will be insoluble because we'll be solving at level 3, and now `kappa[2]` is at level 2. We're too late.\r\n\r\nYet, I claim that this program should be accepted, and it would be if GHC tracked a set of ambient givens and used them in local calls to the solver. With these \"ambient givens\" (instead of putting them only in implication constraints), we would know `cb ~ True` the first time we try to solve, and then we'll succeed.\r\n\r\nAn alternative story is to change how levels are used with variables. Currently, levels are, essentially, the number of type variables available from an outer scope. Accordingly, we must make sure that the level of a variable is never higher than the ambient level. (If it were, we wouldn't know what extra variable(s) were in scope.) Instead, we could just store the list of variables that were in scope. We wouldn't then need to promote in this case  promotion would happen only during floating. But tracking these lists is a real pain. (If we decide to pursue this further, I can add more details, but it's all in Chapter 6 in [https://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1074&context=compsci_pubs my thesis]  section 6.5 to be specific.)","type_of_failure":"OtherFailure","blocking":[]} >Currently, when checking a type signature, GHC promotes all the metavariables that arise during checking as soon as it's done checking the signature. This may be incorrect sometimes.
Consider
```hs
{# LANGUAGE ScopedTypeVariables, TypeInType, TypeOperators, TypeFamilies,
AllowAmbiguousTypes #}
import Data.Proxy
import Data.Type.Equality
import Data.Type.Bool
import Data.Kind
data SameKind :: forall k. k > k > Type
type family IfK (e :: Proxy (j :: Bool)) (f :: m) (g :: n) :: If j m n where
IfK (_ :: Proxy True) f _ = f
IfK (_ :: Proxy False) _ g = g
y :: forall (cb :: Bool) (c :: Proxy cb). cb :~: True > ()
y Refl = let x :: forall a b (d :: a). SameKind (IfK c b d) d
x = undefined
in ()
```
This panics currently (#15588), but I'm pretty sure it will erroneously be rejected even after the panic is fixed. Let's walk through it.
 We can derive `IfK :: forall (j :: Bool) (m :: Type) (n :: Type). Proxy j > m > n > If j m n`, where `If :: forall k. Bool > k > k > k` is imported from `Data.Type.Bool` and is a straightforward conditional choice operator.
 In the type of `x`, we see that we need the kind of `IfK c b d` to match the kind of `d`. That is, if `b :: kappa[3]`, we have `[W] If cb kappa[3] a ~ a`. Here, the `forall` in `x`'s type is at level 3; the RHS of `y` is at level 2.
 If we could reduce `If cb kappa[3] a` to `kappa[3]`, then we would solve `kappa[3] := a`, but we can't make this reduction, because `cb` is a skolem.
 Instead, we finish checking the type of `x` and promote `kappa[3]` to `kappa[2]`.
 Later, we'll make an implication constraint with `[G] cb ~ True`. When solving that implication constraint, we'll get `[W] If True kappa[2] a ~ a` and simplify to `[W] kappa[2] ~ a`, but that will be insoluble because we'll be solving at level 3, and now `kappa[2]` is at level 2. We're too late.
Yet, I claim that this program should be accepted, and it would be if GHC tracked a set of ambient givens and used them in local calls to the solver. With these "ambient givens" (instead of putting them only in implication constraints), we would know `cb ~ True` the first time we try to solve, and then we'll succeed.
An alternative story is to change how levels are used with variables. Currently, levels are, essentially, the number of type variables available from an outer scope. Accordingly, we must make sure that the level of a variable is never higher than the ambient level. (If it were, we wouldn't know what extra variable(s) were in scope.) Instead, we could just store the list of variables that were in scope. We wouldn't then need to promote in this case  promotion would happen only during floating. But tracking these lists is a real pain. (If we decide to pursue this further, I can add more details, but it's all in Chapter 6 in [my thesis](https://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1074&context=compsci_pubs)  section 6.5 to be specific.)
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Always promoting metavariables during type inference may be wrong","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Currently, when checking a type signature, GHC promotes all the metavariables that arise during checking as soon as it's done checking the signature. This may be incorrect sometimes.\r\n\r\nConsider\r\n\r\n{{{#!hs\r\n{# LANGUAGE ScopedTypeVariables, TypeInType, TypeOperators, TypeFamilies,\r\n AllowAmbiguousTypes #}\r\n\r\nimport Data.Proxy\r\nimport Data.Type.Equality\r\nimport Data.Type.Bool\r\nimport Data.Kind\r\n\r\ndata SameKind :: forall k. k > k > Type\r\ntype family IfK (e :: Proxy (j :: Bool)) (f :: m) (g :: n) :: If j m n where\r\n IfK (_ :: Proxy True) f _ = f\r\n IfK (_ :: Proxy False) _ g = g\r\n\r\ny :: forall (cb :: Bool) (c :: Proxy cb). cb :~: True > ()\r\ny Refl = let x :: forall a b (d :: a). SameKind (IfK c b d) d\r\n x = undefined\r\n in ()\r\n}}}\r\n\r\nThis panics currently (#15588), but I'm pretty sure it will erroneously be rejected even after the panic is fixed. Let's walk through it.\r\n\r\n* We can derive `IfK :: forall (j :: Bool) (m :: Type) (n :: Type). Proxy j > m > n > If j m n`, where `If :: forall k. Bool > k > k > k` is imported from `Data.Type.Bool` and is a straightforward conditional choice operator.\r\n\r\n* In the type of `x`, we see that we need the kind of `IfK c b d` to match the kind of `d`. That is, if `b :: kappa[3]`, we have `[W] If cb kappa[3] a ~ a`. Here, the `forall` in `x`'s type is at level 3; the RHS of `y` is at level 2.\r\n\r\n* If we could reduce `If cb kappa[3] a` to `kappa[3]`, then we would solve `kappa[3] := a`, but we can't make this reduction, because `cb` is a skolem.\r\n\r\n* Instead, we finish checking the type of `x` and promote `kappa[3]` to `kappa[2]`.\r\n\r\n* Later, we'll make an implication constraint with `[G] cb ~ True`. When solving that implication constraint, we'll get `[W] If True kappa[2] a ~ a` and simplify to `[W] kappa[2] ~ a`, but that will be insoluble because we'll be solving at level 3, and now `kappa[2]` is at level 2. We're too late.\r\n\r\nYet, I claim that this program should be accepted, and it would be if GHC tracked a set of ambient givens and used them in local calls to the solver. With these \"ambient givens\" (instead of putting them only in implication constraints), we would know `cb ~ True` the first time we try to solve, and then we'll succeed.\r\n\r\nAn alternative story is to change how levels are used with variables. Currently, levels are, essentially, the number of type variables available from an outer scope. Accordingly, we must make sure that the level of a variable is never higher than the ambient level. (If it were, we wouldn't know what extra variable(s) were in scope.) Instead, we could just store the list of variables that were in scope. We wouldn't then need to promote in this case  promotion would happen only during floating. But tracking these lists is a real pain. (If we decide to pursue this further, I can add more details, but it's all in Chapter 6 in [https://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1074&context=compsci_pubs my thesis]  section 6.5 to be specific.)","type_of_failure":"OtherFailure","blocking":[]} >8.6.1https://gitlab.haskell.org/ghc/ghc//issues/15588Panic when abusing kind inference20190707T18:04:01ZRichard Eisenbergrae@richarde.devPanic when abusing kind inferenceWhen I say
```hs
{# LANGUAGE ScopedTypeVariables, TypeInType, TypeOperators, TypeFamilies,
AllowAmbiguousTypes #}
import Data.Proxy
import Data.Type.Equality
import Data.Type.Bool
import Data.Kind
data SameKind :: forall k. k > k > Type
type family IfK (e :: Proxy (j :: Bool)) (f :: m) (g :: n) :: If j m n where
IfK (_ :: Proxy True) f _ = f
IfK (_ :: Proxy False) _ g = g
y :: forall ck (c :: ck). ck :~: Proxy True > ()
y Refl = let x :: forall a b (d :: a). SameKind (IfK c b d) d
x = undefined
in ()
```
HEAD says
```
ghcstage2: panic! (the 'impossible' happened)
(GHC version 8.7.20180827 for x86_64appledarwin):
ASSERT failed!
Bad coercion hole co_a3iZ: If
j_a3j0[tau:2] m_a3j1[tau:2] a_a3gV[sk:3]
a_a3gV[sk:3]
nominal
If j_a3j0[tau:2] m_a3j1[tau:2] a_a3jj[sk:3] ~# a_a3jj[sk:3]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable
pprPanic, called at compiler/utils/Outputable.hs:1219:5 in ghc:Outputable
assertPprPanic, called at compiler/typecheck/TcMType.hs:316:25 in ghc:TcMType
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
```
It's as yet unclear whether the program should be accepted. My best guess is that it should, but that (even with this panic fixed) GHC isn't up to the task.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 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":"Panic when abusing kind inference","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"When I say\r\n\r\n{{{#!hs\r\n{# LANGUAGE ScopedTypeVariables, TypeInType, TypeOperators, TypeFamilies,\r\n AllowAmbiguousTypes #}\r\n\r\nimport Data.Proxy\r\nimport Data.Type.Equality\r\nimport Data.Type.Bool\r\nimport Data.Kind\r\n\r\ndata SameKind :: forall k. k > k > Type\r\ntype family IfK (e :: Proxy (j :: Bool)) (f :: m) (g :: n) :: If j m n where\r\n IfK (_ :: Proxy True) f _ = f\r\n IfK (_ :: Proxy False) _ g = g\r\n\r\ny :: forall ck (c :: ck). ck :~: Proxy True > ()\r\ny Refl = let x :: forall a b (d :: a). SameKind (IfK c b d) d\r\n x = undefined\r\n in ()\r\n}}}\r\n\r\nHEAD says\r\n\r\n{{{\r\nghcstage2: panic! (the 'impossible' happened)\r\n (GHC version 8.7.20180827 for x86_64appledarwin):\r\n\tASSERT failed!\r\n Bad coercion hole co_a3iZ: If\r\n j_a3j0[tau:2] m_a3j1[tau:2] a_a3gV[sk:3]\r\n a_a3gV[sk:3]\r\n nominal\r\n If j_a3j0[tau:2] m_a3j1[tau:2] a_a3jj[sk:3] ~# a_a3jj[sk:3]\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable\r\n pprPanic, called at compiler/utils/Outputable.hs:1219:5 in ghc:Outputable\r\n assertPprPanic, called at compiler/typecheck/TcMType.hs:316:25 in ghc:TcMType\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n}}}\r\n\r\nIt's as yet unclear whether the program should be accepted. My best guess is that it should, but that (even with this panic fixed) GHC isn't up to the task.","type_of_failure":"OtherFailure","blocking":[]} >When I say
```hs
{# LANGUAGE ScopedTypeVariables, TypeInType, TypeOperators, TypeFamilies,
AllowAmbiguousTypes #}
import Data.Proxy
import Data.Type.Equality
import Data.Type.Bool
import Data.Kind
data SameKind :: forall k. k > k > Type
type family IfK (e :: Proxy (j :: Bool)) (f :: m) (g :: n) :: If j m n where
IfK (_ :: Proxy True) f _ = f
IfK (_ :: Proxy False) _ g = g
y :: forall ck (c :: ck). ck :~: Proxy True > ()
y Refl = let x :: forall a b (d :: a). SameKind (IfK c b d) d
x = undefined
in ()
```
HEAD says
```
ghcstage2: panic! (the 'impossible' happened)
(GHC version 8.7.20180827 for x86_64appledarwin):
ASSERT failed!
Bad coercion hole co_a3iZ: If
j_a3j0[tau:2] m_a3j1[tau:2] a_a3gV[sk:3]
a_a3gV[sk:3]
nominal
If j_a3j0[tau:2] m_a3j1[tau:2] a_a3jj[sk:3] ~# a_a3jj[sk:3]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable
pprPanic, called at compiler/utils/Outputable.hs:1219:5 in ghc:Outputable
assertPprPanic, called at compiler/typecheck/TcMType.hs:316:25 in ghc:TcMType
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
```
It's as yet unclear whether the program should be accepted. My best guess is that it should, but that (even with this panic fixed) GHC isn't up to the task.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 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":"Panic when abusing kind inference","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"When I say\r\n\r\n{{{#!hs\r\n{# LANGUAGE ScopedTypeVariables, TypeInType, TypeOperators, TypeFamilies,\r\n AllowAmbiguousTypes #}\r\n\r\nimport Data.Proxy\r\nimport Data.Type.Equality\r\nimport Data.Type.Bool\r\nimport Data.Kind\r\n\r\ndata SameKind :: forall k. k > k > Type\r\ntype family IfK (e :: Proxy (j :: Bool)) (f :: m) (g :: n) :: If j m n where\r\n IfK (_ :: Proxy True) f _ = f\r\n IfK (_ :: Proxy False) _ g = g\r\n\r\ny :: forall ck (c :: ck). ck :~: Proxy True > ()\r\ny Refl = let x :: forall a b (d :: a). SameKind (IfK c b d) d\r\n x = undefined\r\n in ()\r\n}}}\r\n\r\nHEAD says\r\n\r\n{{{\r\nghcstage2: panic! (the 'impossible' happened)\r\n (GHC version 8.7.20180827 for x86_64appledarwin):\r\n\tASSERT failed!\r\n Bad coercion hole co_a3iZ: If\r\n j_a3j0[tau:2] m_a3j1[tau:2] a_a3gV[sk:3]\r\n a_a3gV[sk:3]\r\n nominal\r\n If j_a3j0[tau:2] m_a3j1[tau:2] a_a3jj[sk:3] ~# a_a3jj[sk:3]\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable\r\n pprPanic, called at compiler/utils/Outputable.hs:1219:5 in ghc:Outputable\r\n assertPprPanic, called at compiler/typecheck/TcMType.hs:316:25 in ghc:TcMType\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n}}}\r\n\r\nIt's as yet unclear whether the program should be accepted. My best guess is that it should, but that (even with this panic fixed) GHC isn't up to the task.","type_of_failure":"OtherFailure","blocking":[]} >8.6.1https://gitlab.haskell.org/ghc/ghc//issues/15561TypeInType: Type error conditioned on ordering of GADT and type family defini...20190707T18:04:07ZBj0rnTypeInType: Type error conditioned on ordering of GADT and type family definitionsConsider this code which successfully compiles:
```hs
{# LANGUAGE TypeInType, TypeFamilies, GADTs #}
module Bug where
class HasIndex a where
type Index a
emptyIndex :: IndexWrapper a
instance HasIndex [a] where
type Index [a] = Int
emptyIndex = Wrap 0
data IndexWrapper a where
Wrap :: Index a > IndexWrapper a
type family UnwrapAnyWrapperLikeThing (a :: t) :: k
type instance UnwrapAnyWrapperLikeThing ('Wrap a :: IndexWrapper [b]) = a
```
The mere act of moving the definition of `IndexWrapper` anywhere below the definition of `UnwrapAnyWrapperLikeThing` makes the type family instance at the bottom of the example fail compilation, with this error:
```
Bug.hs:17:15: error:
• Illegal type synonym family application in instance: Index [b]
• In the type instance declaration for ‘UnwrapAnyWrapperLikeThing’

17  type instance UnwrapAnyWrapperLikeThing ('Wrap a :: IndexWrapper [b]) = a
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
This is the smallest example that I could come up with; my real scenario of course has more things going on, but I can share if it would help.
The problem for me (other than that I'm pretty sure reordering definitions in Haskell should never affect anything) is that I would like just the definition of the type family (`UnwrapAnyWrapperLikeThing` in this example) in module `A` and all of the other definitions in module `B` that imports `A`.
Ideally, I would have liked to add a `HasIndex a` constraint to the `Wrap` constructor, but that disqualifies use of `'Wrap` on the type level. This does make me feel like I'm on shaky ground to begin with.
I have reproduced this bug on 8.2.2, 8.4.3 and 8.6.0.20180810 (NixOS). I should note that 8.0.2 rejects even the code that I pasted here.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"TypeInType: Type error conditioned on ordering of GADT and type family definitions","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["GADTs","TypeFamilies,","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider this code which successfully compiles:\r\n{{{#!hs\r\n{# LANGUAGE TypeInType, TypeFamilies, GADTs #}\r\n\r\nmodule Bug where\r\n\r\nclass HasIndex a where\r\n type Index a\r\n emptyIndex :: IndexWrapper a\r\ninstance HasIndex [a] where\r\n type Index [a] = Int\r\n emptyIndex = Wrap 0\r\n\r\ndata IndexWrapper a where\r\n Wrap :: Index a > IndexWrapper a\r\n\r\ntype family UnwrapAnyWrapperLikeThing (a :: t) :: k\r\n\r\ntype instance UnwrapAnyWrapperLikeThing ('Wrap a :: IndexWrapper [b]) = a\r\n}}}\r\n\r\nThe mere act of moving the definition of `IndexWrapper` anywhere below the definition of `UnwrapAnyWrapperLikeThing` makes the type family instance at the bottom of the example fail compilation, with this error:\r\n{{{\r\nBug.hs:17:15: error:\r\n • Illegal type synonym family application in instance: Index [b]\r\n • In the type instance declaration for ‘UnwrapAnyWrapperLikeThing’\r\n \r\n17  type instance UnwrapAnyWrapperLikeThing ('Wrap a :: IndexWrapper [b]) = a\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nThis is the smallest example that I could come up with; my real scenario of course has more things going on, but I can share if it would help.\r\n\r\nThe problem for me (other than that I'm pretty sure reordering definitions in Haskell should never affect anything) is that I would like just the definition of the type family (`UnwrapAnyWrapperLikeThing` in this example) in module `A` and all of the other definitions in module `B` that imports `A`.\r\n\r\nIdeally, I would have liked to add a `HasIndex a` constraint to the `Wrap` constructor, but that disqualifies use of `'Wrap` on the type level. This does make me feel like I'm on shaky ground to begin with.\r\n\r\nI have reproduced this bug on 8.2.2, 8.4.3 and 8.6.0.20180810 (NixOS). I should note that 8.0.2 rejects even the code that I pasted here.","type_of_failure":"OtherFailure","blocking":[]} >Consider this code which successfully compiles:
```hs
{# LANGUAGE TypeInType, TypeFamilies, GADTs #}
module Bug where
class HasIndex a where
type Index a
emptyIndex :: IndexWrapper a
instance HasIndex [a] where
type Index [a] = Int
emptyIndex = Wrap 0
data IndexWrapper a where
Wrap :: Index a > IndexWrapper a
type family UnwrapAnyWrapperLikeThing (a :: t) :: k
type instance UnwrapAnyWrapperLikeThing ('Wrap a :: IndexWrapper [b]) = a
```
The mere act of moving the definition of `IndexWrapper` anywhere below the definition of `UnwrapAnyWrapperLikeThing` makes the type family instance at the bottom of the example fail compilation, with this error:
```
Bug.hs:17:15: error:
• Illegal type synonym family application in instance: Index [b]
• In the type instance declaration for ‘UnwrapAnyWrapperLikeThing’

17  type instance UnwrapAnyWrapperLikeThing ('Wrap a :: IndexWrapper [b]) = a
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
This is the smallest example that I could come up with; my real scenario of course has more things going on, but I can share if it would help.
The problem for me (other than that I'm pretty sure reordering definitions in Haskell should never affect anything) is that I would like just the definition of the type family (`UnwrapAnyWrapperLikeThing` in this example) in module `A` and all of the other definitions in module `B` that imports `A`.
Ideally, I would have liked to add a `HasIndex a` constraint to the `Wrap` constructor, but that disqualifies use of `'Wrap` on the type level. This does make me feel like I'm on shaky ground to begin with.
I have reproduced this bug on 8.2.2, 8.4.3 and 8.6.0.20180810 (NixOS). I should note that 8.0.2 rejects even the code that I pasted here.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"TypeInType: Type error conditioned on ordering of GADT and type family definitions","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["GADTs","TypeFamilies,","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider this code which successfully compiles:\r\n{{{#!hs\r\n{# LANGUAGE TypeInType, TypeFamilies, GADTs #}\r\n\r\nmodule Bug where\r\n\r\nclass HasIndex a where\r\n type Index a\r\n emptyIndex :: IndexWrapper a\r\ninstance HasIndex [a] where\r\n type Index [a] = Int\r\n emptyIndex = Wrap 0\r\n\r\ndata IndexWrapper a where\r\n Wrap :: Index a > IndexWrapper a\r\n\r\ntype family UnwrapAnyWrapperLikeThing (a :: t) :: k\r\n\r\ntype instance UnwrapAnyWrapperLikeThing ('Wrap a :: IndexWrapper [b]) = a\r\n}}}\r\n\r\nThe mere act of moving the definition of `IndexWrapper` anywhere below the definition of `UnwrapAnyWrapperLikeThing` makes the type family instance at the bottom of the example fail compilation, with this error:\r\n{{{\r\nBug.hs:17:15: error:\r\n • Illegal type synonym family application in instance: Index [b]\r\n • In the type instance declaration for ‘UnwrapAnyWrapperLikeThing’\r\n \r\n17  type instance UnwrapAnyWrapperLikeThing ('Wrap a :: IndexWrapper [b]) = a\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nThis is the smallest example that I could come up with; my real scenario of course has more things going on, but I can share if it would help.\r\n\r\nThe problem for me (other than that I'm pretty sure reordering definitions in Haskell should never affect anything) is that I would like just the definition of the type family (`UnwrapAnyWrapperLikeThing` in this example) in module `A` and all of the other definitions in module `B` that imports `A`.\r\n\r\nIdeally, I would have liked to add a `HasIndex a` constraint to the `Wrap` constructor, but that disqualifies use of `'Wrap` on the type level. This does make me feel like I'm on shaky ground to begin with.\r\n\r\nI have reproduced this bug on 8.2.2, 8.4.3 and 8.6.0.20180810 (NixOS). I should note that 8.0.2 rejects even the code that I pasted here.","type_of_failure":"OtherFailure","blocking":[]} >8.6.1https://gitlab.haskell.org/ghc/ghc//issues/15474Error message mentions Any20200123T19:16:21ZKrzysztof GogolewskiError message mentions AnyI'm not sure if this is a bug. File:
```hs
{# LANGUAGE RankNTypes #}
{# LANGUAGE TypeInType #}
module T15474 where
import Data.Kind (Type)
data Proxy a
type Forall = forall t. Proxy t
f1 :: forall (t :: Type). Proxy t
f1 = f1
f2 :: Forall
f2 = f1
```
gives an error message mentioning Any:
```
• Couldn't match type ‘GHC.Types.Any’ with ‘*’
Expected type: Proxy t
Actual type: Proxy t0
```
The appearance of Any is suspicious to me  I thought it's an implementation detail?I'm not sure if this is a bug. File:
```hs
{# LANGUAGE RankNTypes #}
{# LANGUAGE TypeInType #}
module T15474 where
import Data.Kind (Type)
data Proxy a
type Forall = forall t. Proxy t
f1 :: forall (t :: Type). Proxy t
f1 = f1
f2 :: Forall
f2 = f1
```
gives an error message mentioning Any:
```
• Couldn't match type ‘GHC.Types.Any’ with ‘*’
Expected type: Proxy t
Actual type: Proxy t0
```
The appearance of Any is suspicious to me  I thought it's an implementation detail?8.12.1https://gitlab.haskell.org/ghc/ghc//issues/14668Ordering of declarations can cause typechecking to fail20190707T18:16:05ZheptahedronOrdering of declarations can cause typechecking to failThe following will successfully typecheck:
```hs
{# LANGUAGE DataKinds #}
{# LANGUAGE KindSignatures #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeFamilies #}
data CInst
data G (b :: ()) = G
class C a where
type family F a
class (C a) => C' a where
type family F' a (b :: F a)
 data CInst
instance C CInst where
type F CInst = ()
instance C' CInst where
type F' CInst (b :: F CInst) = G b
```
But if the `data CInst` declaration is moved to where it is currently commented out, typechecking fails with this error:
```
Test.hs:23:18: error:
• Expected kind ‘F CInst’, but ‘b’ has kind ‘()’
• In the second argument of ‘F'’, namely ‘(b :: F CInst)’
In the type instance declaration for ‘F'’
In the instance declaration for ‘C' CInst’

23  type F' CInst (b :: F CInst) = G b

```
However, the data declaration //can// be in the lower position if the kind annotation for its argument is instead written as `data G (b :: F CInst) = G`.
This behavior is also exhibited when G is a type family (I believe the sort of type family does not matter, but I know for sure closed and open type families).
I was using GHC 8.2.2 when I discovered this, but user `erisco` on `#haskell` confirmed for 8.2.1 as well.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Ordering of declarations can cause typechecking to fail","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following will successfully typecheck:\r\n\r\n{{{#!hs\r\n{# LANGUAGE DataKinds #}\r\n{# LANGUAGE KindSignatures #}\r\n{# LANGUAGE TypeInType #}\r\n{# LANGUAGE TypeFamilies #}\r\n\r\ndata CInst\r\n\r\ndata G (b :: ()) = G \r\n\r\nclass C a where\r\n type family F a\r\n \r\nclass (C a) => C' a where\r\n type family F' a (b :: F a)\r\n\r\n data CInst\r\n\r\ninstance C CInst where\r\n type F CInst = ()\r\n\r\ninstance C' CInst where\r\ntype F' CInst (b :: F CInst) = G b\r\n}}}\r\n\r\nBut if the `data CInst` declaration is moved to where it is currently commented out, typechecking fails with this error: \r\n\r\n{{{\r\nTest.hs:23:18: error:\r\n • Expected kind ‘F CInst’, but ‘b’ has kind ‘()’\r\n • In the second argument of ‘F'’, namely ‘(b :: F CInst)’\r\n In the type instance declaration for ‘F'’\r\n In the instance declaration for ‘C' CInst’\r\n \r\n23  type F' CInst (b :: F CInst) = G b\r\n  \r\n}}}\r\n\r\nHowever, the data declaration //can// be in the lower position if the kind annotation for its argument is instead written as `data G (b :: F CInst) = G`.\r\n\r\nThis behavior is also exhibited when G is a type family (I believe the sort of type family does not matter, but I know for sure closed and open type families).\r\n\r\nI was using GHC 8.2.2 when I discovered this, but user `erisco` on `#haskell` confirmed for 8.2.1 as well.","type_of_failure":"OtherFailure","blocking":[]} >The following will successfully typecheck:
```hs
{# LANGUAGE DataKinds #}
{# LANGUAGE KindSignatures #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeFamilies #}
data CInst
data G (b :: ()) = G
class C a where
type family F a
class (C a) => C' a where
type family F' a (b :: F a)
 data CInst
instance C CInst where
type F CInst = ()
instance C' CInst where
type F' CInst (b :: F CInst) = G b
```
But if the `data CInst` declaration is moved to where it is currently commented out, typechecking fails with this error:
```
Test.hs:23:18: error:
• Expected kind ‘F CInst’, but ‘b’ has kind ‘()’
• In the second argument of ‘F'’, namely ‘(b :: F CInst)’
In the type instance declaration for ‘F'’
In the instance declaration for ‘C' CInst’

23  type F' CInst (b :: F CInst) = G b

```
However, the data declaration //can// be in the lower position if the kind annotation for its argument is instead written as `data G (b :: F CInst) = G`.
This behavior is also exhibited when G is a type family (I believe the sort of type family does not matter, but I know for sure closed and open type families).
I was using GHC 8.2.2 when I discovered this, but user `erisco` on `#haskell` confirmed for 8.2.1 as well.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Ordering of declarations can cause typechecking to fail","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following will successfully typecheck:\r\n\r\n{{{#!hs\r\n{# LANGUAGE DataKinds #}\r\n{# LANGUAGE KindSignatures #}\r\n{# LANGUAGE TypeInType #}\r\n{# LANGUAGE TypeFamilies #}\r\n\r\ndata CInst\r\n\r\ndata G (b :: ()) = G \r\n\r\nclass C a where\r\n type family F a\r\n \r\nclass (C a) => C' a where\r\n type family F' a (b :: F a)\r\n\r\n data CInst\r\n\r\ninstance C CInst where\r\n type F CInst = ()\r\n\r\ninstance C' CInst where\r\ntype F' CInst (b :: F CInst) = G b\r\n}}}\r\n\r\nBut if the `data CInst` declaration is moved to where it is currently commented out, typechecking fails with this error: \r\n\r\n{{{\r\nTest.hs:23:18: error:\r\n • Expected kind ‘F CInst’, but ‘b’ has kind ‘()’\r\n • In the second argument of ‘F'’, namely ‘(b :: F CInst)’\r\n In the type instance declaration for ‘F'’\r\n In the instance declaration for ‘C' CInst’\r\n \r\n23  type F' CInst (b :: F CInst) = G b\r\n  \r\n}}}\r\n\r\nHowever, the data declaration //can// be in the lower position if the kind annotation for its argument is instead written as `data G (b :: F CInst) = G`.\r\n\r\nThis behavior is also exhibited when G is a type family (I believe the sort of type family does not matter, but I know for sure closed and open type families).\r\n\r\nI was using GHC 8.2.2 when I discovered this, but user `erisco` on `#haskell` confirmed for 8.2.1 as well.","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/14645Allow type family in data family return kind20190707T18:16:10ZRichard Eisenbergrae@richarde.devAllow type family in data family return kindGHC currently allows
```hs
data family DF1 :: k1 > k2
```
where it's expected (and checked) that all data *instances* have a return kind of `Type`. (Perhaps `k2` expands to `Type > Type`, for example.)
However, it rejects
```hs
type family TF (x :: Type) :: Type
data family DF2 :: x > TF x
```
when that's clearly just as sensible as the first definition.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.1alpha1 
 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":"Allow type family in data family return kind","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.1alpha1","keywords":["TypeFamilies","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"GHC currently allows\r\n\r\n{{{#!hs\r\ndata family DF1 :: k1 > k2\r\n}}}\r\n\r\nwhere it's expected (and checked) that all data ''instances'' have a return kind of `Type`. (Perhaps `k2` expands to `Type > Type`, for example.)\r\n\r\nHowever, it rejects\r\n\r\n{{{#!hs\r\ntype family TF (x :: Type) :: Type\r\ndata family DF2 :: x > TF x\r\n}}}\r\n\r\nwhen that's clearly just as sensible as the first definition.","type_of_failure":"OtherFailure","blocking":[]} >GHC currently allows
```hs
data family DF1 :: k1 > k2
```
where it's expected (and checked) that all data *instances* have a return kind of `Type`. (Perhaps `k2` expands to `Type > Type`, for example.)
However, it rejects
```hs
type family TF (x :: Type) :: Type
data family DF2 :: x > TF x
```
when that's clearly just as sensible as the first definition.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.1alpha1 
 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":"Allow type family in data family return kind","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.1alpha1","keywords":["TypeFamilies","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"GHC currently allows\r\n\r\n{{{#!hs\r\ndata family DF1 :: k1 > k2\r\n}}}\r\n\r\nwhere it's expected (and checked) that all data ''instances'' have a return kind of `Type`. (Perhaps `k2` expands to `Type > Type`, for example.)\r\n\r\nHowever, it rejects\r\n\r\n{{{#!hs\r\ntype family TF (x :: Type) :: Type\r\ndata family DF2 :: x > TF x\r\n}}}\r\n\r\nwhen that's clearly just as sensible as the first definition.","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/14420Data families should not instantiate to nonType kinds20190710T12:48:27ZRichard Eisenbergrae@richarde.devData families should not instantiate to nonType kinds```hs
data family Any :: k  allowable now due to fix for #12369
type family F (a :: Bool) :: Nat where
F True = 0
F False = 1
F Any = 2
```
```
ghci> :kind! F True
F True :: Nat
= 0
ghci> :kind! F False
F False :: Nat
= 1
ghci> :kind! F Any
F Any :: Nat
= 2
```
Oh dear.
We should require that any instantiation of a data family be to a kind that ends in `Type`.
Inspired by [ticket:9429\#comment:144757](https://gitlab.haskell.org//ghc/ghc/issues/9429#note_144757)
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Data families should not instantiate to nonType kinds","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\ndata family Any :: k  allowable now due to fix for #12369\r\n\r\ntype family F (a :: Bool) :: Nat where\r\n F True = 0\r\n F False = 1\r\n F Any = 2\r\n}}}\r\n\r\n{{{\r\nghci> :kind! F True\r\nF True :: Nat\r\n= 0\r\nghci> :kind! F False\r\nF False :: Nat\r\n= 1\r\nghci> :kind! F Any\r\nF Any :: Nat\r\n= 2\r\n}}}\r\n\r\nOh dear.\r\n\r\nWe should require that any instantiation of a data family be to a kind that ends in `Type`.\r\n\r\nInspired by comment:31:ticket:9429","type_of_failure":"OtherFailure","blocking":[]} >```hs
data family Any :: k  allowable now due to fix for #12369
type family F (a :: Bool) :: Nat where
F True = 0
F False = 1
F Any = 2
```
```
ghci> :kind! F True
F True :: Nat
= 0
ghci> :kind! F False
F False :: Nat
= 1
ghci> :kind! F Any
F Any :: Nat
= 2
```
Oh dear.
We should require that any instantiation of a data family be to a kind that ends in `Type`.
Inspired by [ticket:9429\#comment:144757](https://gitlab.haskell.org//ghc/ghc/issues/9429#note_144757)
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Data families should not instantiate to nonType kinds","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\ndata family Any :: k  allowable now due to fix for #12369\r\n\r\ntype family F (a :: Bool) :: Nat where\r\n F True = 0\r\n F False = 1\r\n F Any = 2\r\n}}}\r\n\r\n{{{\r\nghci> :kind! F True\r\nF True :: Nat\r\n= 0\r\nghci> :kind! F False\r\nF False :: Nat\r\n= 1\r\nghci> :kind! F Any\r\nF Any :: Nat\r\n= 2\r\n}}}\r\n\r\nOh dear.\r\n\r\nWe should require that any instantiation of a data family be to a kind that ends in `Type`.\r\n\r\nInspired by comment:31:ticket:9429","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/14319Stuck type families can lead to lousy error messages20200123T19:27:40ZDavid FeuerStuck type families can lead to lousy error messagesI first noticed this problem at the type level:
```hs
{# language TypeFamilies, TypeInType, ScopedTypeVariables #}
module ArityError where
import Data.Kind
import GHC.TypeLits
import Data.Proxy
type family F (s :: Symbol) :: Type
type family G (s :: Symbol) :: F s
type instance G "Hi" = Maybe
```
This produces the error message
```hs
ArityError.hs:10:24: error:
• Expecting one more argument to ‘Maybe’
Expected kind ‘F "Hi"’, but ‘Maybe’ has kind ‘* > *’
• In the type ‘Maybe’
In the type instance declaration for ‘G’

10  type instance G "Hi" = Maybe
 ^^^^^
```
This looks utterly bogus: `F "Hi"` is stuck, so we have no idea what arity it indicates.

I just realized we have a similar problem at the term level:
```hs
f :: forall (s :: Symbol). Proxy s > F s
f _ _ = undefined
```
produces
```hs
ArityError.hs:14:1: error:
• Couldn't match expected type ‘F s’ with actual type ‘p0 > a0’
The type variables ‘p0’, ‘a0’ are ambiguous
• The equation(s) for ‘f’ have two arguments,
but its type ‘Proxy s > F s’ has only one
• Relevant bindings include
f :: Proxy s > F s (bound at ArityError.hs:14:1)

14  f _ _ = undefined
 ^^^^^^^^^^^^^^^^^
```
The claim that `Proxy s > F s` has only one argument is bogus; we only know that it has *at least* one argument. The fix (I imagine) is to refrain from reporting arity errors when we don't know enough about the relevant arities.I first noticed this problem at the type level:
```hs
{# language TypeFamilies, TypeInType, ScopedTypeVariables #}
module ArityError where
import Data.Kind
import GHC.TypeLits
import Data.Proxy
type family F (s :: Symbol) :: Type
type family G (s :: Symbol) :: F s
type instance G "Hi" = Maybe
```
This produces the error message
```hs
ArityError.hs:10:24: error:
• Expecting one more argument to ‘Maybe’
Expected kind ‘F "Hi"’, but ‘Maybe’ has kind ‘* > *’
• In the type ‘Maybe’
In the type instance declaration for ‘G’

10  type instance G "Hi" = Maybe
 ^^^^^
```
This looks utterly bogus: `F "Hi"` is stuck, so we have no idea what arity it indicates.

I just realized we have a similar problem at the term level:
```hs
f :: forall (s :: Symbol). Proxy s > F s
f _ _ = undefined
```
produces
```hs
ArityError.hs:14:1: error:
• Couldn't match expected type ‘F s’ with actual type ‘p0 > a0’
The type variables ‘p0’, ‘a0’ are ambiguous
• The equation(s) for ‘f’ have two arguments,
but its type ‘Proxy s > F s’ has only one
• Relevant bindings include
f :: Proxy s > F s (bound at ArityError.hs:14:1)

14  f _ _ = undefined
 ^^^^^^^^^^^^^^^^^
```
The claim that `Proxy s > F s` has only one argument is bogus; we only know that it has *at least* one argument. The fix (I imagine) is to refrain from reporting arity errors when we don't know enough about the relevant arities.https://gitlab.haskell.org/ghc/ghc//issues/14198Inconsistent treatment of implicitly bound kind variables as freefloating20191211T15:53:21ZRyan ScottInconsistent treatment of implicitly bound kind variables as freefloating(Spun off from the discussion starting at https://phabricator.haskell.org/D3872#109927.)
This program is accepted:
```hs
{# LANGUAGE ExistentialQuantification #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE RankNTypes #}
import Data.Proxy
data Foo = MkFoo (forall a. Proxy a)
```
There's something interesting going on here, however. Because `PolyKinds` is enabled, the kind of `a` is generalized to `k`. But where does `k` get quantified? It turns out that it's implicitly quantified as an existential type variable to `MkFoo`:
```
λ> :i Foo
data Foo = forall k. MkFoo (forall (a :: k). Proxy a)
```
This was brought up some time ago in #7873, where the conclusion was to keep this behavior. But it's strange becuase the `k` is existential, so the definition is probably unusable.
But to make things stranger, it you write out the kind of `a` explicitly:
```hs
{# LANGUAGE ExistentialQuantification #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE RankNTypes #}
import Data.Proxy
data Foo2 = MkFoo2 (forall (a :: k). Proxy a)
```
Then GHC will reject it:
```
Bug.hs:7:1: error:
Kind variable ‘k’ is implicitly bound in data type
‘Foo2’, but does not appear as the kind of any
of its type variables. Perhaps you meant
to bind it (with TypeInType) explicitly somewhere?

7  data Foo2 = MkFoo2 (forall (a :: k). Proxy a)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
So GHC's treatment is inconsistent. What should GHC do? We could:
1. Have both be an error.
2. Have both be accepted, and implicitly quantify `k` as an existential type variable
3. Have both be accepted, and implicitly quantify `k` in the `forall` itself. That is:
```hs
MkFoo :: (forall {k} (a :: k). Proxy k a) > Foo
```
4. Something else. When you try a similar trick with type synonyms:
```hs
{# LANGUAGE ExistentialQuantification #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE RankNTypes #}
import Data.Proxy
type Foo3 = forall a. Proxy a
```
Instead of generalizing the kind of `a`, its kind will default to `Any`:
```
λ> :i Foo3
type Foo3 = forall (a :: GHC.Types.Any). Proxy a
```
Would that be an appropriate trick for data types as well?(Spun off from the discussion starting at https://phabricator.haskell.org/D3872#109927.)
This program is accepted:
```hs
{# LANGUAGE ExistentialQuantification #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE RankNTypes #}
import Data.Proxy
data Foo = MkFoo (forall a. Proxy a)
```
There's something interesting going on here, however. Because `PolyKinds` is enabled, the kind of `a` is generalized to `k`. But where does `k` get quantified? It turns out that it's implicitly quantified as an existential type variable to `MkFoo`:
```
λ> :i Foo
data Foo = forall k. MkFoo (forall (a :: k). Proxy a)
```
This was brought up some time ago in #7873, where the conclusion was to keep this behavior. But it's strange becuase the `k` is existential, so the definition is probably unusable.
But to make things stranger, it you write out the kind of `a` explicitly:
```hs
{# LANGUAGE ExistentialQuantification #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE RankNTypes #}
import Data.Proxy
data Foo2 = MkFoo2 (forall (a :: k). Proxy a)
```
Then GHC will reject it:
```
Bug.hs:7:1: error:
Kind variable ‘k’ is implicitly bound in data type
‘Foo2’, but does not appear as the kind of any
of its type variables. Perhaps you meant
to bind it (with TypeInType) explicitly somewhere?

7  data Foo2 = MkFoo2 (forall (a :: k). Proxy a)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
So GHC's treatment is inconsistent. What should GHC do? We could:
1. Have both be an error.
2. Have both be accepted, and implicitly quantify `k` as an existential type variable
3. Have both be accepted, and implicitly quantify `k` in the `forall` itself. That is:
```hs
MkFoo :: (forall {k} (a :: k). Proxy k a) > Foo
```
4. Something else. When you try a similar trick with type synonyms:
```hs
{# LANGUAGE ExistentialQuantification #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE RankNTypes #}
import Data.Proxy
type Foo3 = forall a. Proxy a
```
Instead of generalizing the kind of `a`, its kind will default to `Any`:
```
λ> :i Foo3
type Foo3 = forall (a :: GHC.Types.Any). Proxy a
```
Would that be an appropriate trick for data types as well?https://gitlab.haskell.org/ghc/ghc//issues/14180Permit levity polymorphism in kinds20200519T15:14:06ZDavid FeuerPermit levity polymorphism in kinds```hs
{# language TypeInType, TypeFamilies, MagicHash #}
import GHC.Exts
type family MatchInt (f :: Int) :: () where
MatchInt ('I# x) = '()
```
produces
```
<interactive>:2:59: error:
• Couldn't match a lifted type with an unlifted type
When matching kinds
k0 :: *
Int# :: TYPE 'IntRep
Expected kind ‘Int#’, but ‘x’ has kind ‘k0’
• In the first argument of ‘ 'I#’, namely ‘x’
In the first argument of ‘MatchInt’, namely ‘( 'I# x)’
In the type family declaration for ‘MatchInt’
```
If, however, I replace `x` in the pattern with `_`, the type checker is satisfied. If I give it a pattern signature,
```hs
MatchInt ('I# (x :: Int#)) = '()
```
I get a different (and equally unhelpful) error message,
```
• Expecting a lifted type, but ‘Int#’ is unlifted
• In the kind ‘Int#’
In the first argument of ‘ 'I#’, namely ‘(x :: Int#)’
In the first argument of ‘MatchInt’, namely ‘( 'I# (x :: Int#))’
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Strange/bad error message binding unboxed type variable","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.2.2","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.3","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{# language TypeInType, TypeFamilies, MagicHash #}\r\n\r\nimport GHC.Exts\r\n\r\ntype family MatchInt (f :: Int) :: () where\r\n MatchInt ('I# x) = '()\r\n}}}\r\n\r\nproduces\r\n\r\n{{{\r\n<interactive>:2:59: error:\r\n • Couldn't match a lifted type with an unlifted type\r\n When matching kinds\r\n k0 :: *\r\n Int# :: TYPE 'IntRep\r\n Expected kind ‘Int#’, but ‘x’ has kind ‘k0’\r\n • In the first argument of ‘ 'I#’, namely ‘x’\r\n In the first argument of ‘MatchInt’, namely ‘( 'I# x)’\r\n In the type family declaration for ‘MatchInt’\r\n}}}\r\n\r\nIf, however, I replace `x` in the pattern with `_`, the type checker is satisfied. If I give it a pattern signature,\r\n\r\n{{{#!hs\r\nMatchInt ('I# (x :: Int#)) = '()\r\n}}}\r\n\r\nI get a different (and equally unhelpful) error message,\r\n\r\n{{{\r\n • Expecting a lifted type, but ‘Int#’ is unlifted\r\n • In the kind ‘Int#’\r\n In the first argument of ‘ 'I#’, namely ‘(x :: Int#)’\r\n In the first argument of ‘MatchInt’, namely ‘( 'I# (x :: Int#))’\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >```hs
{# language TypeInType, TypeFamilies, MagicHash #}
import GHC.Exts
type family MatchInt (f :: Int) :: () where
MatchInt ('I# x) = '()
```
produces
```
<interactive>:2:59: error:
• Couldn't match a lifted type with an unlifted type
When matching kinds
k0 :: *
Int# :: TYPE 'IntRep
Expected kind ‘Int#’, but ‘x’ has kind ‘k0’
• In the first argument of ‘ 'I#’, namely ‘x’
In the first argument of ‘MatchInt’, namely ‘( 'I# x)’
In the type family declaration for ‘MatchInt’
```
If, however, I replace `x` in the pattern with `_`, the type checker is satisfied. If I give it a pattern signature,
```hs
MatchInt ('I# (x :: Int#)) = '()
```
I get a different (and equally unhelpful) error message,
```
• Expecting a lifted type, but ‘Int#’ is unlifted
• In the kind ‘Int#’
In the first argument of ‘ 'I#’, namely ‘(x :: Int#)’
In the first argument of ‘MatchInt’, namely ‘( 'I# (x :: Int#))’
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Strange/bad error message binding unboxed type variable","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.2.2","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.3","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{# language TypeInType, TypeFamilies, MagicHash #}\r\n\r\nimport GHC.Exts\r\n\r\ntype family MatchInt (f :: Int) :: () where\r\n MatchInt ('I# x) = '()\r\n}}}\r\n\r\nproduces\r\n\r\n{{{\r\n<interactive>:2:59: error:\r\n • Couldn't match a lifted type with an unlifted type\r\n When matching kinds\r\n k0 :: *\r\n Int# :: TYPE 'IntRep\r\n Expected kind ‘Int#’, but ‘x’ has kind ‘k0’\r\n • In the first argument of ‘ 'I#’, namely ‘x’\r\n In the first argument of ‘MatchInt’, namely ‘( 'I# x)’\r\n In the type family declaration for ‘MatchInt’\r\n}}}\r\n\r\nIf, however, I replace `x` in the pattern with `_`, the type checker is satisfied. If I give it a pattern signature,\r\n\r\n{{{#!hs\r\nMatchInt ('I# (x :: Int#)) = '()\r\n}}}\r\n\r\nI get a different (and equally unhelpful) error message,\r\n\r\n{{{\r\n • Expecting a lifted type, but ‘Int#’ is unlifted\r\n • In the kind ‘Int#’\r\n In the first argument of ‘ 'I#’, namely ‘(x :: Int#)’\r\n In the first argument of ‘MatchInt’, namely ‘( 'I# (x :: Int#))’\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >8.2.3https://gitlab.haskell.org/ghc/ghc//issues/14155GHC mentions unlifted types out of the blue (to me anyway)20200123T19:31:01ZIcelandjackGHC mentions unlifted types out of the blue (to me anyway)This one does me 'ead in, I accidentally type `Ran` instead of `Swap`
```hs
{# Language RankNTypes, DerivingStrategies, TypeApplications, ScopedTypeVariables, GADTs, GeneralizedNewtypeDeriving, InstanceSigs, PolyKinds #}
import Data.Coerce
newtype Ran g h a = Ran (forall b. (a > g b) > h b)
newtype Swap p f g a where
Swap :: p g f a > Swap p f g a
deriving newtype
Show
class IxPointed m where
ireturn :: a > m i i a
instance IxPointed f => IxPointed (Swap f) where
ireturn :: forall a i. a > Swap f i i a
ireturn a = Ran (ireturn a)
```
and get this error
```
$ ghci ignoredotghci /tmp/bug.hs
GHCi, version 8.3.20170605: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( /tmp/bug.hs, interpreted )
/tmp/bug.hs:17:15: error:
• Couldn't match expected type ‘Swap f i i a’
with actual type ‘Ran g0 h0 a0’
• In the expression: Ran (ireturn a)
In an equation for ‘ireturn’: ireturn a = Ran (ireturn a)
In the instance declaration for ‘IxPointed (Swap f)’
• Relevant bindings include
a :: a (bound at /tmp/bug.hs:17:11)
ireturn :: a > Swap f i i a (bound at /tmp/bug.hs:17:3)

17  ireturn a = Ran (ireturn a)
 ^^^^^^^^^^^^^^^
/tmp/bug.hs:17:20: error:
• Couldn't match a lifted type with an unlifted type
Expected type: (a0 > g0 b) > h0 b
Actual type: (>) (a0 > g0 b) (a0 > g0 b) a
• In the first argument of ‘Ran’, namely ‘(ireturn a)’
In the expression: Ran (ireturn a)
In an equation for ‘ireturn’: ireturn a = Ran (ireturn a)

17  ireturn a = Ran (ireturn a)
 ^^^^^^^^^
Failed, modules loaded: none.
```
Is GHC right to bring up unlifted types? I would guess this is due to the newly added levity polymorphism of `(>) :: TYPE rep > TYPE rep' > Type`
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.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 mentions unlifted types out of the blue (to me anyway)","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This one does me 'ead in, I accidentally type `Ran` instead of `Swap` \r\n\r\n{{{#!hs\r\n{# Language RankNTypes, DerivingStrategies, TypeApplications, ScopedTypeVariables, GADTs, GeneralizedNewtypeDeriving, InstanceSigs, PolyKinds #}\r\n\r\nimport Data.Coerce\r\n\r\nnewtype Ran g h a = Ran (forall b. (a > g b) > h b)\r\n\r\nnewtype Swap p f g a where\r\n Swap :: p g f a > Swap p f g a\r\n deriving newtype\r\n Show\r\n\r\nclass IxPointed m where\r\n ireturn :: a > m i i a\r\n\r\ninstance IxPointed f => IxPointed (Swap f) where\r\n ireturn :: forall a i. a > Swap f i i a\r\n ireturn a = Ran (ireturn a)\r\n}}}\r\n\r\nand get this error\r\n\r\n{{{\r\n$ ghci ignoredotghci /tmp/bug.hs\r\nGHCi, version 8.3.20170605: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( /tmp/bug.hs, interpreted )\r\n\r\n/tmp/bug.hs:17:15: error:\r\n • Couldn't match expected type ‘Swap f i i a’\r\n with actual type ‘Ran g0 h0 a0’\r\n • In the expression: Ran (ireturn a)\r\n In an equation for ‘ireturn’: ireturn a = Ran (ireturn a)\r\n In the instance declaration for ‘IxPointed (Swap f)’\r\n • Relevant bindings include\r\n a :: a (bound at /tmp/bug.hs:17:11)\r\n ireturn :: a > Swap f i i a (bound at /tmp/bug.hs:17:3)\r\n \r\n17  ireturn a = Ran (ireturn a)\r\n  ^^^^^^^^^^^^^^^\r\n\r\n/tmp/bug.hs:17:20: error:\r\n • Couldn't match a lifted type with an unlifted type\r\n Expected type: (a0 > g0 b) > h0 b\r\n Actual type: (>) (a0 > g0 b) (a0 > g0 b) a\r\n • In the first argument of ‘Ran’, namely ‘(ireturn a)’\r\n In the expression: Ran (ireturn a)\r\n In an equation for ‘ireturn’: ireturn a = Ran (ireturn a)\r\n \r\n17  ireturn a = Ran (ireturn a)\r\n  ^^^^^^^^^\r\nFailed, modules loaded: none.\r\n}}}\r\n\r\nIs GHC right to bring up unlifted types? I would guess this is due to the newly added levity polymorphism of `(>) :: TYPE rep > TYPE rep' > Type`","type_of_failure":"OtherFailure","blocking":[]} >This one does me 'ead in, I accidentally type `Ran` instead of `Swap`
```hs
{# Language RankNTypes, DerivingStrategies, TypeApplications, ScopedTypeVariables, GADTs, GeneralizedNewtypeDeriving, InstanceSigs, PolyKinds #}
import Data.Coerce
newtype Ran g h a = Ran (forall b. (a > g b) > h b)
newtype Swap p f g a where
Swap :: p g f a > Swap p f g a
deriving newtype
Show
class IxPointed m where
ireturn :: a > m i i a
instance IxPointed f => IxPointed (Swap f) where
ireturn :: forall a i. a > Swap f i i a
ireturn a = Ran (ireturn a)
```
and get this error
```
$ ghci ignoredotghci /tmp/bug.hs
GHCi, version 8.3.20170605: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( /tmp/bug.hs, interpreted )
/tmp/bug.hs:17:15: error:
• Couldn't match expected type ‘Swap f i i a’
with actual type ‘Ran g0 h0 a0’
• In the expression: Ran (ireturn a)
In an equation for ‘ireturn’: ireturn a = Ran (ireturn a)
In the instance declaration for ‘IxPointed (Swap f)’
• Relevant bindings include
a :: a (bound at /tmp/bug.hs:17:11)
ireturn :: a > Swap f i i a (bound at /tmp/bug.hs:17:3)

17  ireturn a = Ran (ireturn a)
 ^^^^^^^^^^^^^^^
/tmp/bug.hs:17:20: error:
• Couldn't match a lifted type with an unlifted type
Expected type: (a0 > g0 b) > h0 b
Actual type: (>) (a0 > g0 b) (a0 > g0 b) a
• In the first argument of ‘Ran’, namely ‘(ireturn a)’
In the expression: Ran (ireturn a)
In an equation for ‘ireturn’: ireturn a = Ran (ireturn a)

17  ireturn a = Ran (ireturn a)
 ^^^^^^^^^
Failed, modules loaded: none.
```
Is GHC right to bring up unlifted types? I would guess this is due to the newly added levity polymorphism of `(>) :: TYPE rep > TYPE rep' > Type`
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.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 mentions unlifted types out of the blue (to me anyway)","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This one does me 'ead in, I accidentally type `Ran` instead of `Swap` \r\n\r\n{{{#!hs\r\n{# Language RankNTypes, DerivingStrategies, TypeApplications, ScopedTypeVariables, GADTs, GeneralizedNewtypeDeriving, InstanceSigs, PolyKinds #}\r\n\r\nimport Data.Coerce\r\n\r\nnewtype Ran g h a = Ran (forall b. (a > g b) > h b)\r\n\r\nnewtype Swap p f g a where\r\n Swap :: p g f a > Swap p f g a\r\n deriving newtype\r\n Show\r\n\r\nclass IxPointed m where\r\n ireturn :: a > m i i a\r\n\r\ninstance IxPointed f => IxPointed (Swap f) where\r\n ireturn :: forall a i. a > Swap f i i a\r\n ireturn a = Ran (ireturn a)\r\n}}}\r\n\r\nand get this error\r\n\r\n{{{\r\n$ ghci ignoredotghci /tmp/bug.hs\r\nGHCi, version 8.3.20170605: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( /tmp/bug.hs, interpreted )\r\n\r\n/tmp/bug.hs:17:15: error:\r\n • Couldn't match expected type ‘Swap f i i a’\r\n with actual type ‘Ran g0 h0 a0’\r\n • In the expression: Ran (ireturn a)\r\n In an equation for ‘ireturn’: ireturn a = Ran (ireturn a)\r\n In the instance declaration for ‘IxPointed (Swap f)’\r\n • Relevant bindings include\r\n a :: a (bound at /tmp/bug.hs:17:11)\r\n ireturn :: a > Swap f i i a (bound at /tmp/bug.hs:17:3)\r\n \r\n17  ireturn a = Ran (ireturn a)\r\n  ^^^^^^^^^^^^^^^\r\n\r\n/tmp/bug.hs:17:20: error:\r\n • Couldn't match a lifted type with an unlifted type\r\n Expected type: (a0 > g0 b) > h0 b\r\n Actual type: (>) (a0 > g0 b) (a0 > g0 b) a\r\n • In the first argument of ‘Ran’, namely ‘(ireturn a)’\r\n In the expression: Ran (ireturn a)\r\n In an equation for ‘ireturn’: ireturn a = Ran (ireturn a)\r\n \r\n17  ireturn a = Ran (ireturn a)\r\n  ^^^^^^^^^\r\nFailed, modules loaded: none.\r\n}}}\r\n\r\nIs GHC right to bring up unlifted types? I would guess this is due to the newly added levity polymorphism of `(>) :: TYPE rep > TYPE rep' > Type`","type_of_failure":"OtherFailure","blocking":[]} >Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://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/14040Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2]20200123T19:31:02ZRyan ScottTyped holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2](Originally spun off from #13877.)
The following program gives a somewhat decent error message in GHC 8.0.1:
```hs
{# LANGUAGE GADTs #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeApplications #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
module Bug where
import Data.Kind
data family Sing (a :: k)
data WeirdList :: Type > Type where
WeirdNil :: WeirdList a
WeirdCons :: a > WeirdList (WeirdList a) > WeirdList a
data instance Sing (z :: WeirdList a) where
SWeirdNil :: Sing WeirdNil
SWeirdCons :: Sing w > Sing wws > Sing (WeirdCons w wws)
elimWeirdList :: forall (a :: Type) (wl :: WeirdList a)
(p :: forall (x :: Type). x > WeirdList x > Type).
Sing wl
> (forall (y :: Type). p _ WeirdNil)
> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x > Sing xs > p _ xs
> p _ (WeirdCons x xs))
> p _ wl
elimWeirdList SWeirdNil pWeirdNil _ = pWeirdNil
elimWeirdList (SWeirdCons (x :: Sing (x :: z))
(xs :: Sing (xs :: WeirdList (WeirdList z))))
pWeirdNil pWeirdCons
= pWeirdCons @z @x @xs x xs
(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)
```
```
$ /opt/ghc/8.0.1/bin/ghci Foo.hs
GHCi, version 8.0.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Foo.hs, interpreted )
Foo.hs:34:8: error:
• Cannot apply expression of type ‘Sing wl
> (forall y. p x0 t3 'WeirdNil)
> (forall z (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x
> Sing xs
> p (WeirdList z) t2 xs
> p z t1 ('WeirdCons x xs))
> p a t0 wl’
to a visible type argument ‘WeirdList z’
• In the sixth argument of ‘pWeirdCons’, namely
‘(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)’
In the expression:
pWeirdCons
@z
@x
@xs
x
xs
(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)
In an equation for ‘elimWeirdList’:
elimWeirdList
(SWeirdCons (x :: Sing (x :: z))
(xs :: Sing (xs :: WeirdList (WeirdList z))))
pWeirdNil
pWeirdCons
= pWeirdCons
@z
@x
@xs
x
xs
(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)
```
But in GHC 8.0.2, 8.2.1, and HEAD, it panics to varying degrees:
```
$ /opt/ghc/8.0.2/bin/ghci Foo.hs
GHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Foo.hs, interpreted )
Foo.hs:24:41: error:
• Found type wildcard ‘_’ standing for ‘t0’
Where: ‘t0’ is an ambiguous type variable
‘x0’ is an ambiguous type variable
To use the inferred type, enable PartialTypeSignatures
• In the type signature:
elimWeirdList :: forall (a :: Type)
(wl :: WeirdList a)
(p :: forall (x :: Type). x > WeirdList x > Type).
Sing wl
> (forall (y :: Type). p _ WeirdNil)
> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x > Sing xs > p _ xs > p _ (WeirdCons x xs))
> p _ wl
• Relevant bindings include
elimWeirdList :: Sing wl
> (forall y. p x0 t0 'WeirdNil)
> (forall z (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x
> Sing xs > p (WeirdList z) t1 xs > p z t2 ('WeirdCons x xs))
> p a t3 wl
(bound at Foo.hs:29:1)
Foo.hs:26:44: error:ghc: panic! (the 'impossible' happened)
(GHC version 8.0.2 for x86_64unknownlinux):
No skolem info: z_a13X[sk]
```
```
$ /opt/ghc/8.2.1/bin/ghci Foo.hs
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Foo.hs, interpreted )
Foo.hs:21:18: error:
• The kind of variable ‘wl1’, namely ‘WeirdList a1’,
depends on variable ‘a1’ from an inner scope
Perhaps bind ‘wl1’ sometime after binding ‘a1’
• In the type signature:
elimWeirdList :: forall (a :: Type)
(wl :: WeirdList a)
(p :: forall (x :: Type). x > WeirdList x > Type).
Sing wl
> (forall (y :: Type). p _ WeirdNil)
> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x > Sing xs > p _ xs > p _ (WeirdCons x xs))
> p _ wl

21  elimWeirdList :: forall (a :: Type) (wl :: WeirdList a)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
Foo.hs:24:41: error:
• Found type wildcard ‘_’ standing for ‘w0’
Where: ‘w0’ is an ambiguous type variable
‘x0’ is an ambiguous type variable
To use the inferred type, enable PartialTypeSignatures
• In the type signature:
elimWeirdList :: forall (a :: Type)
(wl :: WeirdList a)
(p :: forall (x :: Type). x > WeirdList x > Type).
Sing wl
> (forall (y :: Type). p _ WeirdNil)
> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x > Sing xs > p _ xs > p _ (WeirdCons x xs))
> p _ wl

24  > (forall (y :: Type). p _ WeirdNil)
 ^
Foo.hs:26:44: error:ghc: panic! (the 'impossible' happened)
(GHC version 8.2.1 for x86_64unknownlinux):
No skolem info:
z_a1sY[sk:2]
Call stack:
CallStack (from HasCallStack):
prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1133:58 in ghc:Outputable
callStackDoc, called at compiler/utils/Outputable.hs:1137:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcErrors.hs:2653:5 in ghc:TcErrors
```
(The error messages from HEAD, at commit 791947db6db32ef7d4772a821a0823e558e3c05b, are the same as in GHC 8.2.1.)
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.2 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  #13877 
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2]","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[13877],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.2","keywords":["PartialTypeSignatures","TypeFamilies,","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"(Originally spun off from #13877.)\r\n\r\nThe following program gives a somewhat decent error message in GHC 8.0.1:\r\n\r\n{{{#!hs\r\n{# LANGUAGE GADTs #}\r\n{# LANGUAGE RankNTypes #}\r\n{# LANGUAGE ScopedTypeVariables #}\r\n{# LANGUAGE TypeApplications #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeInType #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ndata family Sing (a :: k)\r\n\r\ndata WeirdList :: Type > Type where\r\n WeirdNil :: WeirdList a\r\n WeirdCons :: a > WeirdList (WeirdList a) > WeirdList a\r\n\r\ndata instance Sing (z :: WeirdList a) where\r\n SWeirdNil :: Sing WeirdNil\r\n SWeirdCons :: Sing w > Sing wws > Sing (WeirdCons w wws)\r\n\r\nelimWeirdList :: forall (a :: Type) (wl :: WeirdList a)\r\n (p :: forall (x :: Type). x > WeirdList x > Type).\r\n Sing wl\r\n > (forall (y :: Type). p _ WeirdNil)\r\n > (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).\r\n Sing x > Sing xs > p _ xs\r\n > p _ (WeirdCons x xs))\r\n > p _ wl\r\nelimWeirdList SWeirdNil pWeirdNil _ = pWeirdNil\r\nelimWeirdList (SWeirdCons (x :: Sing (x :: z))\r\n (xs :: Sing (xs :: WeirdList (WeirdList z))))\r\n pWeirdNil pWeirdCons\r\n = pWeirdCons @z @x @xs x xs\r\n (elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)\r\n}}}\r\n\r\n{{{\r\n$ /opt/ghc/8.0.1/bin/ghci Foo.hs \r\nGHCi, version 8.0.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Foo.hs, interpreted )\r\n\r\nFoo.hs:34:8: error:\r\n • Cannot apply expression of type ‘Sing wl\r\n > (forall y. p x0 t3 'WeirdNil)\r\n > (forall z (x :: z) (xs :: WeirdList (WeirdList z)).\r\n Sing x\r\n > Sing xs\r\n > p (WeirdList z) t2 xs\r\n > p z t1 ('WeirdCons x xs))\r\n > p a t0 wl’\r\n to a visible type argument ‘WeirdList z’\r\n • In the sixth argument of ‘pWeirdCons’, namely\r\n ‘(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)’\r\n In the expression:\r\n pWeirdCons\r\n @z\r\n @x\r\n @xs\r\n x\r\n xs\r\n (elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)\r\n In an equation for ‘elimWeirdList’:\r\n elimWeirdList\r\n (SWeirdCons (x :: Sing (x :: z))\r\n (xs :: Sing (xs :: WeirdList (WeirdList z))))\r\n pWeirdNil\r\n pWeirdCons\r\n = pWeirdCons\r\n @z\r\n @x\r\n @xs\r\n x\r\n xs\r\n (elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)\r\n}}}\r\n\r\nBut in GHC 8.0.2, 8.2.1, and HEAD, it panics to varying degrees:\r\n\r\n{{{\r\n$ /opt/ghc/8.0.2/bin/ghci Foo.hs \r\nGHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Foo.hs, interpreted )\r\n\r\nFoo.hs:24:41: error:\r\n • Found type wildcard ‘_’ standing for ‘t0’\r\n Where: ‘t0’ is an ambiguous type variable\r\n ‘x0’ is an ambiguous type variable\r\n To use the inferred type, enable PartialTypeSignatures\r\n • In the type signature:\r\n elimWeirdList :: forall (a :: Type)\r\n (wl :: WeirdList a)\r\n (p :: forall (x :: Type). x > WeirdList x > Type).\r\n Sing wl\r\n > (forall (y :: Type). p _ WeirdNil)\r\n > (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).\r\n Sing x > Sing xs > p _ xs > p _ (WeirdCons x xs))\r\n > p _ wl\r\n • Relevant bindings include\r\n elimWeirdList :: Sing wl\r\n > (forall y. p x0 t0 'WeirdNil)\r\n > (forall z (x :: z) (xs :: WeirdList (WeirdList z)).\r\n Sing x\r\n > Sing xs > p (WeirdList z) t1 xs > p z t2 ('WeirdCons x xs))\r\n > p a t3 wl\r\n (bound at Foo.hs:29:1)\r\n\r\nFoo.hs:26:44: error:ghc: panic! (the 'impossible' happened)\r\n (GHC version 8.0.2 for x86_64unknownlinux):\r\n\tNo skolem info: z_a13X[sk]\r\n}}}\r\n\r\n{{{\r\n$ /opt/ghc/8.2.1/bin/ghci Foo.hs \r\nGHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Foo.hs, interpreted )\r\n\r\nFoo.hs:21:18: error:\r\n • The kind of variable ‘wl1’, namely ‘WeirdList a1’,\r\n depends on variable ‘a1’ from an inner scope\r\n Perhaps bind ‘wl1’ sometime after binding ‘a1’\r\n • In the type signature:\r\n elimWeirdList :: forall (a :: Type)\r\n (wl :: WeirdList a)\r\n (p :: forall (x :: Type). x > WeirdList x > Type).\r\n Sing wl\r\n > (forall (y :: Type). p _ WeirdNil)\r\n > (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).\r\n Sing x > Sing xs > p _ xs > p _ (WeirdCons x xs))\r\n > p _ wl\r\n \r\n21  elimWeirdList :: forall (a :: Type) (wl :: WeirdList a)\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...\r\n\r\nFoo.hs:24:41: error:\r\n • Found type wildcard ‘_’ standing for ‘w0’\r\n Where: ‘w0’ is an ambiguous type variable\r\n ‘x0’ is an ambiguous type variable\r\n To use the inferred type, enable PartialTypeSignatures\r\n • In the type signature:\r\n elimWeirdList :: forall (a :: Type)\r\n (wl :: WeirdList a)\r\n (p :: forall (x :: Type). x > WeirdList x > Type).\r\n Sing wl\r\n > (forall (y :: Type). p _ WeirdNil)\r\n > (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).\r\n Sing x > Sing xs > p _ xs > p _ (WeirdCons x xs))\r\n > p _ wl\r\n \r\n24  > (forall (y :: Type). p _ WeirdNil)\r\n  ^\r\n\r\nFoo.hs:26:44: error:ghc: panic! (the 'impossible' happened)\r\n (GHC version 8.2.1 for x86_64unknownlinux):\r\n\tNo skolem info:\r\n z_a1sY[sk:2]\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1133:58 in ghc:Outputable\r\n callStackDoc, called at compiler/utils/Outputable.hs:1137:37 in ghc:Outputable\r\n pprPanic, called at compiler/typecheck/TcErrors.hs:2653:5 in ghc:TcErrors\r\n}}}\r\n\r\n(The error messages from HEAD, at commit 791947db6db32ef7d4772a821a0823e558e3c05b, are the same as in GHC 8.2.1.)","type_of_failure":"OtherFailure","blocking":[]} >(Originally spun off from #13877.)
The following program gives a somewhat decent error message in GHC 8.0.1:
```hs
{# LANGUAGE GADTs #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeApplications #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
module Bug where
import Data.Kind
data family Sing (a :: k)
data WeirdList :: Type > Type where
WeirdNil :: WeirdList a
WeirdCons :: a > WeirdList (WeirdList a) > WeirdList a
data instance Sing (z :: WeirdList a) where
SWeirdNil :: Sing WeirdNil
SWeirdCons :: Sing w > Sing wws > Sing (WeirdCons w wws)
elimWeirdList :: forall (a :: Type) (wl :: WeirdList a)
(p :: forall (x :: Type). x > WeirdList x > Type).
Sing wl
> (forall (y :: Type). p _ WeirdNil)
> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x > Sing xs > p _ xs
> p _ (WeirdCons x xs))
> p _ wl
elimWeirdList SWeirdNil pWeirdNil _ = pWeirdNil
elimWeirdList (SWeirdCons (x :: Sing (x :: z))
(xs :: Sing (xs :: WeirdList (WeirdList z))))
pWeirdNil pWeirdCons
= pWeirdCons @z @x @xs x xs
(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)
```
```
$ /opt/ghc/8.0.1/bin/ghci Foo.hs
GHCi, version 8.0.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Foo.hs, interpreted )
Foo.hs:34:8: error:
• Cannot apply expression of type ‘Sing wl
> (forall y. p x0 t3 'WeirdNil)
> (forall z (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x
> Sing xs
> p (WeirdList z) t2 xs
> p z t1 ('WeirdCons x xs))
> p a t0 wl’
to a visible type argument ‘WeirdList z’
• In the sixth argument of ‘pWeirdCons’, namely
‘(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)’
In the expression:
pWeirdCons
@z
@x
@xs
x
xs
(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)
In an equation for ‘elimWeirdList’:
elimWeirdList
(SWeirdCons (x :: Sing (x :: z))
(xs :: Sing (xs :: WeirdList (WeirdList z))))
pWeirdNil
pWeirdCons
= pWeirdCons
@z
@x
@xs
x
xs
(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)
```
But in GHC 8.0.2, 8.2.1, and HEAD, it panics to varying degrees:
```
$ /opt/ghc/8.0.2/bin/ghci Foo.hs
GHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Foo.hs, interpreted )
Foo.hs:24:41: error:
• Found type wildcard ‘_’ standing for ‘t0’
Where: ‘t0’ is an ambiguous type variable
‘x0’ is an ambiguous type variable
To use the inferred type, enable PartialTypeSignatures
• In the type signature:
elimWeirdList :: forall (a :: Type)
(wl :: WeirdList a)
(p :: forall (x :: Type). x > WeirdList x > Type).
Sing wl
> (forall (y :: Type). p _ WeirdNil)
> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x > Sing xs > p _ xs > p _ (WeirdCons x xs))
> p _ wl
• Relevant bindings include
elimWeirdList :: Sing wl
> (forall y. p x0 t0 'WeirdNil)
> (forall z (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x
> Sing xs > p (WeirdList z) t1 xs > p z t2 ('WeirdCons x xs))
> p a t3 wl
(bound at Foo.hs:29:1)
Foo.hs:26:44: error:ghc: panic! (the 'impossible' happened)
(GHC version 8.0.2 for x86_64unknownlinux):
No skolem info: z_a13X[sk]
```
```
$ /opt/ghc/8.2.1/bin/ghci Foo.hs
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Foo.hs, interpreted )
Foo.hs:21:18: error:
• The kind of variable ‘wl1’, namely ‘WeirdList a1’,
depends on variable ‘a1’ from an inner scope
Perhaps bind ‘wl1’ sometime after binding ‘a1’
• In the type signature:
elimWeirdList :: forall (a :: Type)
(wl :: WeirdList a)
(p :: forall (x :: Type). x > WeirdList x > Type).
Sing wl
> (forall (y :: Type). p _ WeirdNil)
> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x > Sing xs > p _ xs > p _ (WeirdCons x xs))
> p _ wl

21  elimWeirdList :: forall (a :: Type) (wl :: WeirdList a)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
Foo.hs:24:41: error:
• Found type wildcard ‘_’ standing for ‘w0’
Where: ‘w0’ is an ambiguous type variable
‘x0’ is an ambiguous type variable
To use the inferred type, enable PartialTypeSignatures
• In the type signature:
elimWeirdList :: forall (a :: Type)
(wl :: WeirdList a)
(p :: forall (x :: Type). x > WeirdList x > Type).
Sing wl
> (forall (y :: Type). p _ WeirdNil)
> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x > Sing xs > p _ xs > p _ (WeirdCons x xs))
> p _ wl

24  > (forall (y :: Type). p _ WeirdNil)
 ^
Foo.hs:26:44: error:ghc: panic! (the 'impossible' happened)
(GHC version 8.2.1 for x86_64unknownlinux):
No skolem info:
z_a1sY[sk:2]
Call stack:
CallStack (from HasCallStack):
prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1133:58 in ghc:Outputable
callStackDoc, called at compiler/utils/Outputable.hs:1137:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcErrors.hs:2653:5 in ghc:TcErrors
```
(The error messages from HEAD, at commit 791947db6db32ef7d4772a821a0823e558e3c05b, are the same as in GHC 8.2.1.)
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.2 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  #13877 
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2]","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[13877],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.2","keywords":["PartialTypeSignatures","TypeFamilies,","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"(Originally spun off from #13877.)\r\n\r\nThe following program gives a somewhat decent error message in GHC 8.0.1:\r\n\r\n{{{#!hs\r\n{# LANGUAGE GADTs #}\r\n{# LANGUAGE RankNTypes #}\r\n{# LANGUAGE ScopedTypeVariables #}\r\n{# LANGUAGE TypeApplications #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeInType #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ndata family Sing (a :: k)\r\n\r\ndata WeirdList :: Type > Type where\r\n WeirdNil :: WeirdList a\r\n WeirdCons :: a > WeirdList (WeirdList a) > WeirdList a\r\n\r\ndata instance Sing (z :: WeirdList a) where\r\n SWeirdNil :: Sing WeirdNil\r\n SWeirdCons :: Sing w > Sing wws > Sing (WeirdCons w wws)\r\n\r\nelimWeirdList :: forall (a :: Type) (wl :: WeirdList a)\r\n (p :: forall (x :: Type). x > WeirdList x > Type).\r\n Sing wl\r\n > (forall (y :: Type). p _ WeirdNil)\r\n > (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).\r\n Sing x > Sing xs > p _ xs\r\n > p _ (WeirdCons x xs))\r\n > p _ wl\r\nelimWeirdList SWeirdNil pWeirdNil _ = pWeirdNil\r\nelimWeirdList (SWeirdCons (x :: Sing (x :: z))\r\n (xs :: Sing (xs :: WeirdList (WeirdList z))))\r\n pWeirdNil pWeirdCons\r\n = pWeirdCons @z @x @xs x xs\r\n (elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)\r\n}}}\r\n\r\n{{{\r\n$ /opt/ghc/8.0.1/bin/ghci Foo.hs \r\nGHCi, version 8.0.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Foo.hs, interpreted )\r\n\r\nFoo.hs:34:8: error:\r\n • Cannot apply expression of type ‘Sing wl\r\n > (forall y. p x0 t3 'WeirdNil)\r\n > (forall z (x :: z) (xs :: WeirdList (WeirdList z)).\r\n Sing x\r\n > Sing xs\r\n > p (WeirdList z) t2 xs\r\n > p z t1 ('WeirdCons x xs))\r\n > p a t0 wl’\r\n to a visible type argument ‘WeirdList z’\r\n • In the sixth argument of ‘pWeirdCons’, namely\r\n ‘(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)’\r\n In the expression:\r\n pWeirdCons\r\n @z\r\n @x\r\n @xs\r\n x\r\n xs\r\n (elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)\r\n In an equation for ‘elimWeirdList’:\r\n elimWeirdList\r\n (SWeirdCons (x :: Sing (x :: z))\r\n (xs :: Sing (xs :: WeirdList (WeirdList z))))\r\n pWeirdNil\r\n pWeirdCons\r\n = pWeirdCons\r\n @z\r\n @x\r\n @xs\r\n x\r\n xs\r\n (elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)\r\n}}}\r\n\r\nBut in GHC 8.0.2, 8.2.1, and HEAD, it panics to varying degrees:\r\n\r\n{{{\r\n$ /opt/ghc/8.0.2/bin/ghci Foo.hs \r\nGHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Foo.hs, interpreted )\r\n\r\nFoo.hs:24:41: error:\r\n • Found type wildcard ‘_’ standing for ‘t0’\r\n Where: ‘t0’ is an ambiguous type variable\r\n ‘x0’ is an ambiguous type variable\r\n To use the inferred type, enable PartialTypeSignatures\r\n • In the type signature:\r\n elimWeirdList :: forall (a :: Type)\r\n (wl :: WeirdList a)\r\n (p :: forall (x :: Type). x > WeirdList x > Type).\r\n Sing wl\r\n > (forall (y :: Type). p _ WeirdNil)\r\n > (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).\r\n Sing x > Sing xs > p _ xs > p _ (WeirdCons x xs))\r\n > p _ wl\r\n • Relevant bindings include\r\n elimWeirdList :: Sing wl\r\n > (forall y. p x0 t0 'WeirdNil)\r\n > (forall z (x :: z) (xs :: WeirdList (WeirdList z)).\r\n Sing x\r\n > Sing xs > p (WeirdList z) t1 xs > p z t2 ('WeirdCons x xs))\r\n > p a t3 wl\r\n (bound at Foo.hs:29:1)\r\n\r\nFoo.hs:26:44: error:ghc: panic! (the 'impossible' happened)\r\n (GHC version 8.0.2 for x86_64unknownlinux):\r\n\tNo skolem info: z_a13X[sk]\r\n}}}\r\n\r\n{{{\r\n$ /opt/ghc/8.2.1/bin/ghci Foo.hs \r\nGHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Foo.hs, interpreted )\r\n\r\nFoo.hs:21:18: error:\r\n • The kind of variable ‘wl1’, namely ‘WeirdList a1’,\r\n depends on variable ‘a1’ from an inner scope\r\n Perhaps bind ‘wl1’ sometime after binding ‘a1’\r\n • In the type signature:\r\n elimWeirdList :: forall (a :: Type)\r\n (wl :: WeirdList a)\r\n (p :: forall (x :: Type). x > WeirdList x > Type).\r\n Sing wl\r\n > (forall (y :: Type). p _ WeirdNil)\r\n > (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).\r\n Sing x > Sing xs > p _ xs > p _ (WeirdCons x xs))\r\n > p _ wl\r\n \r\n21  elimWeirdList :: forall (a :: Type) (wl :: WeirdList a)\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...\r\n\r\nFoo.hs:24:41: error:\r\n • Found type wildcard ‘_’ standing for ‘w0’\r\n Where: ‘w0’ is an ambiguous type variable\r\n ‘x0’ is an ambiguous type variable\r\n To use the inferred type, enable PartialTypeSignatures\r\n • In the type signature:\r\n elimWeirdList :: forall (a :: Type)\r\n (wl :: WeirdList a)\r\n (p :: forall (x :: Type). x > WeirdList x > Type).\r\n Sing wl\r\n > (forall (y :: Type). p _ WeirdNil)\r\n > (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).\r\n Sing x > Sing xs > p _ xs > p _ (WeirdCons x xs))\r\n > p _ wl\r\n \r\n24  > (forall (y :: Type). p _ WeirdNil)\r\n  ^\r\n\r\nFoo.hs:26:44: error:ghc: panic! (the 'impossible' happened)\r\n (GHC version 8.2.1 for x86_64unknownlinux):\r\n\tNo skolem info:\r\n z_a1sY[sk:2]\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1133:58 in ghc:Outputable\r\n callStackDoc, called at compiler/utils/Outputable.hs:1137:37 in ghc:Outputable\r\n pprPanic, called at compiler/typecheck/TcErrors.hs:2653:5 in ghc:TcErrors\r\n}}}\r\n\r\n(The error messages from HEAD, at commit 791947db6db32ef7d4772a821a0823e558e3c05b, are the same as in GHC 8.2.1.)","type_of_failure":"OtherFailure","blocking":[]} >Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/13933Support Typeable instances for types with coercions20190707T18:19:21ZRichard Eisenbergrae@richarde.devSupport Typeable instances for types with coercionsIf I say
```hs
{# LANGUAGE GADTs, TypeApplications, TypeInType #}
module Bug where
import Type.Reflection
data G a where
MkG :: a ~ Bool => G a
rep = typeRep @MkG
```
I get
```
Bug.hs:10:7: error:
• No instance for (Typeable <>) arising from a use of ‘typeRep’
• In the expression: typeRep @MkG
In an equation for ‘rep’: rep = typeRep @MkG

10  rep = typeRep @MkG

```
First off, the error message is confusing, mentioning the mysterious `<>`. But more importantly, it would be nice if the `Typeable` mechanism supported coercions.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Support Typeable instances for types with coercions","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.3","keywords":["TypeInType,","Typeable"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"If I say\r\n\r\n{{{#!hs\r\n{# LANGUAGE GADTs, TypeApplications, TypeInType #}\r\n\r\nmodule Bug where\r\n\r\nimport Type.Reflection\r\n\r\ndata G a where\r\n MkG :: a ~ Bool => G a\r\n\r\nrep = typeRep @MkG\r\n}}}\r\n\r\nI get\r\n\r\n{{{\r\nBug.hs:10:7: error:\r\n • No instance for (Typeable <>) arising from a use of ‘typeRep’\r\n • In the expression: typeRep @MkG\r\n In an equation for ‘rep’: rep = typeRep @MkG\r\n \r\n10  rep = typeRep @MkG\r\n  \r\n}}}\r\n\r\nFirst off, the error message is confusing, mentioning the mysterious `<>`. But more importantly, it would be nice if the `Typeable` mechanism supported coercions.","type_of_failure":"OtherFailure","blocking":[]} >If I say
```hs
{# LANGUAGE GADTs, TypeApplications, TypeInType #}
module Bug where
import Type.Reflection
data G a where
MkG :: a ~ Bool => G a
rep = typeRep @MkG
```
I get
```
Bug.hs:10:7: error:
• No instance for (Typeable <>) arising from a use of ‘typeRep’
• In the expression: typeRep @MkG
In an equation for ‘rep’: rep = typeRep @MkG

10  rep = typeRep @MkG

```
First off, the error message is confusing, mentioning the mysterious `<>`. But more importantly, it would be nice if the `Typeable` mechanism supported coercions.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Support Typeable instances for types with coercions","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.3","keywords":["TypeInType,","Typeable"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"If I say\r\n\r\n{{{#!hs\r\n{# LANGUAGE GADTs, TypeApplications, TypeInType #}\r\n\r\nmodule Bug where\r\n\r\nimport Type.Reflection\r\n\r\ndata G a where\r\n MkG :: a ~ Bool => G a\r\n\r\nrep = typeRep @MkG\r\n}}}\r\n\r\nI get\r\n\r\n{{{\r\nBug.hs:10:7: error:\r\n • No instance for (Typeable <>) arising from a use of ‘typeRep’\r\n • In the expression: typeRep @MkG\r\n In an equation for ‘rep’: rep = typeRep @MkG\r\n \r\n10  rep = typeRep @MkG\r\n  \r\n}}}\r\n\r\nFirst off, the error message is confusing, mentioning the mysterious `<>`. But more importantly, it would be nice if the `Typeable` mechanism supported coercions.","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/13408Consider inferring a higherrank kind for type synonyms20200123T19:31:52ZRichard 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/12612Allow kinds of associated types to depend on earlier associated types20190707T18:25:50ZdavemenendezAllow kinds of associated types to depend on earlier associated typesGHC rejects the following code:
```hs
class C t where
type K t :: Type
type T t :: K t > Type
m :: t > T t a
```
with this error message
```
• Type constructor ‘K’ cannot be used here
(it is defined and used in the same recursive group)
• In the kind ‘K t > Type’
```
See [email discussion](https://mail.haskell.org/pipermail/glasgowhaskellusers/2016September/026402.html). This is connected to #12088, at least as far as defining instances of C.
<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":"Allow kinds of associated types to depend on earlier associated types","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"GHC rejects the following code:\r\n\r\n{{{#!hs\r\nclass C t where\r\n type K t :: Type\r\n type T t :: K t > Type\r\n\r\n m :: t > T t a\r\n}}}\r\n\r\nwith this error message\r\n\r\n{{{\r\n • Type constructor ‘K’ cannot be used here\r\n (it is defined and used in the same recursive group)\r\n • In the kind ‘K t > Type’\r\n}}}\r\n\r\nSee [https://mail.haskell.org/pipermail/glasgowhaskellusers/2016September/026402.html email discussion]. This is connected to #12088, at least as far as defining instances of C.","type_of_failure":"OtherFailure","blocking":[]} >GHC rejects the following code:
```hs
class C t where
type K t :: Type
type T t :: K t > Type
m :: t > T t a
```
with this error message
```
• Type constructor ‘K’ cannot be used here
(it is defined and used in the same recursive group)
• In the kind ‘K t > Type’
```
See [email discussion](https://mail.haskell.org/pipermail/glasgowhaskellusers/2016September/026402.html). This is connected to #12088, at least as far as defining instances of C.
<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":"Allow kinds of associated types to depend on earlier associated types","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"GHC rejects the following code:\r\n\r\n{{{#!hs\r\nclass C t where\r\n type K t :: Type\r\n type T t :: K t > Type\r\n\r\n m :: t > T t a\r\n}}}\r\n\r\nwith this error message\r\n\r\n{{{\r\n • Type constructor ‘K’ cannot be used here\r\n (it is defined and used in the same recursive group)\r\n • In the kind ‘K t > Type’\r\n}}}\r\n\r\nSee [https://mail.haskell.org/pipermail/glasgowhaskellusers/2016September/026402.html email discussion]. This is connected to #12088, at least as far as defining instances of C.","type_of_failure":"OtherFailure","blocking":[]} >https://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":[]} >