GHC issueshttps://gitlab.haskell.org/ghc/ghc//issues20190707T18:01:56Zhttps://gitlab.haskell.org/ghc/ghc//issues/16033Rankn typechecking regression between GHC 8.4 and 8.620190707T18:01:56ZRyan ScottRankn typechecking regression between GHC 8.4 and 8.6The following program typechecks on GHC 7.0.4 through 8.4.4:
```hs
{# LANGUAGE GADTs #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE ScopedTypeVariables #}
module Bug where
f :: (forall a. a > forall b. b > c) > ()
f (_ :: forall a. a > forall b. b > c) = ()
```
However, it does not typecheck on GHC 8.6.3:
```
$ /opt/ghc/8.6.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:7:4: error:
• Couldn't match type ‘b0 > c1’ with ‘forall b. b > c’
Expected type: a > forall b. b > c
Actual type: a > b0 > c1
• When checking that the pattern signature:
forall a. a > forall b. b > c
fits the type of its context: forall a. a > forall b. b > c1
In the pattern: _ :: forall a. a > forall b. b > c
In an equation for ‘f’:
f (_ :: forall a. a > forall b. b > c) = ()
• Relevant bindings include
f :: (forall a. a > forall b. b > c1) > () (bound at Bug.hs:7:1)

7  f (_ :: forall a. a > forall b. b > c) = ()
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```The following program typechecks on GHC 7.0.4 through 8.4.4:
```hs
{# LANGUAGE GADTs #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE ScopedTypeVariables #}
module Bug where
f :: (forall a. a > forall b. b > c) > ()
f (_ :: forall a. a > forall b. b > c) = ()
```
However, it does not typecheck on GHC 8.6.3:
```
$ /opt/ghc/8.6.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:7:4: error:
• Couldn't match type ‘b0 > c1’ with ‘forall b. b > c’
Expected type: a > forall b. b > c
Actual type: a > b0 > c1
• When checking that the pattern signature:
forall a. a > forall b. b > c
fits the type of its context: forall a. a > forall b. b > c1
In the pattern: _ :: forall a. a > forall b. b > c
In an equation for ‘f’:
f (_ :: forall a. a > forall b. b > c) = ()
• Relevant bindings include
f :: (forall a. a > forall b. b > c1) > () (bound at Bug.hs:7:1)

7  f (_ :: forall a. a > forall b. b > c) = ()
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```8.8.1https://gitlab.haskell.org/ghc/ghc//issues/15989Adding extra quantified constraints leads to resolution failure20190707T18:02:08ZerorAdding extra quantified constraints leads to resolution failure```
{# LANGUAGE QuantifiedConstraints, FlexibleContexts #}
import Control.Monad.Reader
data T x = T
ok :: ( forall x x'. MonadReader (T x) (m x') )
=> m y Bool
ok = fmap not (pure True)
bad :: ( forall x x'. MonadReader (T x) (m x')
, forall x. Monad (m x) )
=> m y Bool
bad = fmap not (pure True)
better :: ( forall x x'. MonadReader (T x) (m x')
, forall x. Applicative (m x)
, forall x. Functor (m x) )
=> m y Bool
better = fmap not (pure True)
```
`ok` and `better` compile, but `bad` fails to resolve, despite having strictly more in the context than `ok`:
```
BadQC.hs:15:7: error:
• Could not deduce (Functor (m y)) arising from a use of ‘fmap’
from the context: (forall x x'. MonadReader (T x) (m x'),
forall x. Monad (m x))
bound by the type signature for:
bad :: forall (m :: * > * > *) y.
(forall x x'. MonadReader (T x) (m x'), forall x. Monad (m x)) =>
m y Bool
at BadQC.hs:(12,1)(14,15)
• In the expression: fmap not (pure True)
In an equation for ‘bad’: bad = fmap not (pure True)

15  bad = fmap not (pure True)
 ^^^^^^^^^^^^^^^^^^^^
BadQC.hs:15:17: error:
• Could not deduce (Applicative (m y)) arising from a use of ‘pure’
from the context: (forall x x'. MonadReader (T x) (m x'),
forall x. Monad (m x))
bound by the type signature for:
bad :: forall (m :: * > * > *) y.
(forall x x'. MonadReader (T x) (m x'), forall x. Monad (m x)) =>
m y Bool
at BadQC.hs:(12,1)(14,15)
• In the second argument of ‘fmap’, namely ‘(pure True)’
In the expression: fmap not (pure True)
In an equation for ‘bad’: bad = fmap not (pure True)

15  bad = fmap not (pure True)
 ^^^^^^^^^
Failed, no modules loaded.
```
Also:
 `( forall x. MonadReader (T x) (m x), forall x. Monad (m x) )` compiles — the error seems to require two quantified type variables
 `( forall x x'. Monad (m x), forall x. Monad (m x) )` reports an ambiguity error on the constraint, which makes sense; if I turn on `AllowAmbiguousTypes`, it fails with the same error as above — the error isn't caused by MPTCs, and it doesn't matter that `x'` is unused
 `( forall x x'. Foldable (m x), forall x. Monad (m x) )` and `( forall x x'. Monad (m x), forall x. Foldable (m x) )` compile — being in the same class hierarchy matters
 `( forall x x'. Applicative (m x), forall x. Monad (m x) )` fails on `fmap` (but not `pure`) — which is the superclass doesn't seem to matter```
{# LANGUAGE QuantifiedConstraints, FlexibleContexts #}
import Control.Monad.Reader
data T x = T
ok :: ( forall x x'. MonadReader (T x) (m x') )
=> m y Bool
ok = fmap not (pure True)
bad :: ( forall x x'. MonadReader (T x) (m x')
, forall x. Monad (m x) )
=> m y Bool
bad = fmap not (pure True)
better :: ( forall x x'. MonadReader (T x) (m x')
, forall x. Applicative (m x)
, forall x. Functor (m x) )
=> m y Bool
better = fmap not (pure True)
```
`ok` and `better` compile, but `bad` fails to resolve, despite having strictly more in the context than `ok`:
```
BadQC.hs:15:7: error:
• Could not deduce (Functor (m y)) arising from a use of ‘fmap’
from the context: (forall x x'. MonadReader (T x) (m x'),
forall x. Monad (m x))
bound by the type signature for:
bad :: forall (m :: * > * > *) y.
(forall x x'. MonadReader (T x) (m x'), forall x. Monad (m x)) =>
m y Bool
at BadQC.hs:(12,1)(14,15)
• In the expression: fmap not (pure True)
In an equation for ‘bad’: bad = fmap not (pure True)

15  bad = fmap not (pure True)
 ^^^^^^^^^^^^^^^^^^^^
BadQC.hs:15:17: error:
• Could not deduce (Applicative (m y)) arising from a use of ‘pure’
from the context: (forall x x'. MonadReader (T x) (m x'),
forall x. Monad (m x))
bound by the type signature for:
bad :: forall (m :: * > * > *) y.
(forall x x'. MonadReader (T x) (m x'), forall x. Monad (m x)) =>
m y Bool
at BadQC.hs:(12,1)(14,15)
• In the second argument of ‘fmap’, namely ‘(pure True)’
In the expression: fmap not (pure True)
In an equation for ‘bad’: bad = fmap not (pure True)

15  bad = fmap not (pure True)
 ^^^^^^^^^
Failed, no modules loaded.
```
Also:
 `( forall x. MonadReader (T x) (m x), forall x. Monad (m x) )` compiles — the error seems to require two quantified type variables
 `( forall x x'. Monad (m x), forall x. Monad (m x) )` reports an ambiguity error on the constraint, which makes sense; if I turn on `AllowAmbiguousTypes`, it fails with the same error as above — the error isn't caused by MPTCs, and it doesn't matter that `x'` is unused
 `( forall x x'. Foldable (m x), forall x. Monad (m x) )` and `( forall x x'. Monad (m x), forall x. Foldable (m x) )` compile — being in the same class hierarchy matters
 `( forall x x'. Applicative (m x), forall x. Monad (m x) )` fails on `fmap` (but not `pure`) — which is the superclass doesn't seem to matter8.6.3https://gitlab.haskell.org/ghc/ghc//issues/15962Type family & typeclass interaction suppresses errors20190707T18:02:16ZmadgenType family & typeclass interaction suppresses errorsThe following program despite having a hole and an undefined variable `iDontExist` \*quietly\* fails to compile on 8.4.3 and 8.4.4. It produces errors as expected on 8.6.1 and 8.6.2.
By quietly failing, I mean it fails on CLI but without producing any error messages and in GHCI. It just says "Failed, no modules loaded."
```hs
{# LANGUAGE GADTs #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeOperators #}
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE FlexibleInstances #}
module Bug where
import Data.Kind (Type)
type Exp a = a > Type
type family Eval (e :: Exp a) :: a
data OpKind = Conjunction
data Dual (k :: OpKind) :: Exp OpKind
data Map :: (a > Exp b) > [ a ] > Exp [ b ]
type instance Eval (Map f (a ': as)) = Eval (f a) ': Eval (Map f as)
data Big :: [ OpKind ] > Type where
Big :: [ Big ks ] > Big ('Conjunction ': ks)
dualBig :: Big ks > Big (Eval (Map Dual ks))
dualBig = _
instance Semigroup (Big a) where
Big xs <> Big ys = Big (xs <> ys)
instance Monoid (Big ('Conjunction ': ks)) where
mempty = iDontExist
flatten :: Monoid (Big ks) => Big (k ': k ': ks) > Big ks
flatten = undefined
```
Sorry, the example is a bit big but almost any change causes the errors to appear again including the `Monoid` constraint on `flatten`.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.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":"Type family & typeclass interaction suppresses errors","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"⊥","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["error","family,","message","type","typeclass,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program despite having a hole and an undefined variable `iDontExist` *quietly* fails to compile on 8.4.3 and 8.4.4. It produces errors as expected on 8.6.1 and 8.6.2.\r\n\r\nBy quietly failing, I mean it fails on CLI but without producing any error messages and in GHCI. It just says \"Failed, no modules loaded.\"\r\n\r\n{{{#!hs\r\n{# LANGUAGE GADTs #}\r\n{# LANGUAGE TypeInType #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeOperators #}\r\n{# LANGUAGE FlexibleContexts #}\r\n{# LANGUAGE FlexibleInstances #}\r\n\r\nmodule Bug where\r\n\r\nimport Data.Kind (Type)\r\n\r\ntype Exp a = a > Type\r\ntype family Eval (e :: Exp a) :: a\r\n\r\ndata OpKind = Conjunction\r\n\r\ndata Dual (k :: OpKind) :: Exp OpKind\r\n\r\ndata Map :: (a > Exp b) > [ a ] > Exp [ b ]\r\n\r\ntype instance Eval (Map f (a ': as)) = Eval (f a) ': Eval (Map f as)\r\n\r\ndata Big :: [ OpKind ] > Type where\r\n Big :: [ Big ks ] > Big ('Conjunction ': ks)\r\n\r\ndualBig :: Big ks > Big (Eval (Map Dual ks))\r\ndualBig = _\r\n\r\ninstance Semigroup (Big a) where\r\n Big xs <> Big ys = Big (xs <> ys)\r\n\r\ninstance Monoid (Big ('Conjunction ': ks)) where\r\n mempty = iDontExist\r\n\r\nflatten :: Monoid (Big ks) => Big (k ': k ': ks) > Big ks\r\nflatten = undefined\r\n}}} \r\n\r\nSorry, the example is a bit big but almost any change causes the errors to appear again including the `Monoid` constraint on `flatten`.","type_of_failure":"OtherFailure","blocking":[]} >The following program despite having a hole and an undefined variable `iDontExist` \*quietly\* fails to compile on 8.4.3 and 8.4.4. It produces errors as expected on 8.6.1 and 8.6.2.
By quietly failing, I mean it fails on CLI but without producing any error messages and in GHCI. It just says "Failed, no modules loaded."
```hs
{# LANGUAGE GADTs #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeOperators #}
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE FlexibleInstances #}
module Bug where
import Data.Kind (Type)
type Exp a = a > Type
type family Eval (e :: Exp a) :: a
data OpKind = Conjunction
data Dual (k :: OpKind) :: Exp OpKind
data Map :: (a > Exp b) > [ a ] > Exp [ b ]
type instance Eval (Map f (a ': as)) = Eval (f a) ': Eval (Map f as)
data Big :: [ OpKind ] > Type where
Big :: [ Big ks ] > Big ('Conjunction ': ks)
dualBig :: Big ks > Big (Eval (Map Dual ks))
dualBig = _
instance Semigroup (Big a) where
Big xs <> Big ys = Big (xs <> ys)
instance Monoid (Big ('Conjunction ': ks)) where
mempty = iDontExist
flatten :: Monoid (Big ks) => Big (k ': k ': ks) > Big ks
flatten = undefined
```
Sorry, the example is a bit big but almost any change causes the errors to appear again including the `Monoid` constraint on `flatten`.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.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":"Type family & typeclass interaction suppresses errors","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"⊥","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["error","family,","message","type","typeclass,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program despite having a hole and an undefined variable `iDontExist` *quietly* fails to compile on 8.4.3 and 8.4.4. It produces errors as expected on 8.6.1 and 8.6.2.\r\n\r\nBy quietly failing, I mean it fails on CLI but without producing any error messages and in GHCI. It just says \"Failed, no modules loaded.\"\r\n\r\n{{{#!hs\r\n{# LANGUAGE GADTs #}\r\n{# LANGUAGE TypeInType #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeOperators #}\r\n{# LANGUAGE FlexibleContexts #}\r\n{# LANGUAGE FlexibleInstances #}\r\n\r\nmodule Bug where\r\n\r\nimport Data.Kind (Type)\r\n\r\ntype Exp a = a > Type\r\ntype family Eval (e :: Exp a) :: a\r\n\r\ndata OpKind = Conjunction\r\n\r\ndata Dual (k :: OpKind) :: Exp OpKind\r\n\r\ndata Map :: (a > Exp b) > [ a ] > Exp [ b ]\r\n\r\ntype instance Eval (Map f (a ': as)) = Eval (f a) ': Eval (Map f as)\r\n\r\ndata Big :: [ OpKind ] > Type where\r\n Big :: [ Big ks ] > Big ('Conjunction ': ks)\r\n\r\ndualBig :: Big ks > Big (Eval (Map Dual ks))\r\ndualBig = _\r\n\r\ninstance Semigroup (Big a) where\r\n Big xs <> Big ys = Big (xs <> ys)\r\n\r\ninstance Monoid (Big ('Conjunction ': ks)) where\r\n mempty = iDontExist\r\n\r\nflatten :: Monoid (Big ks) => Big (k ': k ': ks) > Big ks\r\nflatten = undefined\r\n}}} \r\n\r\nSorry, the example is a bit big but almost any change causes the errors to appear again including the `Monoid` constraint on `flatten`.","type_of_failure":"OtherFailure","blocking":[]} >8.8.1https://gitlab.haskell.org/ghc/ghc//issues/15954LiberalTypeSynonyms unsaturation check doesn't kick in20190707T18:02:18ZRyan ScottLiberalTypeSynonyms unsaturation check doesn't kick inGHC accepts this program:
```hs
{# LANGUAGE ImpredicativeTypes #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE RankNTypes #}
module Bug where
import GHC.Exts (Any)
type KindOf (a :: k) = k
type A a = (Any :: a)
type KA = KindOf A
```
But it really oughtn't to. After all, we have an unsaturated use of `A` in `KindOf A`, and we don't have `LiberalTypeSynonyms` enabled!
What's even stranger is that there seems to be something about this exact setup that sneaks by `LiberalTypeSynonyms`' validity checks. If I add another argument to `A`:
```hs
type A x a = (Any :: a)
```
Then it //does// error:
```
$ /opt/ghc/8.6.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:10:1: error:
• Illegal polymorphic type: forall a > a
Perhaps you intended to use LiberalTypeSynonyms
• In the type synonym declaration for ‘KA’

10  type KA = KindOf A
 ^^^^^^^^^^^^^^^^^^
```
Similarly, if I use something besides `KindOf`:
```hs
{# LANGUAGE ImpredicativeTypes #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE RankNTypes #}
module Bug where
import GHC.Exts (Any)
type A a = (Any :: a)
type B a = Int
type C = B A
```
Then I also get the same `Illegal polymorphic type: forall a > a` error.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.2 
 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":"LiberalTypeSynonyms unsaturation check doesn't kick in","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.3","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"GHC accepts this program:\r\n\r\n{{{#!hs\r\n{# LANGUAGE ImpredicativeTypes #}\r\n{# LANGUAGE PolyKinds #}\r\n{# LANGUAGE RankNTypes #}\r\nmodule Bug where\r\n\r\nimport GHC.Exts (Any)\r\n\r\ntype KindOf (a :: k) = k\r\ntype A a = (Any :: a)\r\ntype KA = KindOf A\r\n}}}\r\n\r\nBut it really oughtn't to. After all, we have an unsaturated use of `A` in `KindOf A`, and we don't have `LiberalTypeSynonyms` enabled!\r\n\r\nWhat's even stranger is that there seems to be something about this exact setup that sneaks by `LiberalTypeSynonyms`' validity checks. If I add another argument to `A`:\r\n\r\n{{{#!hs\r\ntype A x a = (Any :: a)\r\n}}}\r\n\r\nThen it //does// error:\r\n\r\n{{{\r\n$ /opt/ghc/8.6.2/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:10:1: error:\r\n • Illegal polymorphic type: forall a > a\r\n Perhaps you intended to use LiberalTypeSynonyms\r\n • In the type synonym declaration for ‘KA’\r\n \r\n10  type KA = KindOf A\r\n  ^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nSimilarly, if I use something besides `KindOf`:\r\n\r\n{{{#!hs\r\n{# LANGUAGE ImpredicativeTypes #}\r\n{# LANGUAGE PolyKinds #}\r\n{# LANGUAGE RankNTypes #}\r\nmodule Bug where\r\n\r\nimport GHC.Exts (Any)\r\n\r\ntype A a = (Any :: a)\r\ntype B a = Int\r\ntype C = B A\r\n}}}\r\n\r\nThen I also get the same `Illegal polymorphic type: forall a > a` error.","type_of_failure":"OtherFailure","blocking":[]} >GHC accepts this program:
```hs
{# LANGUAGE ImpredicativeTypes #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE RankNTypes #}
module Bug where
import GHC.Exts (Any)
type KindOf (a :: k) = k
type A a = (Any :: a)
type KA = KindOf A
```
But it really oughtn't to. After all, we have an unsaturated use of `A` in `KindOf A`, and we don't have `LiberalTypeSynonyms` enabled!
What's even stranger is that there seems to be something about this exact setup that sneaks by `LiberalTypeSynonyms`' validity checks. If I add another argument to `A`:
```hs
type A x a = (Any :: a)
```
Then it //does// error:
```
$ /opt/ghc/8.6.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:10:1: error:
• Illegal polymorphic type: forall a > a
Perhaps you intended to use LiberalTypeSynonyms
• In the type synonym declaration for ‘KA’

10  type KA = KindOf A
 ^^^^^^^^^^^^^^^^^^
```
Similarly, if I use something besides `KindOf`:
```hs
{# LANGUAGE ImpredicativeTypes #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE RankNTypes #}
module Bug where
import GHC.Exts (Any)
type A a = (Any :: a)
type B a = Int
type C = B A
```
Then I also get the same `Illegal polymorphic type: forall a > a` error.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.2 
 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":"LiberalTypeSynonyms unsaturation check doesn't kick in","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.3","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"GHC accepts this program:\r\n\r\n{{{#!hs\r\n{# LANGUAGE ImpredicativeTypes #}\r\n{# LANGUAGE PolyKinds #}\r\n{# LANGUAGE RankNTypes #}\r\nmodule Bug where\r\n\r\nimport GHC.Exts (Any)\r\n\r\ntype KindOf (a :: k) = k\r\ntype A a = (Any :: a)\r\ntype KA = KindOf A\r\n}}}\r\n\r\nBut it really oughtn't to. After all, we have an unsaturated use of `A` in `KindOf A`, and we don't have `LiberalTypeSynonyms` enabled!\r\n\r\nWhat's even stranger is that there seems to be something about this exact setup that sneaks by `LiberalTypeSynonyms`' validity checks. If I add another argument to `A`:\r\n\r\n{{{#!hs\r\ntype A x a = (Any :: a)\r\n}}}\r\n\r\nThen it //does// error:\r\n\r\n{{{\r\n$ /opt/ghc/8.6.2/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:10:1: error:\r\n • Illegal polymorphic type: forall a > a\r\n Perhaps you intended to use LiberalTypeSynonyms\r\n • In the type synonym declaration for ‘KA’\r\n \r\n10  type KA = KindOf A\r\n  ^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nSimilarly, if I use something besides `KindOf`:\r\n\r\n{{{#!hs\r\n{# LANGUAGE ImpredicativeTypes #}\r\n{# LANGUAGE PolyKinds #}\r\n{# LANGUAGE RankNTypes #}\r\nmodule Bug where\r\n\r\nimport GHC.Exts (Any)\r\n\r\ntype A a = (Any :: a)\r\ntype B a = Int\r\ntype C = B A\r\n}}}\r\n\r\nThen I also get the same `Illegal polymorphic type: forall a > a` error.","type_of_failure":"OtherFailure","blocking":[]} >8.8.1https://gitlab.haskell.org/ghc/ghc//issues/15883GHC panic: newtype F rep = F (forall (a :: TYPE rep). a)20200117T16:43:24ZIcelandjackGHC panic: newtype F rep = F (forall (a :: TYPE rep). a)```hs
{# Language RankNTypes #}
{# Language KindSignatures #}
{# Language PolyKinds #}
import GHC.Exts
newtype Foo rep = MkFoo (forall (a :: TYPE rep). a)
```
```
$ ~/code/unmodifiedghc/inplace/bin/ghcstage2 interactive ignoredotghci /tmp/U.hs
GHCi, version 8.7.20181029: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( /tmp/U.hs, interpreted )
ghcstage2: panic! (the 'impossible' happened)
(GHC version 8.7.20181029 for x86_64unknownlinux):
isUnliftedType
forall (a :: TYPE rep_a1AA[sk:0]). a :: TYPE rep_a1AA[sk:0]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable
pprPanic, called at compiler/types/Type.hs:2332:10 in ghc:Type
isUnliftedType, called at compiler/typecheck/TcTyClsDecls.hs:3055:25 in ghc:TcTyClsDecls
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
>
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.2 
 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 panic: newtype F rep = F (forall (a :: TYPE rep). a)","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.3","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{# Language RankNTypes #}\r\n{# Language KindSignatures #}\r\n{# Language PolyKinds #}\r\n\r\nimport GHC.Exts\r\n\r\nnewtype Foo rep = MkFoo (forall (a :: TYPE rep). a)\r\n}}}\r\n\r\n{{{\r\n$ ~/code/unmodifiedghc/inplace/bin/ghcstage2 interactive ignoredotghci /tmp/U.hs\r\nGHCi, version 8.7.20181029: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( /tmp/U.hs, interpreted )\r\nghcstage2: panic! (the 'impossible' happened)\r\n (GHC version 8.7.20181029 for x86_64unknownlinux):\r\n isUnliftedType\r\n forall (a :: TYPE rep_a1AA[sk:0]). a :: TYPE rep_a1AA[sk:0]\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/types/Type.hs:2332:10 in ghc:Type\r\n isUnliftedType, called at compiler/typecheck/TcTyClsDecls.hs:3055:25 in ghc:TcTyClsDecls\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n\r\n>\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >```hs
{# Language RankNTypes #}
{# Language KindSignatures #}
{# Language PolyKinds #}
import GHC.Exts
newtype Foo rep = MkFoo (forall (a :: TYPE rep). a)
```
```
$ ~/code/unmodifiedghc/inplace/bin/ghcstage2 interactive ignoredotghci /tmp/U.hs
GHCi, version 8.7.20181029: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( /tmp/U.hs, interpreted )
ghcstage2: panic! (the 'impossible' happened)
(GHC version 8.7.20181029 for x86_64unknownlinux):
isUnliftedType
forall (a :: TYPE rep_a1AA[sk:0]). a :: TYPE rep_a1AA[sk:0]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable
pprPanic, called at compiler/types/Type.hs:2332:10 in ghc:Type
isUnliftedType, called at compiler/typecheck/TcTyClsDecls.hs:3055:25 in ghc:TcTyClsDecls
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
>
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.2 
 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 panic: newtype F rep = F (forall (a :: TYPE rep). a)","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.3","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{# Language RankNTypes #}\r\n{# Language KindSignatures #}\r\n{# Language PolyKinds #}\r\n\r\nimport GHC.Exts\r\n\r\nnewtype Foo rep = MkFoo (forall (a :: TYPE rep). a)\r\n}}}\r\n\r\n{{{\r\n$ ~/code/unmodifiedghc/inplace/bin/ghcstage2 interactive ignoredotghci /tmp/U.hs\r\nGHCi, version 8.7.20181029: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( /tmp/U.hs, interpreted )\r\nghcstage2: panic! (the 'impossible' happened)\r\n (GHC version 8.7.20181029 for x86_64unknownlinux):\r\n isUnliftedType\r\n forall (a :: TYPE rep_a1AA[sk:0]). a :: TYPE rep_a1AA[sk:0]\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/types/Type.hs:2332:10 in ghc:Type\r\n isUnliftedType, called at compiler/typecheck/TcTyClsDecls.hs:3055:25 in ghc:TcTyClsDecls\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n\r\n>\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >8.10.1https://gitlab.haskell.org/ghc/ghc//issues/15869Discrepancy between seemingly equivalent type synonym and type family20190707T18:02:38ZRyan ScottDiscrepancy between seemingly equivalent type synonym and type familyConsider the following code:
```hs
{# LANGUAGE DataKinds #}
{# LANGUAGE ImpredicativeTypes #}
{# LANGUAGE LiberalTypeSynonyms #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
module Bug where
import Data.Kind
type KindOf1 (a :: k) = k
type family KindOf2 (a :: k) :: Type where
KindOf2 (a :: k) = k
data A (a :: Type) :: a > Type
type family Apply1 (f :: KindOf1 A) (a :: Type) (x :: a) :: Type where
Apply1 f a x = f a x
```
`Apply1` kindchecks, which is just peachy. Note that `Apply1` uses `KindOf1`, which is a type synonym. Suppose I wanted to swap out `KindOf1` for `KindOf2`, which is (seemingly) an equivalent type family. I can define this:
```hs
type family Apply2 (f :: KindOf2 A)  (f :: forall a > a > Type)
(a :: Type)
(x :: a)
:: Type where
Apply2 f a x = f a x
```
However, GHC rejects this!
```
$ /opt/ghc/8.6.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:25:10: error:
• Expecting two more arguments to ‘f’
Expected kind ‘KindOf2 A’, but ‘f’ has kind ‘* > a > *’
• In the first argument of ‘Apply2’, namely ‘f’
In the type family declaration for ‘Apply2’

25  Apply2 f a x = f a x
 ^
```
I find this quite surprising, since I would have expected `KindOf1` and `KindOf2` to be functionally equivalent. Even providing explicit `forall`s does not make it kindcheck:
```hs
type family Apply2 (f :: KindOf2 A)  (f :: forall a > a > Type)
(a :: Type)
(x :: a)
:: Type where
forall (f :: KindOf2 A) (a :: Type) (x :: a).
Apply2 f a x = f a x
```
Although the error message does change a bit:
```
$ ~/Software/ghc3/inplace/bin/ghcstage2 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:26:20: error:
• Expected kind ‘* > a > *’, but ‘f’ has kind ‘KindOf2 A’
• In the type ‘f a x’
In the type family declaration for ‘Apply2’

26  Apply2 f a x = f a x
 ^^^^^
```Consider the following code:
```hs
{# LANGUAGE DataKinds #}
{# LANGUAGE ImpredicativeTypes #}
{# LANGUAGE LiberalTypeSynonyms #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
module Bug where
import Data.Kind
type KindOf1 (a :: k) = k
type family KindOf2 (a :: k) :: Type where
KindOf2 (a :: k) = k
data A (a :: Type) :: a > Type
type family Apply1 (f :: KindOf1 A) (a :: Type) (x :: a) :: Type where
Apply1 f a x = f a x
```
`Apply1` kindchecks, which is just peachy. Note that `Apply1` uses `KindOf1`, which is a type synonym. Suppose I wanted to swap out `KindOf1` for `KindOf2`, which is (seemingly) an equivalent type family. I can define this:
```hs
type family Apply2 (f :: KindOf2 A)  (f :: forall a > a > Type)
(a :: Type)
(x :: a)
:: Type where
Apply2 f a x = f a x
```
However, GHC rejects this!
```
$ /opt/ghc/8.6.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:25:10: error:
• Expecting two more arguments to ‘f’
Expected kind ‘KindOf2 A’, but ‘f’ has kind ‘* > a > *’
• In the first argument of ‘Apply2’, namely ‘f’
In the type family declaration for ‘Apply2’

25  Apply2 f a x = f a x
 ^
```
I find this quite surprising, since I would have expected `KindOf1` and `KindOf2` to be functionally equivalent. Even providing explicit `forall`s does not make it kindcheck:
```hs
type family Apply2 (f :: KindOf2 A)  (f :: forall a > a > Type)
(a :: Type)
(x :: a)
:: Type where
forall (f :: KindOf2 A) (a :: Type) (x :: a).
Apply2 f a x = f a x
```
Although the error message does change a bit:
```
$ ~/Software/ghc3/inplace/bin/ghcstage2 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:26:20: error:
• Expected kind ‘* > a > *’, but ‘f’ has kind ‘KindOf2 A’
• In the type ‘f a x’
In the type family declaration for ‘Apply2’

26  Apply2 f a x = f a x
 ^^^^^
```https://gitlab.haskell.org/ghc/ghc//issues/15829Add a test case for tricky type synonyms involving visible dependent kinds20190707T18:02:49ZRyan ScottAdd a test case for tricky type synonyms involving visible dependent kindsThis code does not typecheck on GHC 8.6.1:
```hs
{# LANGUAGE DataKinds #}
{# LANGUAGE PolyKinds #}
module Bug where
import Data.Kind
data A :: Type > Type
data B a :: A a > Type
type C a = B a
```
However, it //does// typecheck on GHC HEAD, after commit 5e45ad10ffca1ad175b10f6ef3327e1ed8ba25f3 (Finish fix for #14880.). This is very cool, although it does alarm me that there is no test case which checks for this at the moment. Let's add one to ensure that this stays fixed.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.7 
 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":"Add a test case for tricky type synonyms involving visible dependent kinds","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.8.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.7","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This code does not typecheck on GHC 8.6.1:\r\n\r\n{{{#!hs\r\n{# LANGUAGE DataKinds #}\r\n{# LANGUAGE PolyKinds #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ndata A :: Type > Type\r\ndata B a :: A a > Type\r\ntype C a = B a\r\n}}}\r\n\r\nHowever, it //does// typecheck on GHC HEAD, after commit 5e45ad10ffca1ad175b10f6ef3327e1ed8ba25f3 (Finish fix for #14880.). This is very cool, although it does alarm me that there is no test case which checks for this at the moment. Let's add one to ensure that this stays fixed.","type_of_failure":"OtherFailure","blocking":[]} >This code does not typecheck on GHC 8.6.1:
```hs
{# LANGUAGE DataKinds #}
{# LANGUAGE PolyKinds #}
module Bug where
import Data.Kind
data A :: Type > Type
data B a :: A a > Type
type C a = B a
```
However, it //does// typecheck on GHC HEAD, after commit 5e45ad10ffca1ad175b10f6ef3327e1ed8ba25f3 (Finish fix for #14880.). This is very cool, although it does alarm me that there is no test case which checks for this at the moment. Let's add one to ensure that this stays fixed.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.7 
 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":"Add a test case for tricky type synonyms involving visible dependent kinds","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.8.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.7","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This code does not typecheck on GHC 8.6.1:\r\n\r\n{{{#!hs\r\n{# LANGUAGE DataKinds #}\r\n{# LANGUAGE PolyKinds #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ndata A :: Type > Type\r\ndata B a :: A a > Type\r\ntype C a = B a\r\n}}}\r\n\r\nHowever, it //does// typecheck on GHC HEAD, after commit 5e45ad10ffca1ad175b10f6ef3327e1ed8ba25f3 (Finish fix for #14880.). This is very cool, although it does alarm me that there is no test case which checks for this at the moment. Let's add one to ensure that this stays fixed.","type_of_failure":"OtherFailure","blocking":[]} >8.8.1https://gitlab.haskell.org/ghc/ghc//issues/15796Core Lint error with invalid newtype declaration20190707T18:02:56ZIcelandjackCore Lint error with invalid newtype declarationThis gives a Core Lint error
```hs
{# Language QuantifiedConstraints #}
{# Language TypeApplications #}
{# Language TypeOperators #}
{# Language PolyKinds #}
{# Language FlexibleInstances #}
{# Language DataKinds #}
{# Language TypeFamilies #}
{# Language MultiParamTypeClasses #}
{# Language ConstraintKinds #}
{# Language UndecidableInstances #}
{# Language GADTs #}
{# Options_GHC dcorelint #}
import Data.Kind
type Cat ob = ob > ob > Type
class Ríki (obj :: Type) where
type (>) :: Cat obj
class Varpi (f :: dom > cod)
newtype
(··>) :: Cat (a > b) where
Natu :: Varpi f
=> (forall xx. f xx > f' xx)
> (f ··> f')
instance
Ríki cod
=> 
Ríki (dom > cod)
where
type (>) = (··>) @dom @cod
```
```
$ ghci ignoredotghci 568_bug.hs
GHCi, version 8.7.20181017: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( 568_bug.hs, interpreted )
ghcstage2: panic! (the 'impossible' happened)
(GHC version 8.7.20181017 for x86_64unknownlinux):
Core Lint error
<no location info>: warning:
In the type ‘(··>)’
Found TcTyCon: ··>[tc]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/FamInst.hs:171:31 in ghc:FamInst
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
> :q
Leaving GHCi.
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.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":"Core Lint error","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This gives a Core Lint error\r\n\r\n{{{#!hs\r\n{# Language QuantifiedConstraints #}\r\n{# Language TypeApplications #}\r\n{# Language TypeOperators #}\r\n{# Language PolyKinds #}\r\n{# Language FlexibleInstances #}\r\n{# Language DataKinds #}\r\n{# Language TypeFamilies #}\r\n{# Language MultiParamTypeClasses #}\r\n{# Language ConstraintKinds #}\r\n{# Language UndecidableInstances #}\r\n{# Language GADTs #}\r\n\r\n{# Options_GHC dcorelint #}\r\n\r\nimport Data.Kind\r\n\r\ntype Cat ob = ob > ob > Type\r\n\r\nclass Ríki (obj :: Type) where\r\n type (>) :: Cat obj\r\n\r\nclass Varpi (f :: dom > cod)\r\n\r\nnewtype\r\n (··>) :: Cat (a > b) where\r\n Natu :: Varpi f\r\n => (forall xx. f xx > f' xx)\r\n > (f ··> f')\r\n\r\ninstance\r\n Ríki cod\r\n => \r\n Ríki (dom > cod)\r\n where\r\n\r\n type (>) = (··>) @dom @cod\r\n}}}\r\n\r\n{{{\r\n$ ghci ignoredotghci 568_bug.hs\r\nGHCi, version 8.7.20181017: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( 568_bug.hs, interpreted )\r\nghcstage2: panic! (the 'impossible' happened)\r\n (GHC version 8.7.20181017 for x86_64unknownlinux):\r\n Core Lint error\r\n <no location info>: warning:\r\n In the type ‘(··>)’\r\n Found TcTyCon: ··>[tc]\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/FamInst.hs:171:31 in ghc:FamInst\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n\r\n> :q\r\nLeaving GHCi.\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >This gives a Core Lint error
```hs
{# Language QuantifiedConstraints #}
{# Language TypeApplications #}
{# Language TypeOperators #}
{# Language PolyKinds #}
{# Language FlexibleInstances #}
{# Language DataKinds #}
{# Language TypeFamilies #}
{# Language MultiParamTypeClasses #}
{# Language ConstraintKinds #}
{# Language UndecidableInstances #}
{# Language GADTs #}
{# Options_GHC dcorelint #}
import Data.Kind
type Cat ob = ob > ob > Type
class Ríki (obj :: Type) where
type (>) :: Cat obj
class Varpi (f :: dom > cod)
newtype
(··>) :: Cat (a > b) where
Natu :: Varpi f
=> (forall xx. f xx > f' xx)
> (f ··> f')
instance
Ríki cod
=> 
Ríki (dom > cod)
where
type (>) = (··>) @dom @cod
```
```
$ ghci ignoredotghci 568_bug.hs
GHCi, version 8.7.20181017: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( 568_bug.hs, interpreted )
ghcstage2: panic! (the 'impossible' happened)
(GHC version 8.7.20181017 for x86_64unknownlinux):
Core Lint error
<no location info>: warning:
In the type ‘(··>)’
Found TcTyCon: ··>[tc]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/FamInst.hs:171:31 in ghc:FamInst
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
> :q
Leaving GHCi.
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.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":"Core Lint error","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This gives a Core Lint error\r\n\r\n{{{#!hs\r\n{# Language QuantifiedConstraints #}\r\n{# Language TypeApplications #}\r\n{# Language TypeOperators #}\r\n{# Language PolyKinds #}\r\n{# Language FlexibleInstances #}\r\n{# Language DataKinds #}\r\n{# Language TypeFamilies #}\r\n{# Language MultiParamTypeClasses #}\r\n{# Language ConstraintKinds #}\r\n{# Language UndecidableInstances #}\r\n{# Language GADTs #}\r\n\r\n{# Options_GHC dcorelint #}\r\n\r\nimport Data.Kind\r\n\r\ntype Cat ob = ob > ob > Type\r\n\r\nclass Ríki (obj :: Type) where\r\n type (>) :: Cat obj\r\n\r\nclass Varpi (f :: dom > cod)\r\n\r\nnewtype\r\n (··>) :: Cat (a > b) where\r\n Natu :: Varpi f\r\n => (forall xx. f xx > f' xx)\r\n > (f ··> f')\r\n\r\ninstance\r\n Ríki cod\r\n => \r\n Ríki (dom > cod)\r\n where\r\n\r\n type (>) = (··>) @dom @cod\r\n}}}\r\n\r\n{{{\r\n$ ghci ignoredotghci 568_bug.hs\r\nGHCi, version 8.7.20181017: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( 568_bug.hs, interpreted )\r\nghcstage2: panic! (the 'impossible' happened)\r\n (GHC version 8.7.20181017 for x86_64unknownlinux):\r\n Core Lint error\r\n <no location info>: warning:\r\n In the type ‘(··>)’\r\n Found TcTyCon: ··>[tc]\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/FamInst.hs:171:31 in ghc:FamInst\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n\r\n> :q\r\nLeaving GHCi.\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >8.6.2https://gitlab.haskell.org/ghc/ghc//issues/15772Strange constraint error that disappears when adding another toplevel declar...20201226T13:06:22ZAndres LöhStrange constraint error that disappears when adding another toplevel declarationConsider this program:
```hs
{# LANGUAGE DataKinds, TypeFamilies, TypeOperators, UndecidableInstances #}
module CURepro where
import Data.Kind
data NP (f :: Type > Type) (xs :: [Type])
type family Curry (f :: Type > Type) (xs :: [Type]) (r :: Type) (a :: Type) :: Constraint where
Curry f xs r (f x > a) = (xs ~ (x : Tail xs), Curry f (Tail xs) r a)
Curry f xs r a = (xs ~ '[], r ~ a)
type family Tail (a :: [Type]) :: [Type] where
Tail (_ : xs) = xs
uncurry_NP :: (Curry f xs r a) => (NP f xs > r) > a
uncurry_NP = undefined
fun_NP :: NP Id xs > ()
fun_NP = undefined
newtype Id a = MkId a
 test1 :: ()
 test1 = uncurry_NP fun_NP (MkId 5)
test2 :: ()
test2 = uncurry_NP fun_NP (MkId True) (MkId 5) (MkId True)
```
With GHC 8.6.1 (and also 8.4.3), this produces the following error message:
```
CURepro.hs:27:9: error:
• Couldn't match type ‘Tail t0’ with ‘Bool : Tail (Tail t0)’
arising from a use of ‘uncurry_NP’
The type variable ‘t0’ is ambiguous
• In the expression:
uncurry_NP fun_NP (MkId True) (MkId 5) (MkId True)
In an equation for ‘test2’:
test2 = uncurry_NP fun_NP (MkId True) (MkId 5) (MkId True)

27  test2 = uncurry_NP fun_NP (MkId True) (MkId 5) (MkId True)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
However, uncommenting the definition of `test1` makes the whole program check without error!
I think both versions of the program should be accepted.
I've tried to extract this from a much larger failing example, but did not manage to make it any smaller than this. In particular, the fact that `NP` is parameterised over a type constructor `f` seems to be somehow essential to trigger this.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Strange constraint error that disappears when adding another toplevel declaration","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider this program:\r\n{{{#!hs\r\n{# LANGUAGE DataKinds, TypeFamilies, TypeOperators, UndecidableInstances #}\r\nmodule CURepro where\r\n\r\nimport Data.Kind\r\n\r\ndata NP (f :: Type > Type) (xs :: [Type])\r\n\r\ntype family Curry (f :: Type > Type) (xs :: [Type]) (r :: Type) (a :: Type) :: Constraint where\r\n Curry f xs r (f x > a) = (xs ~ (x : Tail xs), Curry f (Tail xs) r a)\r\n Curry f xs r a = (xs ~ '[], r ~ a)\r\n\r\ntype family Tail (a :: [Type]) :: [Type] where\r\n Tail (_ : xs) = xs\r\n\r\nuncurry_NP :: (Curry f xs r a) => (NP f xs > r) > a\r\nuncurry_NP = undefined\r\n\r\nfun_NP :: NP Id xs > ()\r\nfun_NP = undefined\r\n\r\nnewtype Id a = MkId a\r\n\r\n test1 :: ()\r\n test1 = uncurry_NP fun_NP (MkId 5)\r\n\r\ntest2 :: ()\r\ntest2 = uncurry_NP fun_NP (MkId True) (MkId 5) (MkId True)\r\n}}}\r\n\r\nWith GHC 8.6.1 (and also 8.4.3), this produces the following error message:\r\n{{{\r\nCURepro.hs:27:9: error:\r\n • Couldn't match type ‘Tail t0’ with ‘Bool : Tail (Tail t0)’\r\n arising from a use of ‘uncurry_NP’\r\n The type variable ‘t0’ is ambiguous\r\n • In the expression:\r\n uncurry_NP fun_NP (MkId True) (MkId 5) (MkId True)\r\n In an equation for ‘test2’:\r\n test2 = uncurry_NP fun_NP (MkId True) (MkId 5) (MkId True)\r\n \r\n27  test2 = uncurry_NP fun_NP (MkId True) (MkId 5) (MkId True)\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nHowever, uncommenting the definition of `test1` makes the whole program check without error!\r\n\r\nI think both versions of the program should be accepted.\r\n\r\nI've tried to extract this from a much larger failing example, but did not manage to make it any smaller than this. In particular, the fact that `NP` is parameterised over a type constructor `f` seems to be somehow essential to trigger this.","type_of_failure":"OtherFailure","blocking":[]} >Consider this program:
```hs
{# LANGUAGE DataKinds, TypeFamilies, TypeOperators, UndecidableInstances #}
module CURepro where
import Data.Kind
data NP (f :: Type > Type) (xs :: [Type])
type family Curry (f :: Type > Type) (xs :: [Type]) (r :: Type) (a :: Type) :: Constraint where
Curry f xs r (f x > a) = (xs ~ (x : Tail xs), Curry f (Tail xs) r a)
Curry f xs r a = (xs ~ '[], r ~ a)
type family Tail (a :: [Type]) :: [Type] where
Tail (_ : xs) = xs
uncurry_NP :: (Curry f xs r a) => (NP f xs > r) > a
uncurry_NP = undefined
fun_NP :: NP Id xs > ()
fun_NP = undefined
newtype Id a = MkId a
 test1 :: ()
 test1 = uncurry_NP fun_NP (MkId 5)
test2 :: ()
test2 = uncurry_NP fun_NP (MkId True) (MkId 5) (MkId True)
```
With GHC 8.6.1 (and also 8.4.3), this produces the following error message:
```
CURepro.hs:27:9: error:
• Couldn't match type ‘Tail t0’ with ‘Bool : Tail (Tail t0)’
arising from a use of ‘uncurry_NP’
The type variable ‘t0’ is ambiguous
• In the expression:
uncurry_NP fun_NP (MkId True) (MkId 5) (MkId True)
In an equation for ‘test2’:
test2 = uncurry_NP fun_NP (MkId True) (MkId 5) (MkId True)

27  test2 = uncurry_NP fun_NP (MkId True) (MkId 5) (MkId True)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
However, uncommenting the definition of `test1` makes the whole program check without error!
I think both versions of the program should be accepted.
I've tried to extract this from a much larger failing example, but did not manage to make it any smaller than this. In particular, the fact that `NP` is parameterised over a type constructor `f` seems to be somehow essential to trigger this.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Strange constraint error that disappears when adding another toplevel declaration","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider this program:\r\n{{{#!hs\r\n{# LANGUAGE DataKinds, TypeFamilies, TypeOperators, UndecidableInstances #}\r\nmodule CURepro where\r\n\r\nimport Data.Kind\r\n\r\ndata NP (f :: Type > Type) (xs :: [Type])\r\n\r\ntype family Curry (f :: Type > Type) (xs :: [Type]) (r :: Type) (a :: Type) :: Constraint where\r\n Curry f xs r (f x > a) = (xs ~ (x : Tail xs), Curry f (Tail xs) r a)\r\n Curry f xs r a = (xs ~ '[], r ~ a)\r\n\r\ntype family Tail (a :: [Type]) :: [Type] where\r\n Tail (_ : xs) = xs\r\n\r\nuncurry_NP :: (Curry f xs r a) => (NP f xs > r) > a\r\nuncurry_NP = undefined\r\n\r\nfun_NP :: NP Id xs > ()\r\nfun_NP = undefined\r\n\r\nnewtype Id a = MkId a\r\n\r\n test1 :: ()\r\n test1 = uncurry_NP fun_NP (MkId 5)\r\n\r\ntest2 :: ()\r\ntest2 = uncurry_NP fun_NP (MkId True) (MkId 5) (MkId True)\r\n}}}\r\n\r\nWith GHC 8.6.1 (and also 8.4.3), this produces the following error message:\r\n{{{\r\nCURepro.hs:27:9: error:\r\n • Couldn't match type ‘Tail t0’ with ‘Bool : Tail (Tail t0)’\r\n arising from a use of ‘uncurry_NP’\r\n The type variable ‘t0’ is ambiguous\r\n • In the expression:\r\n uncurry_NP fun_NP (MkId True) (MkId 5) (MkId True)\r\n In an equation for ‘test2’:\r\n test2 = uncurry_NP fun_NP (MkId True) (MkId 5) (MkId True)\r\n \r\n27  test2 = uncurry_NP fun_NP (MkId True) (MkId 5) (MkId True)\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nHowever, uncommenting the definition of `test1` makes the whole program check without error!\r\n\r\nI think both versions of the program should be accepted.\r\n\r\nI've tried to extract this from a much larger failing example, but did not manage to make it any smaller than this. In particular, the fact that `NP` is parameterised over a type constructor `f` seems to be somehow essential to trigger this.","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/15708Crossmodule SPECIALZE pragmas aren't typechecked in O020190707T18:03:21ZregnatCrossmodule SPECIALZE pragmas aren't typechecked in O0If a module defines a `SPECIALIZE` pragma for a value defined in another module, then the signature of this pragma won't be typecheck by `ghc O0` (but it will be if the `SPECIALIZE` pragma is in the same module as the value).
For example, given
```hs
 Foo.hs
module Foo where
foo :: a > a
foo = id

 Bar.hs
module Bar where
import Foo
{# SPECIALIZE foo :: Int > Bool #}
```
running `ghc make Bar.hs` will run fine, while `ghc make O2 Bar.hs` will complain:
```
Bar.hs:5:1: error:
• Couldn't match type ‘Bool’ with ‘Int’
Expected type: Int > Int
Actual type: Int > Bool
• In the SPECIALISE pragma {# SPECIALIZE foo :: Int > Bool #}

5  {# SPECIALIZE foo :: Int > Bool #}
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
Tested on ghc 8.6.1 and 8.4.3
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.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":"Crossmodule SPECIALZE pragmas aren't typechecked in O0","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"If a module defines a `SPECIALIZE` pragma for a value defined in another module, then the signature of this pragma won't be typecheck by `ghc O0` (but it will be if the `SPECIALIZE` pragma is in the same module as the value).\r\n\r\nFor example, given\r\n\r\n{{{#!hs\r\n Foo.hs\r\nmodule Foo where\r\n\r\nfoo :: a > a\r\nfoo = id\r\n\r\n\r\n\r\n Bar.hs\r\nmodule Bar where\r\n\r\nimport Foo\r\n\r\n{# SPECIALIZE foo :: Int > Bool #}\r\n}}}\r\n\r\nrunning `ghc make Bar.hs` will run fine, while `ghc make O2 Bar.hs` will complain:\r\n\r\n{{{\r\nBar.hs:5:1: error:\r\n • Couldn't match type ‘Bool’ with ‘Int’\r\n Expected type: Int > Int\r\n Actual type: Int > Bool\r\n • In the SPECIALISE pragma {# SPECIALIZE foo :: Int > Bool #}\r\n \r\n5  {# SPECIALIZE foo :: Int > Bool #}\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nTested on ghc 8.6.1 and 8.4.3","type_of_failure":"OtherFailure","blocking":[]} >If a module defines a `SPECIALIZE` pragma for a value defined in another module, then the signature of this pragma won't be typecheck by `ghc O0` (but it will be if the `SPECIALIZE` pragma is in the same module as the value).
For example, given
```hs
 Foo.hs
module Foo where
foo :: a > a
foo = id

 Bar.hs
module Bar where
import Foo
{# SPECIALIZE foo :: Int > Bool #}
```
running `ghc make Bar.hs` will run fine, while `ghc make O2 Bar.hs` will complain:
```
Bar.hs:5:1: error:
• Couldn't match type ‘Bool’ with ‘Int’
Expected type: Int > Int
Actual type: Int > Bool
• In the SPECIALISE pragma {# SPECIALIZE foo :: Int > Bool #}

5  {# SPECIALIZE foo :: Int > Bool #}
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
Tested on ghc 8.6.1 and 8.4.3
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.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":"Crossmodule SPECIALZE pragmas aren't typechecked in O0","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"If a module defines a `SPECIALIZE` pragma for a value defined in another module, then the signature of this pragma won't be typecheck by `ghc O0` (but it will be if the `SPECIALIZE` pragma is in the same module as the value).\r\n\r\nFor example, given\r\n\r\n{{{#!hs\r\n Foo.hs\r\nmodule Foo where\r\n\r\nfoo :: a > a\r\nfoo = id\r\n\r\n\r\n\r\n Bar.hs\r\nmodule Bar where\r\n\r\nimport Foo\r\n\r\n{# SPECIALIZE foo :: Int > Bool #}\r\n}}}\r\n\r\nrunning `ghc make Bar.hs` will run fine, while `ghc make O2 Bar.hs` will complain:\r\n\r\n{{{\r\nBar.hs:5:1: error:\r\n • Couldn't match type ‘Bool’ with ‘Int’\r\n Expected type: Int > Int\r\n Actual type: Int > Bool\r\n • In the SPECIALISE pragma {# SPECIALIZE foo :: Int > Bool #}\r\n \r\n5  {# SPECIALIZE foo :: Int > Bool #}\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nTested on ghc 8.6.1 and 8.4.3","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/15704Different saturations of the same polymorphickinded type constructor aren't ...20190707T18:03:22ZmniipDifferent saturations of the same polymorphickinded type constructor aren't seen as apart types```hs
{# LANGUAGE TypeFamilies, PolyKinds #}
module A where
data family D :: k
type family F (a :: k) :: *
type instance F (D Int) = Int
type instance F (f a b) = Char
type instance F (D Int Bool) = Char
```
The last equation, even though a specialization of the middle one, trips up the equality consistency check:
```hs
a.hs:9:15: error:
Conflicting family instance declarations:
F (D Int) = Int  Defined at a.hs:9:15
F (D Int Bool) = Char  Defined at a.hs:10:15

9  type instance F (D Int) = Int
 ^
```
So GHC is able to infer that `D Int ~/~ f a b` because `D ~/~ f a`, but for some reason the same reasoning doesn't work for `D ~/~ D a`.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.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":"Different saturations of the same polymorphickinded type constructor aren't seen as apart types","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1","keywords":["TypeFamilies"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{# LANGUAGE TypeFamilies, PolyKinds #}\r\n\r\nmodule A where\r\n\r\ndata family D :: k\r\n\r\ntype family F (a :: k) :: *\r\n\r\ntype instance F (D Int) = Int\r\ntype instance F (f a b) = Char\r\ntype instance F (D Int Bool) = Char\r\n}}}\r\n\r\nThe last equation, even though a specialization of the middle one, trips up the equality consistency check:\r\n{{{#!hs\r\na.hs:9:15: error:\r\n Conflicting family instance declarations:\r\n F (D Int) = Int  Defined at a.hs:9:15\r\n F (D Int Bool) = Char  Defined at a.hs:10:15\r\n \r\n9  type instance F (D Int) = Int\r\n  ^\r\n}}}\r\n\r\nSo GHC is able to infer that `D Int ~/~ f a b` because `D ~/~ f a`, but for some reason the same reasoning doesn't work for `D ~/~ D a`.","type_of_failure":"OtherFailure","blocking":[]} >```hs
{# LANGUAGE TypeFamilies, PolyKinds #}
module A where
data family D :: k
type family F (a :: k) :: *
type instance F (D Int) = Int
type instance F (f a b) = Char
type instance F (D Int Bool) = Char
```
The last equation, even though a specialization of the middle one, trips up the equality consistency check:
```hs
a.hs:9:15: error:
Conflicting family instance declarations:
F (D Int) = Int  Defined at a.hs:9:15
F (D Int Bool) = Char  Defined at a.hs:10:15

9  type instance F (D Int) = Int
 ^
```
So GHC is able to infer that `D Int ~/~ f a b` because `D ~/~ f a`, but for some reason the same reasoning doesn't work for `D ~/~ D a`.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.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":"Different saturations of the same polymorphickinded type constructor aren't seen as apart types","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1","keywords":["TypeFamilies"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{# LANGUAGE TypeFamilies, PolyKinds #}\r\n\r\nmodule A where\r\n\r\ndata family D :: k\r\n\r\ntype family F (a :: k) :: *\r\n\r\ntype instance F (D Int) = Int\r\ntype instance F (f a b) = Char\r\ntype instance F (D Int Bool) = Char\r\n}}}\r\n\r\nThe last equation, even though a specialization of the middle one, trips up the equality consistency check:\r\n{{{#!hs\r\na.hs:9:15: error:\r\n Conflicting family instance declarations:\r\n F (D Int) = Int  Defined at a.hs:9:15\r\n F (D Int Bool) = Char  Defined at a.hs:10:15\r\n \r\n9  type instance F (D Int) = Int\r\n  ^\r\n}}}\r\n\r\nSo GHC is able to infer that `D Int ~/~ f a b` because `D ~/~ f a`, but for some reason the same reasoning doesn't work for `D ~/~ D a`.","type_of_failure":"OtherFailure","blocking":[]} >8.6.1mniipmniiphttps://gitlab.haskell.org/ghc/ghc//issues/15691Marking Pred(S n) = n as injective20190707T18:03:26ZIcelandjackMarking Pred(S n) = n as injectiveShould `Pred` be injective? Please close the ticket if this is a known limitation
```hs
{# Language DataKinds, TypeFamilyDependencies #}
data N = O  S N
type family
Pred n = res  res > n where
Pred(S n) = n
```
fails with
```
• Type family equation violates injectivity annotation.
RHS of injective type family equation is a bare type variable
but these LHS type and kind patterns are not bare variables: ‘'S n’
Pred ('S n) = n  Defined at 462.hs:7:2
• In the equations for closed type family ‘Pred’
In the type family declaration for ‘Pred’

7  Pred(S n) = n
 ^^^^^^^^^^^^^
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.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":"Marking Pred(S n) = n as injective","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1","keywords":["InjectiveFamilies","TypeFamilies,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Should `Pred` be injective? Please close the ticket if this is a known limitation \r\n\r\n{{{#!hs\r\n{# Language DataKinds, TypeFamilyDependencies #}\r\n\r\ndata N = O  S N\r\n\r\ntype family\r\n Pred n = res  res > n where\r\n Pred(S n) = n\r\n}}}\r\n\r\nfails with\r\n\r\n{{{\r\n • Type family equation violates injectivity annotation.\r\n RHS of injective type family equation is a bare type variable\r\n but these LHS type and kind patterns are not bare variables: ‘'S n’\r\n Pred ('S n) = n  Defined at 462.hs:7:2\r\n • In the equations for closed type family ‘Pred’\r\n In the type family declaration for ‘Pred’\r\n \r\n7  Pred(S n) = n\r\n  ^^^^^^^^^^^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >Should `Pred` be injective? Please close the ticket if this is a known limitation
```hs
{# Language DataKinds, TypeFamilyDependencies #}
data N = O  S N
type family
Pred n = res  res > n where
Pred(S n) = n
```
fails with
```
• Type family equation violates injectivity annotation.
RHS of injective type family equation is a bare type variable
but these LHS type and kind patterns are not bare variables: ‘'S n’
Pred ('S n) = n  Defined at 462.hs:7:2
• In the equations for closed type family ‘Pred’
In the type family declaration for ‘Pred’

7  Pred(S n) = n
 ^^^^^^^^^^^^^
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.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":"Marking Pred(S n) = n as injective","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1","keywords":["InjectiveFamilies","TypeFamilies,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Should `Pred` be injective? Please close the ticket if this is a known limitation \r\n\r\n{{{#!hs\r\n{# Language DataKinds, TypeFamilyDependencies #}\r\n\r\ndata N = O  S N\r\n\r\ntype family\r\n Pred n = res  res > n where\r\n Pred(S n) = n\r\n}}}\r\n\r\nfails with\r\n\r\n{{{\r\n • Type family equation violates injectivity annotation.\r\n RHS of injective type family equation is a bare type variable\r\n but these LHS type and kind patterns are not bare variables: ‘'S n’\r\n Pred ('S n) = n  Defined at 462.hs:7:2\r\n • In the equations for closed type family ‘Pred’\r\n In the type family declaration for ‘Pred’\r\n \r\n7  Pred(S n) = n\r\n  ^^^^^^^^^^^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >8.6.1https://gitlab.haskell.org/ghc/ghc//issues/15678Provide the provenance of unification variables in error messages when possible20210125T16:36:44ZRyan ScottProvide the provenance of unification variables in error messages when possibleConsider the following code:
```hs
module Foo where
x :: Int
x = const 42 _
```
When compiles, this gives the following suggestion:
```
$ /opt/ghc/8.6.1/bin/ghc Bug.hs
[1 of 1] Compiling Foo ( Bug.hs, Bug.o )
Bug.hs:4:14: error:
• Found hole: _ :: b0
Where: ‘b0’ is an ambiguous type variable
• In the second argument of ‘const’, namely ‘_’
In the expression: const 42 _
In an equation for ‘x’: x = const 42 _
• Relevant bindings include x :: Int (bound at Bug.hs:4:1)
Valid hole fits include
x :: Int (bound at Bug.hs:4:1)
otherwise :: Bool
(imported from ‘Prelude’ at Bug.hs:1:810
(and originally defined in ‘GHC.Base’))
False :: Bool
(imported from ‘Prelude’ at Bug.hs:1:810
(and originally defined in ‘GHC.Types’))
True :: Bool
(imported from ‘Prelude’ at Bug.hs:1:810
(and originally defined in ‘GHC.Types’))
lines :: String > [String]
(imported from ‘Prelude’ at Bug.hs:1:810
(and originally defined in ‘base4.12.0.0:Data.OldList’))
unlines :: [String] > String
(imported from ‘Prelude’ at Bug.hs:1:810
(and originally defined in ‘base4.12.0.0:Data.OldList’))
(Some hole fits suppressed; use fmaxvalidholefits=N or fnomaxvalidholefits)

4  x = const 42 _
 ^
```
One thing that's rather ugly about this is the use of the type `b0`. What exactly //is// `b0` anyway? The only hint that the error message gives is that it's an ambiguous type variable. But that's not terribly helpful to figure out where `b0` arises from. Ambiguous type variables like this one arise quite frequently when writing Haskell code, and it can often take some sleuthing to figure out why they pop up.
simonpj had one suggestion for making ambiguous type variables less confusing: report their provenance whenever possible. There is one notable example of a situation where it's simple to explain from where exactly in the source code a unification variable originates: function applications. In particular, the program above applies the function `const 42` to `_`, which means that the type of `const 42` is instantiated to be `b0 > Int`. Let's report this! Something like:
```
• Found hole: _ :: b0
Where: ‘b0’ is an ambiguous type variable
Arising from an application of
(const 42 :: b0 > Int)
In the expression: const 42 _
```
This would go a long way to clearing up what GHC is thinking when it reports these ambiguous type variable errors. While we can't easily report the provenance of //every// ambiguous type variables, those arising from function applications are quite doable. We might be able to reuse the `CtOrigin` machinery (or take heavy inspiration from it) to accomplish this feat.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  Tritlo 
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Provide the provenance of unification variables in error messages when possible","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.8.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1","keywords":["TypeErrors"],"differentials":[],"test_case":"","architecture":"","cc":["Tritlo"],"type":"Bug","description":"Consider the following code:\r\n\r\n{{{#!hs\r\nmodule Foo where\r\n\r\nx :: Int\r\nx = const 42 _\r\n}}}\r\n\r\nWhen compiles, this gives the following suggestion:\r\n\r\n{{{\r\n$ /opt/ghc/8.6.1/bin/ghc Bug.hs\r\n[1 of 1] Compiling Foo ( Bug.hs, Bug.o )\r\n\r\nBug.hs:4:14: error:\r\n • Found hole: _ :: b0\r\n Where: ‘b0’ is an ambiguous type variable\r\n • In the second argument of ‘const’, namely ‘_’\r\n In the expression: const 42 _\r\n In an equation for ‘x’: x = const 42 _\r\n • Relevant bindings include x :: Int (bound at Bug.hs:4:1)\r\n Valid hole fits include\r\n x :: Int (bound at Bug.hs:4:1)\r\n otherwise :: Bool\r\n (imported from ‘Prelude’ at Bug.hs:1:810\r\n (and originally defined in ‘GHC.Base’))\r\n False :: Bool\r\n (imported from ‘Prelude’ at Bug.hs:1:810\r\n (and originally defined in ‘GHC.Types’))\r\n True :: Bool\r\n (imported from ‘Prelude’ at Bug.hs:1:810\r\n (and originally defined in ‘GHC.Types’))\r\n lines :: String > [String]\r\n (imported from ‘Prelude’ at Bug.hs:1:810\r\n (and originally defined in ‘base4.12.0.0:Data.OldList’))\r\n unlines :: [String] > String\r\n (imported from ‘Prelude’ at Bug.hs:1:810\r\n (and originally defined in ‘base4.12.0.0:Data.OldList’))\r\n (Some hole fits suppressed; use fmaxvalidholefits=N or fnomaxvalidholefits)\r\n \r\n4  x = const 42 _\r\n  ^\r\n}}}\r\n\r\nOne thing that's rather ugly about this is the use of the type `b0`. What exactly //is// `b0` anyway? The only hint that the error message gives is that it's an ambiguous type variable. But that's not terribly helpful to figure out where `b0` arises from. Ambiguous type variables like this one arise quite frequently when writing Haskell code, and it can often take some sleuthing to figure out why they pop up.\r\n\r\nsimonpj had one suggestion for making ambiguous type variables less confusing: report their provenance whenever possible. There is one notable example of a situation where it's simple to explain from where exactly in the source code a unification variable originates: function applications. In particular, the program above applies the function `const 42` to `_`, which means that the type of `const 42` is instantiated to be `b0 > Int`. Let's report this! Something like:\r\n\r\n{{{\r\n • Found hole: _ :: b0\r\n Where: ‘b0’ is an ambiguous type variable\r\n Arising from an application of\r\n (const 42 :: b0 > Int)\r\n In the expression: const 42 _\r\n}}}\r\n\r\nThis would go a long way to clearing up what GHC is thinking when it reports these ambiguous type variable errors. While we can't easily report the provenance of //every// ambiguous type variables, those arising from function applications are quite doable. We might be able to reuse the `CtOrigin` machinery (or take heavy inspiration from it) to accomplish this feat.","type_of_failure":"OtherFailure","blocking":[]} >Consider the following code:
```hs
module Foo where
x :: Int
x = const 42 _
```
When compiles, this gives the following suggestion:
```
$ /opt/ghc/8.6.1/bin/ghc Bug.hs
[1 of 1] Compiling Foo ( Bug.hs, Bug.o )
Bug.hs:4:14: error:
• Found hole: _ :: b0
Where: ‘b0’ is an ambiguous type variable
• In the second argument of ‘const’, namely ‘_’
In the expression: const 42 _
In an equation for ‘x’: x = const 42 _
• Relevant bindings include x :: Int (bound at Bug.hs:4:1)
Valid hole fits include
x :: Int (bound at Bug.hs:4:1)
otherwise :: Bool
(imported from ‘Prelude’ at Bug.hs:1:810
(and originally defined in ‘GHC.Base’))
False :: Bool
(imported from ‘Prelude’ at Bug.hs:1:810
(and originally defined in ‘GHC.Types’))
True :: Bool
(imported from ‘Prelude’ at Bug.hs:1:810
(and originally defined in ‘GHC.Types’))
lines :: String > [String]
(imported from ‘Prelude’ at Bug.hs:1:810
(and originally defined in ‘base4.12.0.0:Data.OldList’))
unlines :: [String] > String
(imported from ‘Prelude’ at Bug.hs:1:810
(and originally defined in ‘base4.12.0.0:Data.OldList’))
(Some hole fits suppressed; use fmaxvalidholefits=N or fnomaxvalidholefits)

4  x = const 42 _
 ^
```
One thing that's rather ugly about this is the use of the type `b0`. What exactly //is// `b0` anyway? The only hint that the error message gives is that it's an ambiguous type variable. But that's not terribly helpful to figure out where `b0` arises from. Ambiguous type variables like this one arise quite frequently when writing Haskell code, and it can often take some sleuthing to figure out why they pop up.
simonpj had one suggestion for making ambiguous type variables less confusing: report their provenance whenever possible. There is one notable example of a situation where it's simple to explain from where exactly in the source code a unification variable originates: function applications. In particular, the program above applies the function `const 42` to `_`, which means that the type of `const 42` is instantiated to be `b0 > Int`. Let's report this! Something like:
```
• Found hole: _ :: b0
Where: ‘b0’ is an ambiguous type variable
Arising from an application of
(const 42 :: b0 > Int)
In the expression: const 42 _
```
This would go a long way to clearing up what GHC is thinking when it reports these ambiguous type variable errors. While we can't easily report the provenance of //every// ambiguous type variables, those arising from function applications are quite doable. We might be able to reuse the `CtOrigin` machinery (or take heavy inspiration from it) to accomplish this feat.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  Tritlo 
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Provide the provenance of unification variables in error messages when possible","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.8.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1","keywords":["TypeErrors"],"differentials":[],"test_case":"","architecture":"","cc":["Tritlo"],"type":"Bug","description":"Consider the following code:\r\n\r\n{{{#!hs\r\nmodule Foo where\r\n\r\nx :: Int\r\nx = const 42 _\r\n}}}\r\n\r\nWhen compiles, this gives the following suggestion:\r\n\r\n{{{\r\n$ /opt/ghc/8.6.1/bin/ghc Bug.hs\r\n[1 of 1] Compiling Foo ( Bug.hs, Bug.o )\r\n\r\nBug.hs:4:14: error:\r\n • Found hole: _ :: b0\r\n Where: ‘b0’ is an ambiguous type variable\r\n • In the second argument of ‘const’, namely ‘_’\r\n In the expression: const 42 _\r\n In an equation for ‘x’: x = const 42 _\r\n • Relevant bindings include x :: Int (bound at Bug.hs:4:1)\r\n Valid hole fits include\r\n x :: Int (bound at Bug.hs:4:1)\r\n otherwise :: Bool\r\n (imported from ‘Prelude’ at Bug.hs:1:810\r\n (and originally defined in ‘GHC.Base’))\r\n False :: Bool\r\n (imported from ‘Prelude’ at Bug.hs:1:810\r\n (and originally defined in ‘GHC.Types’))\r\n True :: Bool\r\n (imported from ‘Prelude’ at Bug.hs:1:810\r\n (and originally defined in ‘GHC.Types’))\r\n lines :: String > [String]\r\n (imported from ‘Prelude’ at Bug.hs:1:810\r\n (and originally defined in ‘base4.12.0.0:Data.OldList’))\r\n unlines :: [String] > String\r\n (imported from ‘Prelude’ at Bug.hs:1:810\r\n (and originally defined in ‘base4.12.0.0:Data.OldList’))\r\n (Some hole fits suppressed; use fmaxvalidholefits=N or fnomaxvalidholefits)\r\n \r\n4  x = const 42 _\r\n  ^\r\n}}}\r\n\r\nOne thing that's rather ugly about this is the use of the type `b0`. What exactly //is// `b0` anyway? The only hint that the error message gives is that it's an ambiguous type variable. But that's not terribly helpful to figure out where `b0` arises from. Ambiguous type variables like this one arise quite frequently when writing Haskell code, and it can often take some sleuthing to figure out why they pop up.\r\n\r\nsimonpj had one suggestion for making ambiguous type variables less confusing: report their provenance whenever possible. There is one notable example of a situation where it's simple to explain from where exactly in the source code a unification variable originates: function applications. In particular, the program above applies the function `const 42` to `_`, which means that the type of `const 42` is instantiated to be `b0 > Int`. Let's report this! Something like:\r\n\r\n{{{\r\n • Found hole: _ :: b0\r\n Where: ‘b0’ is an ambiguous type variable\r\n Arising from an application of\r\n (const 42 :: b0 > Int)\r\n In the expression: const 42 _\r\n}}}\r\n\r\nThis would go a long way to clearing up what GHC is thinking when it reports these ambiguous type variable errors. While we can't easily report the provenance of //every// ambiguous type variables, those arising from function applications are quite doable. We might be able to reuse the `CtOrigin` machinery (or take heavy inspiration from it) to accomplish this feat.","type_of_failure":"OtherFailure","blocking":[]} >9.2.1Matthías Páll GissurarsonMatthías Páll Gissurarsonhttps://gitlab.haskell.org/ghc/ghc//issues/15639Surprising failure combining QuantifiedConstraints with Coercible20190707T18:03:38ZDavid FeuerSurprising failure combining QuantifiedConstraints with CoercibleI don't understand what's going wrong here.
```hs
 Fishy.hs
{# language RankNTypes, QuantifiedConstraints, RoleAnnotations #}
module Fishy (Yeah, yeahCoercible) where
import Data.Coerce
data Yeah_ a = Yeah_ Int
newtype Yeah a = Yeah (Yeah_ a)
type role Yeah representational
yeahCoercible :: ((forall a b. Coercible (Yeah a) (Yeah b)) => r) > r
yeahCoercible r = r
 Fishy2.hs
module Fishy2 where
import Fishy
import Data.Type.Coercion
import Data.Coerce
yeah :: Coercion [Yeah a] [Yeah b]
yeah = yeahCoercible Coercion
```
I get
```
Fishy2.hs:8:22: error:
• Couldn't match representation of type ‘a’ with that of ‘b’
arising from a use of ‘Coercion’
‘a’ is a rigid type variable bound by
the type signature for:
yeah :: forall a b. Coercion [Yeah a] [Yeah b]
at Fishy2.hs:7:134
‘b’ is a rigid type variable bound by
the type signature for:
yeah :: forall a b. Coercion [Yeah a] [Yeah b]
at Fishy2.hs:7:134
• In the first argument of ‘yeahCoercible’, namely ‘Coercion’
In the expression: yeahCoercible Coercion
In an equation for ‘yeah’: yeah = yeahCoercible Coercion
• Relevant bindings include
yeah :: Coercion [Yeah a] [Yeah b] (bound at Fishy2.hs:8:1)

8  yeah = yeahCoercible Coercion

```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 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":"Surprising failure combining QuantifiedConstraints with Coercible","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I don't understand what's going wrong here.\r\n\r\n{{{#!hs\r\n Fishy.hs\r\n{# language RankNTypes, QuantifiedConstraints, RoleAnnotations #}\r\nmodule Fishy (Yeah, yeahCoercible) where\r\nimport Data.Coerce\r\n\r\ndata Yeah_ a = Yeah_ Int\r\nnewtype Yeah a = Yeah (Yeah_ a)\r\ntype role Yeah representational\r\n\r\nyeahCoercible :: ((forall a b. Coercible (Yeah a) (Yeah b)) => r) > r\r\nyeahCoercible r = r\r\n\r\n\r\n Fishy2.hs\r\n\r\nmodule Fishy2 where\r\n\r\nimport Fishy\r\nimport Data.Type.Coercion\r\nimport Data.Coerce\r\n\r\nyeah :: Coercion [Yeah a] [Yeah b]\r\nyeah = yeahCoercible Coercion\r\n}}}\r\n\r\nI get\r\n\r\n{{{\r\nFishy2.hs:8:22: error:\r\n • Couldn't match representation of type ‘a’ with that of ‘b’\r\n arising from a use of ‘Coercion’\r\n ‘a’ is a rigid type variable bound by\r\n the type signature for:\r\n yeah :: forall a b. Coercion [Yeah a] [Yeah b]\r\n at Fishy2.hs:7:134\r\n ‘b’ is a rigid type variable bound by\r\n the type signature for:\r\n yeah :: forall a b. Coercion [Yeah a] [Yeah b]\r\n at Fishy2.hs:7:134\r\n • In the first argument of ‘yeahCoercible’, namely ‘Coercion’\r\n In the expression: yeahCoercible Coercion\r\n In an equation for ‘yeah’: yeah = yeahCoercible Coercion\r\n • Relevant bindings include\r\n yeah :: Coercion [Yeah a] [Yeah b] (bound at Fishy2.hs:8:1)\r\n \r\n8  yeah = yeahCoercible Coercion\r\n \r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >I don't understand what's going wrong here.
```hs
 Fishy.hs
{# language RankNTypes, QuantifiedConstraints, RoleAnnotations #}
module Fishy (Yeah, yeahCoercible) where
import Data.Coerce
data Yeah_ a = Yeah_ Int
newtype Yeah a = Yeah (Yeah_ a)
type role Yeah representational
yeahCoercible :: ((forall a b. Coercible (Yeah a) (Yeah b)) => r) > r
yeahCoercible r = r
 Fishy2.hs
module Fishy2 where
import Fishy
import Data.Type.Coercion
import Data.Coerce
yeah :: Coercion [Yeah a] [Yeah b]
yeah = yeahCoercible Coercion
```
I get
```
Fishy2.hs:8:22: error:
• Couldn't match representation of type ‘a’ with that of ‘b’
arising from a use of ‘Coercion’
‘a’ is a rigid type variable bound by
the type signature for:
yeah :: forall a b. Coercion [Yeah a] [Yeah b]
at Fishy2.hs:7:134
‘b’ is a rigid type variable bound by
the type signature for:
yeah :: forall a b. Coercion [Yeah a] [Yeah b]
at Fishy2.hs:7:134
• In the first argument of ‘yeahCoercible’, namely ‘Coercion’
In the expression: yeahCoercible Coercion
In an equation for ‘yeah’: yeah = yeahCoercible Coercion
• Relevant bindings include
yeah :: Coercion [Yeah a] [Yeah b] (bound at Fishy2.hs:8:1)

8  yeah = yeahCoercible Coercion

```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 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":"Surprising failure combining QuantifiedConstraints with Coercible","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I don't understand what's going wrong here.\r\n\r\n{{{#!hs\r\n Fishy.hs\r\n{# language RankNTypes, QuantifiedConstraints, RoleAnnotations #}\r\nmodule Fishy (Yeah, yeahCoercible) where\r\nimport Data.Coerce\r\n\r\ndata Yeah_ a = Yeah_ Int\r\nnewtype Yeah a = Yeah (Yeah_ a)\r\ntype role Yeah representational\r\n\r\nyeahCoercible :: ((forall a b. Coercible (Yeah a) (Yeah b)) => r) > r\r\nyeahCoercible r = r\r\n\r\n\r\n Fishy2.hs\r\n\r\nmodule Fishy2 where\r\n\r\nimport Fishy\r\nimport Data.Type.Coercion\r\nimport Data.Coerce\r\n\r\nyeah :: Coercion [Yeah a] [Yeah b]\r\nyeah = yeahCoercible Coercion\r\n}}}\r\n\r\nI get\r\n\r\n{{{\r\nFishy2.hs:8:22: error:\r\n • Couldn't match representation of type ‘a’ with that of ‘b’\r\n arising from a use of ‘Coercion’\r\n ‘a’ is a rigid type variable bound by\r\n the type signature for:\r\n yeah :: forall a b. Coercion [Yeah a] [Yeah b]\r\n at Fishy2.hs:7:134\r\n ‘b’ is a rigid type variable bound by\r\n the type signature for:\r\n yeah :: forall a b. Coercion [Yeah a] [Yeah b]\r\n at Fishy2.hs:7:134\r\n • In the first argument of ‘yeahCoercible’, namely ‘Coercion’\r\n In the expression: yeahCoercible Coercion\r\n In an equation for ‘yeah’: yeah = yeahCoercible Coercion\r\n • Relevant bindings include\r\n yeah :: Coercion [Yeah a] [Yeah b] (bound at Fishy2.hs:8:1)\r\n \r\n8  yeah = yeahCoercible Coercion\r\n \r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >8.6.1https://gitlab.haskell.org/ghc/ghc//issues/15629"No skolem info" panic (GHC 8.6 only)20190707T18:03:40ZRyan Scott"No skolem info" panic (GHC 8.6 only)The following program:
```hs
{# LANGUAGE RankNTypes #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
{# LANGUAGE UndecidableInstances #}
module Bug where
import Data.Kind
import Data.Proxy
import GHC.Generics
data TyFun :: Type > Type > Type
type a ~> b = TyFun a b > Type
infixr 0 ~>
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
data family Sing :: forall k. k > Type
newtype instance Sing (f :: k1 ~> k2) =
SLambda { applySing :: forall t. Sing t > Sing (Apply f t) }
singFun1 :: forall f. (forall t. Sing t > Sing (Apply f t)) > Sing f
singFun1 f = SLambda f
data From1Sym0 :: forall k (f :: k > Type) (a :: k). f a ~> Rep1 f a
data To1Sym0 :: forall k (f :: k > Type) (a :: k). Rep1 f a ~> f a
type family ((f :: b ~> c) :. (g :: a ~> b)) (x :: a) :: c where
(f :. g) x = Apply f (Apply g x)
data (.@#@$$$) :: forall b c a. (b ~> c) > (a ~> b) > (a ~> c)
type instance Apply (f .@#@$$$ g) x = (f :. g) x
(%.) :: forall a b c (f :: b ~> c) (g :: a ~> b) (x :: a).
Sing f > Sing g > Sing x > Sing ((f :. g) x)
(sf %. sg) sx = applySing sf (applySing sg sx)
(%.$$$) :: forall a b c (f :: b ~> c) (g :: a ~> b) (x :: a).
Sing f > Sing g > Sing (f .@#@$$$ g)
sf %.$$$ sg = singFun1 (sf %. sg)
f :: forall (m :: Type > Type) x. Proxy (m x) > ()
f _ = ()
where
sFrom1Fun :: forall ab. Sing (From1Sym0 :: m ab ~> Rep1 m ab)
sFrom1Fun = undefined
sTo1Fun :: forall ab. Sing (To1Sym0 :: Rep1 m ab ~> m ab)
sTo1Fun = undefined
sFrom1To1Fun :: forall ab. Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab ~> Rep1 m ab)
sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun
```
Panics on GHC 8.6:
```
$ /opt/ghc/8.6.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:50:39: error:
• Expected kind ‘m z ~> Rep1 m ab1’,
but ‘(From1Sym0 :: m z ~> Rep1 m z)’ has kind ‘m z ~> Rep1 m z’
• In the first argument of ‘(.@#@$$$)’, namely
‘(From1Sym0 :: m z ~> Rep1 m z)’
In the first argument of ‘Sing’, namely
‘(((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab
~> Rep1 m ab)’
In the type signature:
sFrom1To1Fun :: forall ab.
Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab
~> Rep1 m ab)

50  sFrom1To1Fun :: forall ab. Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab ~> Rep1 m ab)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Bug.hs:51:20: error:ghc: panic! (the 'impossible' happened)
(GHC version 8.6.0.20180823 for x86_64unknownlinux):
No skolem info:
[ab_a1UW[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
```
But merely errors on GHC 8.4.3:
```
$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:50:39: error:
• Expected kind ‘m z ~> Rep1 m ab2’,
but ‘(From1Sym0 :: m z ~> Rep1 m z)’ has kind ‘m z ~> Rep1 m z’
• In the first argument of ‘(.@#@$$$)’, namely
‘(From1Sym0 :: m z ~> Rep1 m z)’
In the first argument of ‘Sing’, namely
‘(((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab
~> Rep1 m ab)’
In the type signature:
sFrom1To1Fun :: forall ab.
Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab
~> Rep1 m ab)

50  sFrom1To1Fun :: forall ab. Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab ~> Rep1 m ab)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Bug.hs:51:20: error:
• Couldn't match type ‘ab1’ with ‘z1’
because type variable ‘z1’ would escape its scope
This (rigid, skolem) type variable is bound by
the type signature for:
sFrom1To1Fun :: forall z1 ab3. Sing (From1Sym0 .@#@$$$ To1Sym0)
at Bug.hs:50:5112
Expected type: Sing From1Sym0
Actual type: Sing From1Sym0
• In the first argument of ‘(%.$$$)’, namely ‘sFrom1Fun’
In the expression: sFrom1Fun %.$$$ sTo1Fun
In an equation for ‘sFrom1To1Fun’:
sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun
• Relevant bindings include
sFrom1To1Fun :: Sing (From1Sym0 .@#@$$$ To1Sym0)
(bound at Bug.hs:51:5)

51  sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun
 ^^^^^^^^^
Bug.hs:51:36: error:
• Couldn't match type ‘ab’ with ‘z1’
because type variable ‘z1’ would escape its scope
This (rigid, skolem) type variable is bound by
the type signature for:
sFrom1To1Fun :: forall z1 ab3. Sing (From1Sym0 .@#@$$$ To1Sym0)
at Bug.hs:50:5112
Expected type: Sing To1Sym0
Actual type: Sing To1Sym0
• In the second argument of ‘(%.$$$)’, namely ‘sTo1Fun’
In the expression: sFrom1Fun %.$$$ sTo1Fun
In an equation for ‘sFrom1To1Fun’:
sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun
• Relevant bindings include
sFrom1To1Fun :: Sing (From1Sym0 .@#@$$$ To1Sym0)
(bound at Bug.hs:51:5)

51  sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun
 ^^^^^^^
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.1beta1 
 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":"\"No skolem info\" panic (GHC 8.6 only)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1beta1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program:\r\n\r\n{{{#!hs\r\n{# LANGUAGE RankNTypes #}\r\n{# LANGUAGE ScopedTypeVariables #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeInType #}\r\n{# LANGUAGE TypeOperators #}\r\n{# LANGUAGE UndecidableInstances #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\nimport Data.Proxy\r\nimport GHC.Generics\r\n\r\ndata TyFun :: Type > Type > Type\r\ntype a ~> b = TyFun a b > Type\r\ninfixr 0 ~>\r\ntype family Apply (f :: k1 ~> k2) (x :: k1) :: k2\r\n\r\ndata family Sing :: forall k. k > Type\r\nnewtype instance Sing (f :: k1 ~> k2) =\r\n SLambda { applySing :: forall t. Sing t > Sing (Apply f t) }\r\nsingFun1 :: forall f. (forall t. Sing t > Sing (Apply f t)) > Sing f\r\nsingFun1 f = SLambda f\r\n\r\ndata From1Sym0 :: forall k (f :: k > Type) (a :: k). f a ~> Rep1 f a\r\ndata To1Sym0 :: forall k (f :: k > Type) (a :: k). Rep1 f a ~> f a\r\n\r\ntype family ((f :: b ~> c) :. (g :: a ~> b)) (x :: a) :: c where\r\n (f :. g) x = Apply f (Apply g x)\r\n\r\ndata (.@#@$$$) :: forall b c a. (b ~> c) > (a ~> b) > (a ~> c)\r\ntype instance Apply (f .@#@$$$ g) x = (f :. g) x\r\n\r\n(%.) :: forall a b c (f :: b ~> c) (g :: a ~> b) (x :: a).\r\n Sing f > Sing g > Sing x > Sing ((f :. g) x)\r\n(sf %. sg) sx = applySing sf (applySing sg sx)\r\n\r\n(%.$$$) :: forall a b c (f :: b ~> c) (g :: a ~> b) (x :: a).\r\n Sing f > Sing g > Sing (f .@#@$$$ g)\r\nsf %.$$$ sg = singFun1 (sf %. sg)\r\n\r\nf :: forall (m :: Type > Type) x. Proxy (m x) > ()\r\nf _ = ()\r\n where\r\n sFrom1Fun :: forall ab. Sing (From1Sym0 :: m ab ~> Rep1 m ab)\r\n sFrom1Fun = undefined\r\n\r\n sTo1Fun :: forall ab. Sing (To1Sym0 :: Rep1 m ab ~> m ab)\r\n sTo1Fun = undefined\r\n\r\n sFrom1To1Fun :: forall ab. Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab ~> Rep1 m ab)\r\n sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun\r\n}}}\r\n\r\nPanics on GHC 8.6:\r\n\r\n{{{\r\n$ /opt/ghc/8.6.1/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:50:39: error:\r\n • Expected kind ‘m z ~> Rep1 m ab1’,\r\n but ‘(From1Sym0 :: m z ~> Rep1 m z)’ has kind ‘m z ~> Rep1 m z’\r\n • In the first argument of ‘(.@#@$$$)’, namely\r\n ‘(From1Sym0 :: m z ~> Rep1 m z)’\r\n In the first argument of ‘Sing’, namely\r\n ‘(((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab\r\n ~> Rep1 m ab)’\r\n In the type signature:\r\n sFrom1To1Fun :: forall ab.\r\n Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab\r\n ~> Rep1 m ab)\r\n \r\n50  sFrom1To1Fun :: forall ab. Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab ~> Rep1 m ab)\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n\r\nBug.hs:51:20: error:ghc: panic! (the 'impossible' happened)\r\n (GHC version 8.6.0.20180823 for x86_64unknownlinux):\r\n No skolem info:\r\n [ab_a1UW[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\nBut merely errors on GHC 8.4.3:\r\n\r\n{{{\r\n$ /opt/ghc/8.4.3/bin/ghc Bug.hs \r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:50:39: error:\r\n • Expected kind ‘m z ~> Rep1 m ab2’,\r\n but ‘(From1Sym0 :: m z ~> Rep1 m z)’ has kind ‘m z ~> Rep1 m z’\r\n • In the first argument of ‘(.@#@$$$)’, namely\r\n ‘(From1Sym0 :: m z ~> Rep1 m z)’\r\n In the first argument of ‘Sing’, namely\r\n ‘(((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab\r\n ~> Rep1 m ab)’\r\n In the type signature:\r\n sFrom1To1Fun :: forall ab.\r\n Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab\r\n ~> Rep1 m ab)\r\n \r\n50  sFrom1To1Fun :: forall ab. Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab ~> Rep1 m ab)\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n\r\nBug.hs:51:20: error:\r\n • Couldn't match type ‘ab1’ with ‘z1’\r\n because type variable ‘z1’ would escape its scope\r\n This (rigid, skolem) type variable is bound by\r\n the type signature for:\r\n sFrom1To1Fun :: forall z1 ab3. Sing (From1Sym0 .@#@$$$ To1Sym0)\r\n at Bug.hs:50:5112\r\n Expected type: Sing From1Sym0\r\n Actual type: Sing From1Sym0\r\n • In the first argument of ‘(%.$$$)’, namely ‘sFrom1Fun’\r\n In the expression: sFrom1Fun %.$$$ sTo1Fun\r\n In an equation for ‘sFrom1To1Fun’:\r\n sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun\r\n • Relevant bindings include\r\n sFrom1To1Fun :: Sing (From1Sym0 .@#@$$$ To1Sym0)\r\n (bound at Bug.hs:51:5)\r\n \r\n51  sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun\r\n  ^^^^^^^^^\r\n\r\nBug.hs:51:36: error:\r\n • Couldn't match type ‘ab’ with ‘z1’\r\n because type variable ‘z1’ would escape its scope\r\n This (rigid, skolem) type variable is bound by\r\n the type signature for:\r\n sFrom1To1Fun :: forall z1 ab3. Sing (From1Sym0 .@#@$$$ To1Sym0)\r\n at Bug.hs:50:5112\r\n Expected type: Sing To1Sym0\r\n Actual type: Sing To1Sym0\r\n • In the second argument of ‘(%.$$$)’, namely ‘sTo1Fun’\r\n In the expression: sFrom1Fun %.$$$ sTo1Fun\r\n In an equation for ‘sFrom1To1Fun’:\r\n sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun\r\n • Relevant bindings include\r\n sFrom1To1Fun :: Sing (From1Sym0 .@#@$$$ To1Sym0)\r\n (bound at Bug.hs:51:5)\r\n \r\n51  sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun\r\n  ^^^^^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >The following program:
```hs
{# LANGUAGE RankNTypes #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
{# LANGUAGE UndecidableInstances #}
module Bug where
import Data.Kind
import Data.Proxy
import GHC.Generics
data TyFun :: Type > Type > Type
type a ~> b = TyFun a b > Type
infixr 0 ~>
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
data family Sing :: forall k. k > Type
newtype instance Sing (f :: k1 ~> k2) =
SLambda { applySing :: forall t. Sing t > Sing (Apply f t) }
singFun1 :: forall f. (forall t. Sing t > Sing (Apply f t)) > Sing f
singFun1 f = SLambda f
data From1Sym0 :: forall k (f :: k > Type) (a :: k). f a ~> Rep1 f a
data To1Sym0 :: forall k (f :: k > Type) (a :: k). Rep1 f a ~> f a
type family ((f :: b ~> c) :. (g :: a ~> b)) (x :: a) :: c where
(f :. g) x = Apply f (Apply g x)
data (.@#@$$$) :: forall b c a. (b ~> c) > (a ~> b) > (a ~> c)
type instance Apply (f .@#@$$$ g) x = (f :. g) x
(%.) :: forall a b c (f :: b ~> c) (g :: a ~> b) (x :: a).
Sing f > Sing g > Sing x > Sing ((f :. g) x)
(sf %. sg) sx = applySing sf (applySing sg sx)
(%.$$$) :: forall a b c (f :: b ~> c) (g :: a ~> b) (x :: a).
Sing f > Sing g > Sing (f .@#@$$$ g)
sf %.$$$ sg = singFun1 (sf %. sg)
f :: forall (m :: Type > Type) x. Proxy (m x) > ()
f _ = ()
where
sFrom1Fun :: forall ab. Sing (From1Sym0 :: m ab ~> Rep1 m ab)
sFrom1Fun = undefined
sTo1Fun :: forall ab. Sing (To1Sym0 :: Rep1 m ab ~> m ab)
sTo1Fun = undefined
sFrom1To1Fun :: forall ab. Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab ~> Rep1 m ab)
sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun
```
Panics on GHC 8.6:
```
$ /opt/ghc/8.6.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:50:39: error:
• Expected kind ‘m z ~> Rep1 m ab1’,
but ‘(From1Sym0 :: m z ~> Rep1 m z)’ has kind ‘m z ~> Rep1 m z’
• In the first argument of ‘(.@#@$$$)’, namely
‘(From1Sym0 :: m z ~> Rep1 m z)’
In the first argument of ‘Sing’, namely
‘(((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab
~> Rep1 m ab)’
In the type signature:
sFrom1To1Fun :: forall ab.
Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab
~> Rep1 m ab)

50  sFrom1To1Fun :: forall ab. Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab ~> Rep1 m ab)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Bug.hs:51:20: error:ghc: panic! (the 'impossible' happened)
(GHC version 8.6.0.20180823 for x86_64unknownlinux):
No skolem info:
[ab_a1UW[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
```
But merely errors on GHC 8.4.3:
```
$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:50:39: error:
• Expected kind ‘m z ~> Rep1 m ab2’,
but ‘(From1Sym0 :: m z ~> Rep1 m z)’ has kind ‘m z ~> Rep1 m z’
• In the first argument of ‘(.@#@$$$)’, namely
‘(From1Sym0 :: m z ~> Rep1 m z)’
In the first argument of ‘Sing’, namely
‘(((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab
~> Rep1 m ab)’
In the type signature:
sFrom1To1Fun :: forall ab.
Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab
~> Rep1 m ab)

50  sFrom1To1Fun :: forall ab. Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab ~> Rep1 m ab)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Bug.hs:51:20: error:
• Couldn't match type ‘ab1’ with ‘z1’
because type variable ‘z1’ would escape its scope
This (rigid, skolem) type variable is bound by
the type signature for:
sFrom1To1Fun :: forall z1 ab3. Sing (From1Sym0 .@#@$$$ To1Sym0)
at Bug.hs:50:5112
Expected type: Sing From1Sym0
Actual type: Sing From1Sym0
• In the first argument of ‘(%.$$$)’, namely ‘sFrom1Fun’
In the expression: sFrom1Fun %.$$$ sTo1Fun
In an equation for ‘sFrom1To1Fun’:
sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun
• Relevant bindings include
sFrom1To1Fun :: Sing (From1Sym0 .@#@$$$ To1Sym0)
(bound at Bug.hs:51:5)

51  sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun
 ^^^^^^^^^
Bug.hs:51:36: error:
• Couldn't match type ‘ab’ with ‘z1’
because type variable ‘z1’ would escape its scope
This (rigid, skolem) type variable is bound by
the type signature for:
sFrom1To1Fun :: forall z1 ab3. Sing (From1Sym0 .@#@$$$ To1Sym0)
at Bug.hs:50:5112
Expected type: Sing To1Sym0
Actual type: Sing To1Sym0
• In the second argument of ‘(%.$$$)’, namely ‘sTo1Fun’
In the expression: sFrom1Fun %.$$$ sTo1Fun
In an equation for ‘sFrom1To1Fun’:
sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun
• Relevant bindings include
sFrom1To1Fun :: Sing (From1Sym0 .@#@$$$ To1Sym0)
(bound at Bug.hs:51:5)

51  sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun
 ^^^^^^^
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.1beta1 
 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":"\"No skolem info\" panic (GHC 8.6 only)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1beta1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program:\r\n\r\n{{{#!hs\r\n{# LANGUAGE RankNTypes #}\r\n{# LANGUAGE ScopedTypeVariables #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeInType #}\r\n{# LANGUAGE TypeOperators #}\r\n{# LANGUAGE UndecidableInstances #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\nimport Data.Proxy\r\nimport GHC.Generics\r\n\r\ndata TyFun :: Type > Type > Type\r\ntype a ~> b = TyFun a b > Type\r\ninfixr 0 ~>\r\ntype family Apply (f :: k1 ~> k2) (x :: k1) :: k2\r\n\r\ndata family Sing :: forall k. k > Type\r\nnewtype instance Sing (f :: k1 ~> k2) =\r\n SLambda { applySing :: forall t. Sing t > Sing (Apply f t) }\r\nsingFun1 :: forall f. (forall t. Sing t > Sing (Apply f t)) > Sing f\r\nsingFun1 f = SLambda f\r\n\r\ndata From1Sym0 :: forall k (f :: k > Type) (a :: k). f a ~> Rep1 f a\r\ndata To1Sym0 :: forall k (f :: k > Type) (a :: k). Rep1 f a ~> f a\r\n\r\ntype family ((f :: b ~> c) :. (g :: a ~> b)) (x :: a) :: c where\r\n (f :. g) x = Apply f (Apply g x)\r\n\r\ndata (.@#@$$$) :: forall b c a. (b ~> c) > (a ~> b) > (a ~> c)\r\ntype instance Apply (f .@#@$$$ g) x = (f :. g) x\r\n\r\n(%.) :: forall a b c (f :: b ~> c) (g :: a ~> b) (x :: a).\r\n Sing f > Sing g > Sing x > Sing ((f :. g) x)\r\n(sf %. sg) sx = applySing sf (applySing sg sx)\r\n\r\n(%.$$$) :: forall a b c (f :: b ~> c) (g :: a ~> b) (x :: a).\r\n Sing f > Sing g > Sing (f .@#@$$$ g)\r\nsf %.$$$ sg = singFun1 (sf %. sg)\r\n\r\nf :: forall (m :: Type > Type) x. Proxy (m x) > ()\r\nf _ = ()\r\n where\r\n sFrom1Fun :: forall ab. Sing (From1Sym0 :: m ab ~> Rep1 m ab)\r\n sFrom1Fun = undefined\r\n\r\n sTo1Fun :: forall ab. Sing (To1Sym0 :: Rep1 m ab ~> m ab)\r\n sTo1Fun = undefined\r\n\r\n sFrom1To1Fun :: forall ab. Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab ~> Rep1 m ab)\r\n sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun\r\n}}}\r\n\r\nPanics on GHC 8.6:\r\n\r\n{{{\r\n$ /opt/ghc/8.6.1/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:50:39: error:\r\n • Expected kind ‘m z ~> Rep1 m ab1’,\r\n but ‘(From1Sym0 :: m z ~> Rep1 m z)’ has kind ‘m z ~> Rep1 m z’\r\n • In the first argument of ‘(.@#@$$$)’, namely\r\n ‘(From1Sym0 :: m z ~> Rep1 m z)’\r\n In the first argument of ‘Sing’, namely\r\n ‘(((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab\r\n ~> Rep1 m ab)’\r\n In the type signature:\r\n sFrom1To1Fun :: forall ab.\r\n Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab\r\n ~> Rep1 m ab)\r\n \r\n50  sFrom1To1Fun :: forall ab. Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab ~> Rep1 m ab)\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n\r\nBug.hs:51:20: error:ghc: panic! (the 'impossible' happened)\r\n (GHC version 8.6.0.20180823 for x86_64unknownlinux):\r\n No skolem info:\r\n [ab_a1UW[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\nBut merely errors on GHC 8.4.3:\r\n\r\n{{{\r\n$ /opt/ghc/8.4.3/bin/ghc Bug.hs \r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:50:39: error:\r\n • Expected kind ‘m z ~> Rep1 m ab2’,\r\n but ‘(From1Sym0 :: m z ~> Rep1 m z)’ has kind ‘m z ~> Rep1 m z’\r\n • In the first argument of ‘(.@#@$$$)’, namely\r\n ‘(From1Sym0 :: m z ~> Rep1 m z)’\r\n In the first argument of ‘Sing’, namely\r\n ‘(((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab\r\n ~> Rep1 m ab)’\r\n In the type signature:\r\n sFrom1To1Fun :: forall ab.\r\n Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab\r\n ~> Rep1 m ab)\r\n \r\n50  sFrom1To1Fun :: forall ab. Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab ~> Rep1 m ab)\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n\r\nBug.hs:51:20: error:\r\n • Couldn't match type ‘ab1’ with ‘z1’\r\n because type variable ‘z1’ would escape its scope\r\n This (rigid, skolem) type variable is bound by\r\n the type signature for:\r\n sFrom1To1Fun :: forall z1 ab3. Sing (From1Sym0 .@#@$$$ To1Sym0)\r\n at Bug.hs:50:5112\r\n Expected type: Sing From1Sym0\r\n Actual type: Sing From1Sym0\r\n • In the first argument of ‘(%.$$$)’, namely ‘sFrom1Fun’\r\n In the expression: sFrom1Fun %.$$$ sTo1Fun\r\n In an equation for ‘sFrom1To1Fun’:\r\n sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun\r\n • Relevant bindings include\r\n sFrom1To1Fun :: Sing (From1Sym0 .@#@$$$ To1Sym0)\r\n (bound at Bug.hs:51:5)\r\n \r\n51  sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun\r\n  ^^^^^^^^^\r\n\r\nBug.hs:51:36: error:\r\n • Couldn't match type ‘ab’ with ‘z1’\r\n because type variable ‘z1’ would escape its scope\r\n This (rigid, skolem) type variable is bound by\r\n the type signature for:\r\n sFrom1To1Fun :: forall z1 ab3. Sing (From1Sym0 .@#@$$$ To1Sym0)\r\n at Bug.hs:50:5112\r\n Expected type: Sing To1Sym0\r\n Actual type: Sing To1Sym0\r\n • In the second argument of ‘(%.$$$)’, namely ‘sTo1Fun’\r\n In the expression: sFrom1Fun %.$$$ sTo1Fun\r\n In an equation for ‘sFrom1To1Fun’:\r\n sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun\r\n • Relevant bindings include\r\n sFrom1To1Fun :: Sing (From1Sym0 .@#@$$$ To1Sym0)\r\n (bound at Bug.hs:51:5)\r\n \r\n51  sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun\r\n  ^^^^^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >8.8.1https://gitlab.haskell.org/ghc/ghc//issues/15624defertypeerrors and equality constraints20190707T18:03:42ZKrzysztof Gogolewskidefertypeerrors and equality constraintsConsider
```
{# OPTIONS_GHC fdefertypeerrors #}
x = const True ('a' + 'a')
y = const True (not 'a')
```
Currently `x` is True, but `y` is undefined. I think it would make sense for both to be True.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  low 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"defertypeerrors and equality constraints","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.8.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider\r\n\r\n{{{\r\n{# OPTIONS_GHC fdefertypeerrors #}\r\nx = const True ('a' + 'a')\r\ny = const True (not 'a')\r\n}}}\r\n\r\nCurrently `x` is True, but `y` is undefined. I think it would make sense for both to be True.","type_of_failure":"OtherFailure","blocking":[]} >Consider
```
{# OPTIONS_GHC fdefertypeerrors #}
x = const True ('a' + 'a')
y = const True (not 'a')
```
Currently `x` is True, but `y` is undefined. I think it would make sense for both to be True.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  low 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"defertypeerrors and equality constraints","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.8.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider\r\n\r\n{{{\r\n{# OPTIONS_GHC fdefertypeerrors #}\r\nx = const True ('a' + 'a')\r\ny = const True (not 'a')\r\n}}}\r\n\r\nCurrently `x` is True, but `y` is undefined. I think it would make sense for both to be True.","type_of_failure":"OtherFailure","blocking":[]} >8.8.1https://gitlab.haskell.org/ghc/ghc//issues/15621Error message involving type families points to wrong location20210125T16:37:52ZRyan ScottError message involving type families points to wrong locationConsider the following program:
```hs
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeOperators #}
module Bug where
import Data.Type.Equality
type family F a
f :: ()
f =
let a :: F Int :~: F Int
a = Refl
b :: F Int :~: F Bool
b = Refl
in ()
```
This doesn't typecheck, which isn't surprising, since `F Int` doesn't equal `F Bool` in the definition of `b`. What //is// surprising is where the error message points to:
```
$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:12:11: error:
• Couldn't match type ‘F Int’ with ‘F Bool’
Expected type: F Int :~: F Int
Actual type: F Bool :~: F Bool
NB: ‘F’ is a noninjective type family
• In the expression: Refl
In an equation for ‘a’: a = Refl
In the expression:
let
a :: F Int :~: F Int
a = Refl
b :: F Int :~: F Bool
....
in ()

12  a = Refl
 ^^^^
```
This claims that the error message arises from the definition of `a`, which is completely wrong! As evidence, if you comment out `b`, then the program typechecks again.
Another interesting facet of this bug is that if you comment out `a`:
```hs
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeOperators #}
module Bug where
import Data.Type.Equality
type family F a
f :: ()
f =
let { a :: F Int :~: F Int
a = Refl }
b :: F Int :~: F Bool
b = Refl
in ()
```
Then the error message will actually point to `b` this time:
```
$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:15:11: error:
• Couldn't match type ‘F Int’ with ‘F Bool’
Expected type: F Int :~: F Bool
Actual type: F Bool :~: F Bool
NB: ‘F’ is a noninjective type family
• In the expression: Refl
In an equation for ‘b’: b = Refl
In the expression:
let
b :: F Int :~: F Bool
b = Refl
in ()

15  b = Refl
 ^^^^
```
The use of type families appears to be important to triggering this bug, since I can't observe this behavior without the use of `F`.
This is a regression that was introduced at some point between GHC 8.0.2 and 8.2.2, since 8.2.2 gives the incorrect error message shown above, while 8.0.2 points to the right location:
```
$ /opt/ghc/8.0.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:15:11: error:
• Couldn't match type ‘F Int’ with ‘F Bool’
Expected type: F Int :~: F Bool
Actual type: F Int :~: F Int
NB: ‘F’ is a type function, and may not be injective
• In the expression: Refl
In an equation for ‘b’: b = Refl
In the expression:
let
a :: F Int :~: F Int
a = Refl
b :: F Int :~: F Bool
....
in ()
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.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":"Error message involving type families points to wrong location","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["TypeFamilies"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider the following program:\r\n\r\n{{{#!hs\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeOperators #}\r\nmodule Bug where\r\n\r\nimport Data.Type.Equality\r\n\r\ntype family F a\r\n\r\nf :: ()\r\nf =\r\n let a :: F Int :~: F Int\r\n a = Refl\r\n\r\n b :: F Int :~: F Bool\r\n b = Refl\r\n in ()\r\n}}}\r\n\r\nThis doesn't typecheck, which isn't surprising, since `F Int` doesn't equal `F Bool` in the definition of `b`. What //is// surprising is where the error message points to:\r\n\r\n{{{\r\n$ /opt/ghc/8.4.3/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:12:11: error:\r\n • Couldn't match type ‘F Int’ with ‘F Bool’\r\n Expected type: F Int :~: F Int\r\n Actual type: F Bool :~: F Bool\r\n NB: ‘F’ is a noninjective type family\r\n • In the expression: Refl\r\n In an equation for ‘a’: a = Refl\r\n In the expression:\r\n let\r\n a :: F Int :~: F Int\r\n a = Refl\r\n b :: F Int :~: F Bool\r\n ....\r\n in ()\r\n \r\n12  a = Refl\r\n  ^^^^\r\n}}}\r\n\r\nThis claims that the error message arises from the definition of `a`, which is completely wrong! As evidence, if you comment out `b`, then the program typechecks again.\r\n\r\nAnother interesting facet of this bug is that if you comment out `a`:\r\n\r\n{{{#!hs\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeOperators #}\r\nmodule Bug where\r\n\r\nimport Data.Type.Equality\r\n\r\ntype family F a\r\n\r\nf :: ()\r\nf =\r\n let { a :: F Int :~: F Int\r\n a = Refl }\r\n\r\n b :: F Int :~: F Bool\r\n b = Refl\r\n in ()\r\n}}}\r\n\r\nThen the error message will actually point to `b` this time:\r\n\r\n{{{\r\n$ /opt/ghc/8.4.3/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:15:11: error:\r\n • Couldn't match type ‘F Int’ with ‘F Bool’\r\n Expected type: F Int :~: F Bool\r\n Actual type: F Bool :~: F Bool\r\n NB: ‘F’ is a noninjective type family\r\n • In the expression: Refl\r\n In an equation for ‘b’: b = Refl\r\n In the expression:\r\n let\r\n b :: F Int :~: F Bool\r\n b = Refl\r\n in ()\r\n \r\n15  b = Refl\r\n  ^^^^\r\n}}}\r\n\r\nThe use of type families appears to be important to triggering this bug, since I can't observe this behavior without the use of `F`.\r\n\r\nThis is a regression that was introduced at some point between GHC 8.0.2 and 8.2.2, since 8.2.2 gives the incorrect error message shown above, while 8.0.2 points to the right location:\r\n\r\n{{{\r\n$ /opt/ghc/8.0.2/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:15:11: error:\r\n • Couldn't match type ‘F Int’ with ‘F Bool’\r\n Expected type: F Int :~: F Bool\r\n Actual type: F Int :~: F Int\r\n NB: ‘F’ is a type function, and may not be injective\r\n • In the expression: Refl\r\n In an equation for ‘b’: b = Refl\r\n In the expression:\r\n let\r\n a :: F Int :~: F Int\r\n a = Refl\r\n b :: F Int :~: F Bool\r\n ....\r\n in ()\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >Consider the following program:
```hs
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeOperators #}
module Bug where
import Data.Type.Equality
type family F a
f :: ()
f =
let a :: F Int :~: F Int
a = Refl
b :: F Int :~: F Bool
b = Refl
in ()
```
This doesn't typecheck, which isn't surprising, since `F Int` doesn't equal `F Bool` in the definition of `b`. What //is// surprising is where the error message points to:
```
$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:12:11: error:
• Couldn't match type ‘F Int’ with ‘F Bool’
Expected type: F Int :~: F Int
Actual type: F Bool :~: F Bool
NB: ‘F’ is a noninjective type family
• In the expression: Refl
In an equation for ‘a’: a = Refl
In the expression:
let
a :: F Int :~: F Int
a = Refl
b :: F Int :~: F Bool
....
in ()

12  a = Refl
 ^^^^
```
This claims that the error message arises from the definition of `a`, which is completely wrong! As evidence, if you comment out `b`, then the program typechecks again.
Another interesting facet of this bug is that if you comment out `a`:
```hs
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeOperators #}
module Bug where
import Data.Type.Equality
type family F a
f :: ()
f =
let { a :: F Int :~: F Int
a = Refl }
b :: F Int :~: F Bool
b = Refl
in ()
```
Then the error message will actually point to `b` this time:
```
$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:15:11: error:
• Couldn't match type ‘F Int’ with ‘F Bool’
Expected type: F Int :~: F Bool
Actual type: F Bool :~: F Bool
NB: ‘F’ is a noninjective type family
• In the expression: Refl
In an equation for ‘b’: b = Refl
In the expression:
let
b :: F Int :~: F Bool
b = Refl
in ()

15  b = Refl
 ^^^^
```
The use of type families appears to be important to triggering this bug, since I can't observe this behavior without the use of `F`.
This is a regression that was introduced at some point between GHC 8.0.2 and 8.2.2, since 8.2.2 gives the incorrect error message shown above, while 8.0.2 points to the right location:
```
$ /opt/ghc/8.0.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:15:11: error:
• Couldn't match type ‘F Int’ with ‘F Bool’
Expected type: F Int :~: F Bool
Actual type: F Int :~: F Int
NB: ‘F’ is a type function, and may not be injective
• In the expression: Refl
In an equation for ‘b’: b = Refl
In the expression:
let
a :: F Int :~: F Int
a = Refl
b :: F Int :~: F Bool
....
in ()
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.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":"Error message involving type families points to wrong location","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["TypeFamilies"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider the following program:\r\n\r\n{{{#!hs\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeOperators #}\r\nmodule Bug where\r\n\r\nimport Data.Type.Equality\r\n\r\ntype family F a\r\n\r\nf :: ()\r\nf =\r\n let a :: F Int :~: F Int\r\n a = Refl\r\n\r\n b :: F Int :~: F Bool\r\n b = Refl\r\n in ()\r\n}}}\r\n\r\nThis doesn't typecheck, which isn't surprising, since `F Int` doesn't equal `F Bool` in the definition of `b`. What //is// surprising is where the error message points to:\r\n\r\n{{{\r\n$ /opt/ghc/8.4.3/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:12:11: error:\r\n • Couldn't match type ‘F Int’ with ‘F Bool’\r\n Expected type: F Int :~: F Int\r\n Actual type: F Bool :~: F Bool\r\n NB: ‘F’ is a noninjective type family\r\n • In the expression: Refl\r\n In an equation for ‘a’: a = Refl\r\n In the expression:\r\n let\r\n a :: F Int :~: F Int\r\n a = Refl\r\n b :: F Int :~: F Bool\r\n ....\r\n in ()\r\n \r\n12  a = Refl\r\n  ^^^^\r\n}}}\r\n\r\nThis claims that the error message arises from the definition of `a`, which is completely wrong! As evidence, if you comment out `b`, then the program typechecks again.\r\n\r\nAnother interesting facet of this bug is that if you comment out `a`:\r\n\r\n{{{#!hs\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeOperators #}\r\nmodule Bug where\r\n\r\nimport Data.Type.Equality\r\n\r\ntype family F a\r\n\r\nf :: ()\r\nf =\r\n let { a :: F Int :~: F Int\r\n a = Refl }\r\n\r\n b :: F Int :~: F Bool\r\n b = Refl\r\n in ()\r\n}}}\r\n\r\nThen the error message will actually point to `b` this time:\r\n\r\n{{{\r\n$ /opt/ghc/8.4.3/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:15:11: error:\r\n • Couldn't match type ‘F Int’ with ‘F Bool’\r\n Expected type: F Int :~: F Bool\r\n Actual type: F Bool :~: F Bool\r\n NB: ‘F’ is a noninjective type family\r\n • In the expression: Refl\r\n In an equation for ‘b’: b = Refl\r\n In the expression:\r\n let\r\n b :: F Int :~: F Bool\r\n b = Refl\r\n in ()\r\n \r\n15  b = Refl\r\n  ^^^^\r\n}}}\r\n\r\nThe use of type families appears to be important to triggering this bug, since I can't observe this behavior without the use of `F`.\r\n\r\nThis is a regression that was introduced at some point between GHC 8.0.2 and 8.2.2, since 8.2.2 gives the incorrect error message shown above, while 8.0.2 points to the right location:\r\n\r\n{{{\r\n$ /opt/ghc/8.0.2/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:15:11: error:\r\n • Couldn't match type ‘F Int’ with ‘F Bool’\r\n Expected type: F Int :~: F Bool\r\n Actual type: F Int :~: F Int\r\n NB: ‘F’ is a type function, and may not be injective\r\n • In the expression: Refl\r\n In an equation for ‘b’: b = Refl\r\n In the expression:\r\n let\r\n a :: F Int :~: F Int\r\n a = Refl\r\n b :: F Int :~: F Bool\r\n ....\r\n in ()\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >9.2.1https://gitlab.haskell.org/ghc/ghc//issues/15577TypeApplicationsrelated infinite loop (GHC 8.6+ only)20190830T12:55:21ZRyan ScottTypeApplicationsrelated infinite loop (GHC 8.6+ only)The following program will loop infinitely when compiled on GHC 8.6 or HEAD:
```hs
{# LANGUAGE AllowAmbiguousTypes #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeApplications #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
module Bug where
import Data.Kind
import Data.Type.Equality
data family Sing :: forall k. k > Type
class Generic1 (f :: k > Type) where
type Rep1 f :: k > Type
class PGeneric1 (f :: k > Type) where
type From1 (z :: f a) :: Rep1 f a
type To1 (z :: Rep1 f a) :: f a
class SGeneric1 (f :: k > Type) where
sFrom1 :: forall (a :: k) (z :: f a). Sing z > Sing (From1 z)
sTo1 :: forall (a :: k) (r :: Rep1 f a). Sing r > Sing (To1 r :: f a)
class (PGeneric1 f, SGeneric1 f) => VGeneric1 (f :: k > Type) where
sTof1 :: forall (a :: k) (z :: f a). Sing z > To1 (From1 z) :~: z
sFot1 :: forall (a :: k) (r :: Rep1 f a). Sing r > From1 (To1 r :: f a) :~: r
foo :: forall (f :: Type > Type) (a :: Type) (r :: Rep1 f a).
VGeneric1 f
=> Sing r > From1 (To1 r :: f a) :~: r
foo x
 Refl < sFot1  Uncommenting the line below makes it work again:
 @Type
@f @a @r x
= Refl
```
This is a regression from GHC 8.4, since compiling this program with 8.4 simply errors:
```
$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:35:20: error:
• Expecting one more argument to ‘f’
Expected a type, but ‘f’ has kind ‘* > *’
• In the type ‘f’
In a stmt of a pattern guard for
an equation for ‘foo’:
Refl < sFot1 @f @a @r x
In an equation for ‘foo’: foo x  Refl < sFot1 @f @a @r x = Refl

35  @f @a @r x
 ^
Bug.hs:35:23: error:
• Expected kind ‘f1 > *’, but ‘a’ has kind ‘*’
• In the type ‘a’
In a stmt of a pattern guard for
an equation for ‘foo’:
Refl < sFot1 @f @a @r x
In an equation for ‘foo’: foo x  Refl < sFot1 @f @a @r x = Refl
• Relevant bindings include
x :: Sing r1 (bound at Bug.hs:32:5)
foo :: Sing r1 > From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)

35  @f @a @r x
 ^
Bug.hs:35:26: error:
• Couldn't match kind ‘* > *’ with ‘*’
When matching kinds
f1 :: * > *
Rep1 f1 a1 :: *
Expected kind ‘f1’, but ‘r’ has kind ‘Rep1 f1 a1’
• In the type ‘r’
In a stmt of a pattern guard for
an equation for ‘foo’:
Refl < sFot1 @f @a @r x
In an equation for ‘foo’: foo x  Refl < sFot1 @f @a @r x = Refl
• Relevant bindings include
x :: Sing r1 (bound at Bug.hs:32:5)
foo :: Sing r1 > From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)

35  @f @a @r x
 ^
Bug.hs:35:28: error:
• Couldn't match kind ‘*’ with ‘GHC.Types.RuntimeRep’
When matching kinds
a1 :: *
'GHC.Types.LiftedRep :: GHC.Types.RuntimeRep
• In the fourth argument of ‘sFot1’, namely ‘x’
In a stmt of a pattern guard for
an equation for ‘foo’:
Refl < sFot1 @f @a @r x
In an equation for ‘foo’: foo x  Refl < sFot1 @f @a @r x = Refl
• Relevant bindings include
x :: Sing r1 (bound at Bug.hs:32:5)
foo :: Sing r1 > From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)

35  @f @a @r x
 ^
Bug.hs:36:5: error:
• Could not deduce: From1 (To1 r1) ~ r1
from the context: r0 ~ From1 (To1 r0)
bound by a pattern with constructor:
Refl :: forall k (a :: k). a :~: a,
in a pattern binding in
pattern guard for
an equation for ‘foo’
at Bug.hs:33:58
‘r1’ is a rigid type variable bound by
the type signature for:
foo :: forall (f1 :: * > *) a1 (r1 :: Rep1 f1 a1).
VGeneric1 f1 =>
Sing r1 > From1 (To1 r1) :~: r1
at Bug.hs:(29,1)(31,43)
Expected type: From1 (To1 r1) :~: r1
Actual type: r1 :~: r1
• In the expression: Refl
In an equation for ‘foo’: foo x  Refl < sFot1 @f @a @r x = Refl
• Relevant bindings include
x :: Sing r1 (bound at Bug.hs:32:5)
foo :: Sing r1 > From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)

36  = Refl
 ^^^^
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  high 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"TypeApplicationsrelated infinite loop (GHC 8.6+ only)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["TypeApplications,","TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program will loop infinitely when compiled on GHC 8.6 or HEAD:\r\n\r\n{{{#!hs\r\n{# LANGUAGE AllowAmbiguousTypes #}\r\n{# LANGUAGE ScopedTypeVariables #}\r\n{# LANGUAGE TypeApplications #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeInType #}\r\n{# LANGUAGE TypeOperators #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\nimport Data.Type.Equality\r\n\r\ndata family Sing :: forall k. k > Type\r\n\r\nclass Generic1 (f :: k > Type) where\r\n type Rep1 f :: k > Type\r\n\r\nclass PGeneric1 (f :: k > Type) where\r\n type From1 (z :: f a) :: Rep1 f a\r\n type To1 (z :: Rep1 f a) :: f a\r\n\r\nclass SGeneric1 (f :: k > Type) where\r\n sFrom1 :: forall (a :: k) (z :: f a). Sing z > Sing (From1 z)\r\n sTo1 :: forall (a :: k) (r :: Rep1 f a). Sing r > Sing (To1 r :: f a)\r\n\r\nclass (PGeneric1 f, SGeneric1 f) => VGeneric1 (f :: k > Type) where\r\n sTof1 :: forall (a :: k) (z :: f a). Sing z > To1 (From1 z) :~: z\r\n sFot1 :: forall (a :: k) (r :: Rep1 f a). Sing r > From1 (To1 r :: f a) :~: r\r\n\r\nfoo :: forall (f :: Type > Type) (a :: Type) (r :: Rep1 f a).\r\n VGeneric1 f\r\n => Sing r > From1 (To1 r :: f a) :~: r\r\nfoo x\r\n  Refl < sFot1  Uncommenting the line below makes it work again:\r\n  @Type\r\n @f @a @r x\r\n = Refl\r\n}}}\r\n\r\nThis is a regression from GHC 8.4, since compiling this program with 8.4 simply errors:\r\n\r\n{{{\r\n$ /opt/ghc/8.4.3/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:35:20: error:\r\n • Expecting one more argument to ‘f’\r\n Expected a type, but ‘f’ has kind ‘* > *’\r\n • In the type ‘f’\r\n In a stmt of a pattern guard for\r\n an equation for ‘foo’:\r\n Refl < sFot1 @f @a @r x\r\n In an equation for ‘foo’: foo x  Refl < sFot1 @f @a @r x = Refl\r\n \r\n35  @f @a @r x\r\n  ^\r\n\r\nBug.hs:35:23: error:\r\n • Expected kind ‘f1 > *’, but ‘a’ has kind ‘*’\r\n • In the type ‘a’\r\n In a stmt of a pattern guard for\r\n an equation for ‘foo’:\r\n Refl < sFot1 @f @a @r x\r\n In an equation for ‘foo’: foo x  Refl < sFot1 @f @a @r x = Refl\r\n • Relevant bindings include\r\n x :: Sing r1 (bound at Bug.hs:32:5)\r\n foo :: Sing r1 > From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)\r\n \r\n35  @f @a @r x\r\n  ^\r\n\r\nBug.hs:35:26: error:\r\n • Couldn't match kind ‘* > *’ with ‘*’\r\n When matching kinds\r\n f1 :: * > *\r\n Rep1 f1 a1 :: *\r\n Expected kind ‘f1’, but ‘r’ has kind ‘Rep1 f1 a1’\r\n • In the type ‘r’\r\n In a stmt of a pattern guard for\r\n an equation for ‘foo’:\r\n Refl < sFot1 @f @a @r x\r\n In an equation for ‘foo’: foo x  Refl < sFot1 @f @a @r x = Refl\r\n • Relevant bindings include\r\n x :: Sing r1 (bound at Bug.hs:32:5)\r\n foo :: Sing r1 > From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)\r\n \r\n35  @f @a @r x\r\n  ^\r\n\r\nBug.hs:35:28: error:\r\n • Couldn't match kind ‘*’ with ‘GHC.Types.RuntimeRep’\r\n When matching kinds\r\n a1 :: *\r\n 'GHC.Types.LiftedRep :: GHC.Types.RuntimeRep\r\n • In the fourth argument of ‘sFot1’, namely ‘x’\r\n In a stmt of a pattern guard for\r\n an equation for ‘foo’:\r\n Refl < sFot1 @f @a @r x\r\n In an equation for ‘foo’: foo x  Refl < sFot1 @f @a @r x = Refl\r\n • Relevant bindings include\r\n x :: Sing r1 (bound at Bug.hs:32:5)\r\n foo :: Sing r1 > From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)\r\n \r\n35  @f @a @r x\r\n  ^\r\n\r\nBug.hs:36:5: error:\r\n • Could not deduce: From1 (To1 r1) ~ r1\r\n from the context: r0 ~ From1 (To1 r0)\r\n bound by a pattern with constructor:\r\n Refl :: forall k (a :: k). a :~: a,\r\n in a pattern binding in\r\n pattern guard for\r\n an equation for ‘foo’\r\n at Bug.hs:33:58\r\n ‘r1’ is a rigid type variable bound by\r\n the type signature for:\r\n foo :: forall (f1 :: * > *) a1 (r1 :: Rep1 f1 a1).\r\n VGeneric1 f1 =>\r\n Sing r1 > From1 (To1 r1) :~: r1\r\n at Bug.hs:(29,1)(31,43)\r\n Expected type: From1 (To1 r1) :~: r1\r\n Actual type: r1 :~: r1\r\n • In the expression: Refl\r\n In an equation for ‘foo’: foo x  Refl < sFot1 @f @a @r x = Refl\r\n • Relevant bindings include\r\n x :: Sing r1 (bound at Bug.hs:32:5)\r\n foo :: Sing r1 > From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)\r\n \r\n36  = Refl\r\n  ^^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >The following program will loop infinitely when compiled on GHC 8.6 or HEAD:
```hs
{# LANGUAGE AllowAmbiguousTypes #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeApplications #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
module Bug where
import Data.Kind
import Data.Type.Equality
data family Sing :: forall k. k > Type
class Generic1 (f :: k > Type) where
type Rep1 f :: k > Type
class PGeneric1 (f :: k > Type) where
type From1 (z :: f a) :: Rep1 f a
type To1 (z :: Rep1 f a) :: f a
class SGeneric1 (f :: k > Type) where
sFrom1 :: forall (a :: k) (z :: f a). Sing z > Sing (From1 z)
sTo1 :: forall (a :: k) (r :: Rep1 f a). Sing r > Sing (To1 r :: f a)
class (PGeneric1 f, SGeneric1 f) => VGeneric1 (f :: k > Type) where
sTof1 :: forall (a :: k) (z :: f a). Sing z > To1 (From1 z) :~: z
sFot1 :: forall (a :: k) (r :: Rep1 f a). Sing r > From1 (To1 r :: f a) :~: r
foo :: forall (f :: Type > Type) (a :: Type) (r :: Rep1 f a).
VGeneric1 f
=> Sing r > From1 (To1 r :: f a) :~: r
foo x
 Refl < sFot1  Uncommenting the line below makes it work again:
 @Type
@f @a @r x
= Refl
```
This is a regression from GHC 8.4, since compiling this program with 8.4 simply errors:
```
$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:35:20: error:
• Expecting one more argument to ‘f’
Expected a type, but ‘f’ has kind ‘* > *’
• In the type ‘f’
In a stmt of a pattern guard for
an equation for ‘foo’:
Refl < sFot1 @f @a @r x
In an equation for ‘foo’: foo x  Refl < sFot1 @f @a @r x = Refl

35  @f @a @r x
 ^
Bug.hs:35:23: error:
• Expected kind ‘f1 > *’, but ‘a’ has kind ‘*’
• In the type ‘a’
In a stmt of a pattern guard for
an equation for ‘foo’:
Refl < sFot1 @f @a @r x
In an equation for ‘foo’: foo x  Refl < sFot1 @f @a @r x = Refl
• Relevant bindings include
x :: Sing r1 (bound at Bug.hs:32:5)
foo :: Sing r1 > From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)

35  @f @a @r x
 ^
Bug.hs:35:26: error:
• Couldn't match kind ‘* > *’ with ‘*’
When matching kinds
f1 :: * > *
Rep1 f1 a1 :: *
Expected kind ‘f1’, but ‘r’ has kind ‘Rep1 f1 a1’
• In the type ‘r’
In a stmt of a pattern guard for
an equation for ‘foo’:
Refl < sFot1 @f @a @r x
In an equation for ‘foo’: foo x  Refl < sFot1 @f @a @r x = Refl
• Relevant bindings include
x :: Sing r1 (bound at Bug.hs:32:5)
foo :: Sing r1 > From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)

35  @f @a @r x
 ^
Bug.hs:35:28: error:
• Couldn't match kind ‘*’ with ‘GHC.Types.RuntimeRep’
When matching kinds
a1 :: *
'GHC.Types.LiftedRep :: GHC.Types.RuntimeRep
• In the fourth argument of ‘sFot1’, namely ‘x’
In a stmt of a pattern guard for
an equation for ‘foo’:
Refl < sFot1 @f @a @r x
In an equation for ‘foo’: foo x  Refl < sFot1 @f @a @r x = Refl
• Relevant bindings include
x :: Sing r1 (bound at Bug.hs:32:5)
foo :: Sing r1 > From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)

35  @f @a @r x
 ^
Bug.hs:36:5: error:
• Could not deduce: From1 (To1 r1) ~ r1
from the context: r0 ~ From1 (To1 r0)
bound by a pattern with constructor:
Refl :: forall k (a :: k). a :~: a,
in a pattern binding in
pattern guard for
an equation for ‘foo’
at Bug.hs:33:58
‘r1’ is a rigid type variable bound by
the type signature for:
foo :: forall (f1 :: * > *) a1 (r1 :: Rep1 f1 a1).
VGeneric1 f1 =>
Sing r1 > From1 (To1 r1) :~: r1
at Bug.hs:(29,1)(31,43)
Expected type: From1 (To1 r1) :~: r1
Actual type: r1 :~: r1
• In the expression: Refl
In an equation for ‘foo’: foo x  Refl < sFot1 @f @a @r x = Refl
• Relevant bindings include
x :: Sing r1 (bound at Bug.hs:32:5)
foo :: Sing r1 > From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)

36  = Refl
 ^^^^
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  high 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"TypeApplicationsrelated infinite loop (GHC 8.6+ only)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["TypeApplications,","TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program will loop infinitely when compiled on GHC 8.6 or HEAD:\r\n\r\n{{{#!hs\r\n{# LANGUAGE AllowAmbiguousTypes #}\r\n{# LANGUAGE ScopedTypeVariables #}\r\n{# LANGUAGE TypeApplications #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeInType #}\r\n{# LANGUAGE TypeOperators #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\nimport Data.Type.Equality\r\n\r\ndata family Sing :: forall k. k > Type\r\n\r\nclass Generic1 (f :: k > Type) where\r\n type Rep1 f :: k > Type\r\n\r\nclass PGeneric1 (f :: k > Type) where\r\n type From1 (z :: f a) :: Rep1 f a\r\n type To1 (z :: Rep1 f a) :: f a\r\n\r\nclass SGeneric1 (f :: k > Type) where\r\n sFrom1 :: forall (a :: k) (z :: f a). Sing z > Sing (From1 z)\r\n sTo1 :: forall (a :: k) (r :: Rep1 f a). Sing r > Sing (To1 r :: f a)\r\n\r\nclass (PGeneric1 f, SGeneric1 f) => VGeneric1 (f :: k > Type) where\r\n sTof1 :: forall (a :: k) (z :: f a). Sing z > To1 (From1 z) :~: z\r\n sFot1 :: forall (a :: k) (r :: Rep1 f a). Sing r > From1 (To1 r :: f a) :~: r\r\n\r\nfoo :: forall (f :: Type > Type) (a :: Type) (r :: Rep1 f a).\r\n VGeneric1 f\r\n => Sing r > From1 (To1 r :: f a) :~: r\r\nfoo x\r\n  Refl < sFot1  Uncommenting the line below makes it work again:\r\n  @Type\r\n @f @a @r x\r\n = Refl\r\n}}}\r\n\r\nThis is a regression from GHC 8.4, since compiling this program with 8.4 simply errors:\r\n\r\n{{{\r\n$ /opt/ghc/8.4.3/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:35:20: error:\r\n • Expecting one more argument to ‘f’\r\n Expected a type, but ‘f’ has kind ‘* > *’\r\n • In the type ‘f’\r\n In a stmt of a pattern guard for\r\n an equation for ‘foo’:\r\n Refl < sFot1 @f @a @r x\r\n In an equation for ‘foo’: foo x  Refl < sFot1 @f @a @r x = Refl\r\n \r\n35  @f @a @r x\r\n  ^\r\n\r\nBug.hs:35:23: error:\r\n • Expected kind ‘f1 > *’, but ‘a’ has kind ‘*’\r\n • In the type ‘a’\r\n In a stmt of a pattern guard for\r\n an equation for ‘foo’:\r\n Refl < sFot1 @f @a @r x\r\n In an equation for ‘foo’: foo x  Refl < sFot1 @f @a @r x = Refl\r\n • Relevant bindings include\r\n x :: Sing r1 (bound at Bug.hs:32:5)\r\n foo :: Sing r1 > From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)\r\n \r\n35  @f @a @r x\r\n  ^\r\n\r\nBug.hs:35:26: error:\r\n • Couldn't match kind ‘* > *’ with ‘*’\r\n When matching kinds\r\n f1 :: * > *\r\n Rep1 f1 a1 :: *\r\n Expected kind ‘f1’, but ‘r’ has kind ‘Rep1 f1 a1’\r\n • In the type ‘r’\r\n In a stmt of a pattern guard for\r\n an equation for ‘foo’:\r\n Refl < sFot1 @f @a @r x\r\n In an equation for ‘foo’: foo x  Refl < sFot1 @f @a @r x = Refl\r\n • Relevant bindings include\r\n x :: Sing r1 (bound at Bug.hs:32:5)\r\n foo :: Sing r1 > From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)\r\n \r\n35  @f @a @r x\r\n  ^\r\n\r\nBug.hs:35:28: error:\r\n • Couldn't match kind ‘*’ with ‘GHC.Types.RuntimeRep’\r\n When matching kinds\r\n a1 :: *\r\n 'GHC.Types.LiftedRep :: GHC.Types.RuntimeRep\r\n • In the fourth argument of ‘sFot1’, namely ‘x’\r\n In a stmt of a pattern guard for\r\n an equation for ‘foo’:\r\n Refl < sFot1 @f @a @r x\r\n In an equation for ‘foo’: foo x  Refl < sFot1 @f @a @r x = Refl\r\n • Relevant bindings include\r\n x :: Sing r1 (bound at Bug.hs:32:5)\r\n foo :: Sing r1 > From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)\r\n \r\n35  @f @a @r x\r\n  ^\r\n\r\nBug.hs:36:5: error:\r\n • Could not deduce: From1 (To1 r1) ~ r1\r\n from the context: r0 ~ From1 (To1 r0)\r\n bound by a pattern with constructor:\r\n Refl :: forall k (a :: k). a :~: a,\r\n in a pattern binding in\r\n pattern guard for\r\n an equation for ‘foo’\r\n at Bug.hs:33:58\r\n ‘r1’ is a rigid type variable bound by\r\n the type signature for:\r\n foo :: forall (f1 :: * > *) a1 (r1 :: Rep1 f1 a1).\r\n VGeneric1 f1 =>\r\n Sing r1 > From1 (To1 r1) :~: r1\r\n at Bug.hs:(29,1)(31,43)\r\n Expected type: From1 (To1 r1) :~: r1\r\n Actual type: r1 :~: r1\r\n • In the expression: Refl\r\n In an equation for ‘foo’: foo x  Refl < sFot1 @f @a @r x = Refl\r\n • Relevant bindings include\r\n x :: Sing r1 (bound at Bug.hs:32:5)\r\n foo :: Sing r1 > From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)\r\n \r\n36  = Refl\r\n  ^^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >8.8.2Alp MestanogullariBen GamariAlp Mestanogullarihttps://gitlab.haskell.org/ghc/ghc//issues/15549Core Lint error with EmptyCase20190707T18:04:11ZRyan ScottCore Lint error with EmptyCaseThe following program gives a Core Lint error on GHC 8.2.2 and later:
```hs
{# LANGUAGE EmptyCase #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE UndecidableInstances #}
module Bug where
import Data.Kind
import Data.Void
data family Sing (a :: k)
data V1 :: Type > Type
data instance Sing (z :: V1 p)
class Generic a where
type Rep a :: Type > Type
to :: Rep a x > a
class PGeneric a where
type To (z :: Rep a x) :: a
class SGeneric a where
sTo :: forall x (r :: Rep a x). Sing r > Sing (To r :: a)

instance Generic Void where
type Rep Void = V1
to x = case x of {}
type family EmptyCase (a :: j) :: k where
instance PGeneric Void where
type To x = EmptyCase x
instance SGeneric Void where
sTo x = case x of
```
```
$ /opt/ghc/8.4.3/bin/ghc Bug.hs dcorelint fforcerecomp
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
*** Core Lint errors : in result of Simplifier ***
Bug.hs:38:7: warning:
[in body of lambda with binder x_aZ8 :: Sing r_a12q]
Kind application error in
coercion ‘(Sing (D:R:RepVoid[0] <x_a12p>_N) <r_a12q>_N)_R’
Function kind = forall k. k > *
Arg kinds = [(V1 x_a12p, *), (r_a12q, Rep Void x_a12p)]
Fun: V1 x_a12p
(r_a12q, Rep Void x_a12p)
Bug.hs:38:7: warning:
[in body of lambda with binder x_aZ8 :: Sing r_a12q]
Kind application error in
coercion ‘D:R:SingV1z0[0] <x_a12p>_N <r_a12q>_N’
Function kind = V1 x_a12p > *
Arg kinds = [(r_a12q, Rep Void x_a12p)]
Fun: V1 x_a12p
(r_a12q, Rep Void x_a12p)
Bug.hs:38:7: warning:
[in body of lambda with binder x_aZ8 :: Sing r_a12q]
Kind application error in
coercion ‘D:R:SingV1z0[0] <x_a12p>_N <r_a12q>_N’
Function kind = V1 x_a12p > *
Arg kinds = [(r_a12q, Rep Void x_a12p)]
Fun: V1 x_a12p
(r_a12q, Rep Void x_a12p)
<no location info>: warning:
In the type ‘R:SingV1z x_a12p r_a12q’
Kind application error in type ‘R:SingV1z x_a12p r_a12q’
Function kind = forall p > V1 p > *
Arg kinds = [(x_a12p, *), (r_a12q, Rep Void x_a12p)]
Fun: V1 x_a12p
(r_a12q, Rep Void x_a12p)
<no location info>: warning:
In the type ‘R:SingV1z x_a12p r_a12q’
Kind application error in type ‘R:SingV1z x_a12p r_a12q’
Function kind = forall p > V1 p > *
Arg kinds = [(x_a12p, *), (r_a12q, Rep Void x_a12p)]
Fun: V1 x_a12p
(r_a12q, Rep Void x_a12p)
*** Offending Program ***
<elided>
$csTo_a12n :: forall x (r :: Rep Void x). Sing r > Sing (To r)
[LclId,
Arity=1,
Str=<L,U>x,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
WorkFree=True, Expandable=True,
Guidance=ALWAYS_IF(arity=1,unsat_ok=True,boring_ok=True)}]
$csTo_a12n
= \ (@ x_a12p)
(@ (r_a12q :: Rep Void x_a12p))
(x_aZ8 :: Sing r_a12q) >
case x_aZ8
`cast` ((Sing
(D:R:RepVoid[0] <x_a12p>_N) <r_a12q>_N)_R ; D:R:SingV1z0[0]
<x_a12p>_N <r_a12q>_N
:: (Sing r_a12q :: *) ~R# (R:SingV1z x_a12p r_a12q :: *))
of nt_s13T {
}
```
GHC 8.0.2 does not appear to suffer from this Core Lint error.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.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":"Core Lint error with empty closed type family","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["TypeFamilies,","TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program gives a Core Lint error on GHC 8.2.2 and later:\r\n\r\n{{{#!hs\r\n{# LANGUAGE EmptyCase #}\r\n{# LANGUAGE ScopedTypeVariables #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeInType #}\r\n{# LANGUAGE UndecidableInstances #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\nimport Data.Void\r\n\r\ndata family Sing (a :: k)\r\n\r\ndata V1 :: Type > Type\r\ndata instance Sing (z :: V1 p)\r\n\r\nclass Generic a where\r\n type Rep a :: Type > Type\r\n to :: Rep a x > a\r\n\r\nclass PGeneric a where\r\n type To (z :: Rep a x) :: a\r\n\r\nclass SGeneric a where\r\n sTo :: forall x (r :: Rep a x). Sing r > Sing (To r :: a)\r\n\r\n\r\n\r\ninstance Generic Void where\r\n type Rep Void = V1\r\n to x = case x of {}\r\n\r\ntype family EmptyCase (a :: j) :: k where\r\n\r\ninstance PGeneric Void where\r\n type To x = EmptyCase x\r\n\r\ninstance SGeneric Void where\r\n sTo x = case x of\r\n}}}\r\n{{{\r\n$ /opt/ghc/8.4.3/bin/ghc Bug.hs dcorelint fforcerecomp \r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n*** Core Lint errors : in result of Simplifier ***\r\nBug.hs:38:7: warning:\r\n [in body of lambda with binder x_aZ8 :: Sing r_a12q]\r\n Kind application error in\r\n coercion ‘(Sing (D:R:RepVoid[0] <x_a12p>_N) <r_a12q>_N)_R’\r\n Function kind = forall k. k > *\r\n Arg kinds = [(V1 x_a12p, *), (r_a12q, Rep Void x_a12p)]\r\n Fun: V1 x_a12p\r\n (r_a12q, Rep Void x_a12p)\r\nBug.hs:38:7: warning:\r\n [in body of lambda with binder x_aZ8 :: Sing r_a12q]\r\n Kind application error in\r\n coercion ‘D:R:SingV1z0[0] <x_a12p>_N <r_a12q>_N’\r\n Function kind = V1 x_a12p > *\r\n Arg kinds = [(r_a12q, Rep Void x_a12p)]\r\n Fun: V1 x_a12p\r\n (r_a12q, Rep Void x_a12p)\r\nBug.hs:38:7: warning:\r\n [in body of lambda with binder x_aZ8 :: Sing r_a12q]\r\n Kind application error in\r\n coercion ‘D:R:SingV1z0[0] <x_a12p>_N <r_a12q>_N’\r\n Function kind = V1 x_a12p > *\r\n Arg kinds = [(r_a12q, Rep Void x_a12p)]\r\n Fun: V1 x_a12p\r\n (r_a12q, Rep Void x_a12p)\r\n<no location info>: warning:\r\n In the type ‘R:SingV1z x_a12p r_a12q’\r\n Kind application error in type ‘R:SingV1z x_a12p r_a12q’\r\n Function kind = forall p > V1 p > *\r\n Arg kinds = [(x_a12p, *), (r_a12q, Rep Void x_a12p)]\r\n Fun: V1 x_a12p\r\n (r_a12q, Rep Void x_a12p)\r\n<no location info>: warning:\r\n In the type ‘R:SingV1z x_a12p r_a12q’\r\n Kind application error in type ‘R:SingV1z x_a12p r_a12q’\r\n Function kind = forall p > V1 p > *\r\n Arg kinds = [(x_a12p, *), (r_a12q, Rep Void x_a12p)]\r\n Fun: V1 x_a12p\r\n (r_a12q, Rep Void x_a12p)\r\n*** Offending Program ***\r\n\r\n<elided>\r\n\r\n$csTo_a12n :: forall x (r :: Rep Void x). Sing r > Sing (To r)\r\n[LclId,\r\n Arity=1,\r\n Str=<L,U>x,\r\n Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,\r\n WorkFree=True, Expandable=True,\r\n Guidance=ALWAYS_IF(arity=1,unsat_ok=True,boring_ok=True)}]\r\n$csTo_a12n\r\n = \\ (@ x_a12p)\r\n (@ (r_a12q :: Rep Void x_a12p))\r\n (x_aZ8 :: Sing r_a12q) >\r\n case x_aZ8\r\n `cast` ((Sing\r\n (D:R:RepVoid[0] <x_a12p>_N) <r_a12q>_N)_R ; D:R:SingV1z0[0]\r\n <x_a12p>_N <r_a12q>_N\r\n :: (Sing r_a12q :: *) ~R# (R:SingV1z x_a12p r_a12q :: *))\r\n of nt_s13T {\r\n }\r\n}}}\r\n\r\nGHC 8.0.2 does not appear to suffer from this Core Lint error.","type_of_failure":"OtherFailure","blocking":[]} >The following program gives a Core Lint error on GHC 8.2.2 and later:
```hs
{# LANGUAGE EmptyCase #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE UndecidableInstances #}
module Bug where
import Data.Kind
import Data.Void
data family Sing (a :: k)
data V1 :: Type > Type
data instance Sing (z :: V1 p)
class Generic a where
type Rep a :: Type > Type
to :: Rep a x > a
class PGeneric a where
type To (z :: Rep a x) :: a
class SGeneric a where
sTo :: forall x (r :: Rep a x). Sing r > Sing (To r :: a)

instance Generic Void where
type Rep Void = V1
to x = case x of {}
type family EmptyCase (a :: j) :: k where
instance PGeneric Void where
type To x = EmptyCase x
instance SGeneric Void where
sTo x = case x of
```
```
$ /opt/ghc/8.4.3/bin/ghc Bug.hs dcorelint fforcerecomp
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
*** Core Lint errors : in result of Simplifier ***
Bug.hs:38:7: warning:
[in body of lambda with binder x_aZ8 :: Sing r_a12q]
Kind application error in
coercion ‘(Sing (D:R:RepVoid[0] <x_a12p>_N) <r_a12q>_N)_R’
Function kind = forall k. k > *
Arg kinds = [(V1 x_a12p, *), (r_a12q, Rep Void x_a12p)]
Fun: V1 x_a12p
(r_a12q, Rep Void x_a12p)
Bug.hs:38:7: warning:
[in body of lambda with binder x_aZ8 :: Sing r_a12q]
Kind application error in
coercion ‘D:R:SingV1z0[0] <x_a12p>_N <r_a12q>_N’
Function kind = V1 x_a12p > *
Arg kinds = [(r_a12q, Rep Void x_a12p)]
Fun: V1 x_a12p
(r_a12q, Rep Void x_a12p)
Bug.hs:38:7: warning:
[in body of lambda with binder x_aZ8 :: Sing r_a12q]
Kind application error in
coercion ‘D:R:SingV1z0[0] <x_a12p>_N <r_a12q>_N’
Function kind = V1 x_a12p > *
Arg kinds = [(r_a12q, Rep Void x_a12p)]
Fun: V1 x_a12p
(r_a12q, Rep Void x_a12p)
<no location info>: warning:
In the type ‘R:SingV1z x_a12p r_a12q’
Kind application error in type ‘R:SingV1z x_a12p r_a12q’
Function kind = forall p > V1 p > *
Arg kinds = [(x_a12p, *), (r_a12q, Rep Void x_a12p)]
Fun: V1 x_a12p
(r_a12q, Rep Void x_a12p)
<no location info>: warning:
In the type ‘R:SingV1z x_a12p r_a12q’
Kind application error in type ‘R:SingV1z x_a12p r_a12q’
Function kind = forall p > V1 p > *
Arg kinds = [(x_a12p, *), (r_a12q, Rep Void x_a12p)]
Fun: V1 x_a12p
(r_a12q, Rep Void x_a12p)
*** Offending Program ***
<elided>
$csTo_a12n :: forall x (r :: Rep Void x). Sing r > Sing (To r)
[LclId,
Arity=1,
Str=<L,U>x,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
WorkFree=True, Expandable=True,
Guidance=ALWAYS_IF(arity=1,unsat_ok=True,boring_ok=True)}]
$csTo_a12n
= \ (@ x_a12p)
(@ (r_a12q :: Rep Void x_a12p))
(x_aZ8 :: Sing r_a12q) >
case x_aZ8
`cast` ((Sing
(D:R:RepVoid[0] <x_a12p>_N) <r_a12q>_N)_R ; D:R:SingV1z0[0]
<x_a12p>_N <r_a12q>_N
:: (Sing r_a12q :: *) ~R# (R:SingV1z x_a12p r_a12q :: *))
of nt_s13T {
}
```
GHC 8.0.2 does not appear to suffer from this Core Lint error.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.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":"Core Lint error with empty closed type family","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["TypeFamilies,","TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program gives a Core Lint error on GHC 8.2.2 and later:\r\n\r\n{{{#!hs\r\n{# LANGUAGE EmptyCase #}\r\n{# LANGUAGE ScopedTypeVariables #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeInType #}\r\n{# LANGUAGE UndecidableInstances #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\nimport Data.Void\r\n\r\ndata family Sing (a :: k)\r\n\r\ndata V1 :: Type > Type\r\ndata instance Sing (z :: V1 p)\r\n\r\nclass Generic a where\r\n type Rep a :: Type > Type\r\n to :: Rep a x > a\r\n\r\nclass PGeneric a where\r\n type To (z :: Rep a x) :: a\r\n\r\nclass SGeneric a where\r\n sTo :: forall x (r :: Rep a x). Sing r > Sing (To r :: a)\r\n\r\n\r\n\r\ninstance Generic Void where\r\n type Rep Void = V1\r\n to x = case x of {}\r\n\r\ntype family EmptyCase (a :: j) :: k where\r\n\r\ninstance PGeneric Void where\r\n type To x = EmptyCase x\r\n\r\ninstance SGeneric Void where\r\n sTo x = case x of\r\n}}}\r\n{{{\r\n$ /opt/ghc/8.4.3/bin/ghc Bug.hs dcorelint fforcerecomp \r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n*** Core Lint errors : in result of Simplifier ***\r\nBug.hs:38:7: warning:\r\n [in body of lambda with binder x_aZ8 :: Sing r_a12q]\r\n Kind application error in\r\n coercion ‘(Sing (D:R:RepVoid[0] <x_a12p>_N) <r_a12q>_N)_R’\r\n Function kind = forall k. k > *\r\n Arg kinds = [(V1 x_a12p, *), (r_a12q, Rep Void x_a12p)]\r\n Fun: V1 x_a12p\r\n (r_a12q, Rep Void x_a12p)\r\nBug.hs:38:7: warning:\r\n [in body of lambda with binder x_aZ8 :: Sing r_a12q]\r\n Kind application error in\r\n coercion ‘D:R:SingV1z0[0] <x_a12p>_N <r_a12q>_N’\r\n Function kind = V1 x_a12p > *\r\n Arg kinds = [(r_a12q, Rep Void x_a12p)]\r\n Fun: V1 x_a12p\r\n (r_a12q, Rep Void x_a12p)\r\nBug.hs:38:7: warning:\r\n [in body of lambda with binder x_aZ8 :: Sing r_a12q]\r\n Kind application error in\r\n coercion ‘D:R:SingV1z0[0] <x_a12p>_N <r_a12q>_N’\r\n Function kind = V1 x_a12p > *\r\n Arg kinds = [(r_a12q, Rep Void x_a12p)]\r\n Fun: V1 x_a12p\r\n (r_a12q, Rep Void x_a12p)\r\n<no location info>: warning:\r\n In the type ‘R:SingV1z x_a12p r_a12q’\r\n Kind application error in type ‘R:SingV1z x_a12p r_a12q’\r\n Function kind = forall p > V1 p > *\r\n Arg kinds = [(x_a12p, *), (r_a12q, Rep Void x_a12p)]\r\n Fun: V1 x_a12p\r\n (r_a12q, Rep Void x_a12p)\r\n<no location info>: warning:\r\n In the type ‘R:SingV1z x_a12p r_a12q’\r\n Kind application error in type ‘R:SingV1z x_a12p r_a12q’\r\n Function kind = forall p > V1 p > *\r\n Arg kinds = [(x_a12p, *), (r_a12q, Rep Void x_a12p)]\r\n Fun: V1 x_a12p\r\n (r_a12q, Rep Void x_a12p)\r\n*** Offending Program ***\r\n\r\n<elided>\r\n\r\n$csTo_a12n :: forall x (r :: Rep Void x). Sing r > Sing (To r)\r\n[LclId,\r\n Arity=1,\r\n Str=<L,U>x,\r\n Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,\r\n WorkFree=True, Expandable=True,\r\n Guidance=ALWAYS_IF(arity=1,unsat_ok=True,boring_ok=True)}]\r\n$csTo_a12n\r\n = \\ (@ x_a12p)\r\n (@ (r_a12q :: Rep Void x_a12p))\r\n (x_aZ8 :: Sing r_a12q) >\r\n case x_aZ8\r\n `cast` ((Sing\r\n (D:R:RepVoid[0] <x_a12p>_N) <r_a12q>_N)_R ; D:R:SingV1z0[0]\r\n <x_a12p>_N <r_a12q>_N\r\n :: (Sing r_a12q :: *) ~R# (R:SingV1z x_a12p r_a12q :: *))\r\n of nt_s13T {\r\n }\r\n}}}\r\n\r\nGHC 8.0.2 does not appear to suffer from this Core Lint error.","type_of_failure":"OtherFailure","blocking":[]} >8.8.1https://gitlab.haskell.org/ghc/ghc//issues/15515Bogus "No instance" error when type families appear in kinds20190707T18:04:23ZRyan ScottBogus "No instance" error when type families appear in kindsThe following code typechecks:
```hs
{# LANGUAGE TypeApplications #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
module Bug where
import Data.Kind
import Data.Proxy
class C a where
c :: Proxy a
type family F
data D :: F > Type
instance C (D :: F > Type) where
c = undefined
```
However, if we try to actually //use// that `C D` instance, like so:
```hs
c' :: Proxy (D :: F > Type)
c' = c @(D :: F > Type)
```
Then GHC gives a rather flummoxing error message:
```
$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:20:6: error:
• No instance for (C D) arising from a use of ‘c’
• In the expression: c @(D :: F > Type)
In an equation for ‘c'’: c' = c @(D :: F > Type)

20  c' = c @(D :: F > Type)
 ^^^^^^^^^^^^^^^^^^^
```
But that error is clearly misleading, as we defined such a `C D` instance directly above it!
The use of the type family `F` in the kind of `D` appears to play an important role in this bug. If I change `F` to be a data type (e.g., `data F`), then `c'` is accepted.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.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":"Bogus \"No instance\" error when type families appear in kinds","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.8.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["TypeFamilies","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following code typechecks:\r\n\r\n{{{#!hs\r\n{# LANGUAGE TypeApplications #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeInType #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\nimport Data.Proxy\r\n\r\nclass C a where\r\n c :: Proxy a\r\n\r\ntype family F\r\n\r\ndata D :: F > Type\r\n\r\ninstance C (D :: F > Type) where\r\n c = undefined\r\n}}}\r\n\r\nHowever, if we try to actually //use// that `C D` instance, like so:\r\n\r\n{{{#!hs\r\nc' :: Proxy (D :: F > Type)\r\nc' = c @(D :: F > Type)\r\n}}}\r\n\r\nThen GHC gives a rather flummoxing error message:\r\n\r\n{{{\r\n$ /opt/ghc/8.4.3/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:20:6: error:\r\n • No instance for (C D) arising from a use of ‘c’\r\n • In the expression: c @(D :: F > Type)\r\n In an equation for ‘c'’: c' = c @(D :: F > Type)\r\n \r\n20  c' = c @(D :: F > Type)\r\n  ^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nBut that error is clearly misleading, as we defined such a `C D` instance directly above it!\r\n\r\nThe use of the type family `F` in the kind of `D` appears to play an important role in this bug. If I change `F` to be a data type (e.g., `data F`), then `c'` is accepted.","type_of_failure":"OtherFailure","blocking":[]} >The following code typechecks:
```hs
{# LANGUAGE TypeApplications #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
module Bug where
import Data.Kind
import Data.Proxy
class C a where
c :: Proxy a
type family F
data D :: F > Type
instance C (D :: F > Type) where
c = undefined
```
However, if we try to actually //use// that `C D` instance, like so:
```hs
c' :: Proxy (D :: F > Type)
c' = c @(D :: F > Type)
```
Then GHC gives a rather flummoxing error message:
```
$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:20:6: error:
• No instance for (C D) arising from a use of ‘c’
• In the expression: c @(D :: F > Type)
In an equation for ‘c'’: c' = c @(D :: F > Type)

20  c' = c @(D :: F > Type)
 ^^^^^^^^^^^^^^^^^^^
```
But that error is clearly misleading, as we defined such a `C D` instance directly above it!
The use of the type family `F` in the kind of `D` appears to play an important role in this bug. If I change `F` to be a data type (e.g., `data F`), then `c'` is accepted.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.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":"Bogus \"No instance\" error when type families appear in kinds","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.8.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["TypeFamilies","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following code typechecks:\r\n\r\n{{{#!hs\r\n{# LANGUAGE TypeApplications #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeInType #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\nimport Data.Proxy\r\n\r\nclass C a where\r\n c :: Proxy a\r\n\r\ntype family F\r\n\r\ndata D :: F > Type\r\n\r\ninstance C (D :: F > Type) where\r\n c = undefined\r\n}}}\r\n\r\nHowever, if we try to actually //use// that `C D` instance, like so:\r\n\r\n{{{#!hs\r\nc' :: Proxy (D :: F > Type)\r\nc' = c @(D :: F > Type)\r\n}}}\r\n\r\nThen GHC gives a rather flummoxing error message:\r\n\r\n{{{\r\n$ /opt/ghc/8.4.3/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:20:6: error:\r\n • No instance for (C D) arising from a use of ‘c’\r\n • In the expression: c @(D :: F > Type)\r\n In an equation for ‘c'’: c' = c @(D :: F > Type)\r\n \r\n20  c' = c @(D :: F > Type)\r\n  ^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nBut that error is clearly misleading, as we defined such a `C D` instance directly above it!\r\n\r\nThe use of the type family `F` in the kind of `D` appears to play an important role in this bug. If I change `F` to be a data type (e.g., `data F`), then `c'` is accepted.","type_of_failure":"OtherFailure","blocking":[]} >8.8.1