GHC issueshttps://gitlab.haskell.org/ghc/ghc//issues20190707T18:17:03Zhttps://gitlab.haskell.org/ghc/ghc//issues/14435GHC 8.2.1 regression: ddumptctrace hangs forever20190707T18:17:03ZRyan ScottGHC 8.2.1 regression: ddumptctrace hangs foreverThanks to Christiaan Baaij for noticing this. Take this program:
```hs
{# LANGUAGE AllowAmbiguousTypes #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
{# LANGUAGE UndecidableInstances #}
module Bug where
import Data.Type.Equality
import GHC.TypeLits
type family Replicate (n :: Nat) (x :: a) :: [a] where
Replicate 0 _ = '[]
Replicate n x = x : Replicate (n  1) x
replicateSucc :: (Replicate (k + 1) x) :~: (x : Replicate k x)
replicateSucc = Refl
```
Note that this program does not typecheck (nor should it). In GHC 8.0.2 and 8.2.1, if you compile this with no tracing flags, it'll give the error:
```
$ /opt/ghc/8.2.1/bin/ghci Bug.hs
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:16:17: error:
• Couldn't match type ‘Replicate (k + 1) x’
with ‘x : Replicate k x’
Expected type: Replicate (k + 1) x :~: (x : Replicate k x)
Actual type: (x : Replicate k x) :~: (x : Replicate k x)
• In the expression: Refl
In an equation for ‘replicateSucc’: replicateSucc = Refl
• Relevant bindings include
replicateSucc :: Replicate (k + 1) x :~: (x : Replicate k x)
(bound at Bug.hs:16:1)

16  replicateSucc = Refl
 ^^^^
```
Things become interesting when you compile this program with `ddumptctrace`. In GHC 8.0.2, it'll trace some extra output and eventually reach the same error as above. In 8.2.1, however, the tracing hangs, causing compilation to never terminate! Here is the output right before it hangs:
```
lk1 :
tc_infer_args (invis) @a_11
tc_infer_args (vis)
[anon] a_11
x_a1Dt
lk1 x_a1Dt
u_tys
tclvl 1
k0_a1GD[tau:1] ~ a0_a1GF[tau:1]
arising from a type equality k0_a1GD[tau:1] ~ a0_a1GF[tau:1]
found filled tyvar k_a1GD[tau:1] :> a0_a1GE[tau:1]
u_tys
tclvl 1
* ~ *
arising from a kind equality arising from
a0_a1GE[tau:1] ~ a0_a1GF[tau:1]
u_tys
tclvl 1
'GHC.Types.LiftedRep ~ 'GHC.Types.LiftedRep
arising from a kind equality arising from
a0_a1GE[tau:1] ~ a0_a1GF[tau:1]
u_tys yields no coercion
u_tys yields no coercion
writeMetaTyVar a_a1GE[tau:1] :: * := a0_a1GF[tau:1]
u_tys yields no coercion
checkExpectedKind
k0_a1GD[tau:1]
a0_a1GF[tau:1]
<a0_a1GF[tau:1]>_N
tc_infer_args (vis)
[anon] [a_11]
Replicate (n_a1Ds  1) x_a1Dt
lk1 Replicate
instantiating tybinders: @a_a1Dp := a0_a1GG[tau:1]
instantiateTyN
```Thanks to Christiaan Baaij for noticing this. Take this program:
```hs
{# LANGUAGE AllowAmbiguousTypes #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
{# LANGUAGE UndecidableInstances #}
module Bug where
import Data.Type.Equality
import GHC.TypeLits
type family Replicate (n :: Nat) (x :: a) :: [a] where
Replicate 0 _ = '[]
Replicate n x = x : Replicate (n  1) x
replicateSucc :: (Replicate (k + 1) x) :~: (x : Replicate k x)
replicateSucc = Refl
```
Note that this program does not typecheck (nor should it). In GHC 8.0.2 and 8.2.1, if you compile this with no tracing flags, it'll give the error:
```
$ /opt/ghc/8.2.1/bin/ghci Bug.hs
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:16:17: error:
• Couldn't match type ‘Replicate (k + 1) x’
with ‘x : Replicate k x’
Expected type: Replicate (k + 1) x :~: (x : Replicate k x)
Actual type: (x : Replicate k x) :~: (x : Replicate k x)
• In the expression: Refl
In an equation for ‘replicateSucc’: replicateSucc = Refl
• Relevant bindings include
replicateSucc :: Replicate (k + 1) x :~: (x : Replicate k x)
(bound at Bug.hs:16:1)

16  replicateSucc = Refl
 ^^^^
```
Things become interesting when you compile this program with `ddumptctrace`. In GHC 8.0.2, it'll trace some extra output and eventually reach the same error as above. In 8.2.1, however, the tracing hangs, causing compilation to never terminate! Here is the output right before it hangs:
```
lk1 :
tc_infer_args (invis) @a_11
tc_infer_args (vis)
[anon] a_11
x_a1Dt
lk1 x_a1Dt
u_tys
tclvl 1
k0_a1GD[tau:1] ~ a0_a1GF[tau:1]
arising from a type equality k0_a1GD[tau:1] ~ a0_a1GF[tau:1]
found filled tyvar k_a1GD[tau:1] :> a0_a1GE[tau:1]
u_tys
tclvl 1
* ~ *
arising from a kind equality arising from
a0_a1GE[tau:1] ~ a0_a1GF[tau:1]
u_tys
tclvl 1
'GHC.Types.LiftedRep ~ 'GHC.Types.LiftedRep
arising from a kind equality arising from
a0_a1GE[tau:1] ~ a0_a1GF[tau:1]
u_tys yields no coercion
u_tys yields no coercion
writeMetaTyVar a_a1GE[tau:1] :: * := a0_a1GF[tau:1]
u_tys yields no coercion
checkExpectedKind
k0_a1GD[tau:1]
a0_a1GF[tau:1]
<a0_a1GF[tau:1]>_N
tc_infer_args (vis)
[anon] [a_11]
Replicate (n_a1Ds  1) x_a1Dt
lk1 Replicate
instantiating tybinders: @a_a1Dp := a0_a1GG[tau:1]
instantiateTyN
```https://gitlab.haskell.org/ghc/ghc//issues/14423{# complete #} should be able to handle  like {# minimal #}20190707T18:17:05ZEdward Kmett{# complete #} should be able to handle  like {# minimal #}It'd be really convenient to be able to specify these like we can with `minimal` pragmas, mixing ands and ors. I wind up with a combinatorial explosion of such annotations for the cases where it works when I have large numbers of patterns.
I have at least one use case where something that would be a trivial pattern to express with one (complicated) expression involving `` becomes 64 lines of complete pragmas, and every time I extend it this count doubles.
Consider what happens if you add a mix of actual and smart views of a data type:
```hs
{# language ViewPatterns, PatternSynonyms, GeneralizedNewtypeDeriving #}
newtype Delta = Delta Int deriving (Eq,Num)
instance Monoid Delta where
mempty = 0
mappend = (+)
data Exp = Var !Int  AP !Delta !Exp !Exp  LAM !Delta !Exp
rel 0 xs = xs
rel d (AP d' l r) = AP (d + d') l r
rel d (LAM d' b) = LAM (d + d') b
rel _ (Var n) = Var n
pattern Ap a b < AP d (rel d > a) (rel d > b) where
Ap a b = AP 0 a b
pattern Lam b < LAM d (rel d > b) where
Lam b = LAM 0 b
{# complete Var, AP, Lam #}
{# complete Var, Ap, LAM #}
{# complete Var, AP, LAM #}
```
Every data constructor I add with a smart view adds to the powerset of complete pragmas I should supply.
On the other hand with `` patterns:
```hs
{# complete Var, (Ap  AP), (Lam  LAM) #}
```
extends linearly.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1 
 Type  FeatureRequest 
 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":"{# complete #} should be able to handle  like {# minimal #}","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"It'd be really convenient to be able to specify these like we can with `minimal` pragmas, mixing ands and ors. I wind up with a combinatorial explosion of such annotations for the cases where it works when I have large numbers of patterns. \r\n\r\nI have at least one use case where something that would be a trivial pattern to express with one (complicated) expression involving `` becomes 64 lines of complete pragmas, and every time I extend it this count doubles.\r\n\r\nConsider what happens if you add a mix of actual and smart views of a data type:\r\n\r\n{{{#!hs\r\n{# language ViewPatterns, PatternSynonyms, GeneralizedNewtypeDeriving #}\r\n\r\nnewtype Delta = Delta Int deriving (Eq,Num)\r\n\r\ninstance Monoid Delta where\r\n mempty = 0\r\n mappend = (+)\r\n\r\ndata Exp = Var !Int  AP !Delta !Exp !Exp  LAM !Delta !Exp\r\n\r\nrel 0 xs = xs\r\nrel d (AP d' l r) = AP (d + d') l r\r\nrel d (LAM d' b) = LAM (d + d') b\r\nrel _ (Var n) = Var n\r\n\r\npattern Ap a b < AP d (rel d > a) (rel d > b) where\r\n Ap a b = AP 0 a b\r\n\r\npattern Lam b < LAM d (rel d > b) where\r\n Lam b = LAM 0 b\r\n\r\n{# complete Var, AP, Lam #}\r\n{# complete Var, Ap, LAM #}\r\n{# complete Var, AP, LAM #}\r\n}}}\r\n\r\nEvery data constructor I add with a smart view adds to the powerset of complete pragmas I should supply.\r\n\r\nOn the other hand with `` patterns:\r\n\r\n{{{#!hs\r\n{# complete Var, (Ap  AP), (Lam  LAM) #}\r\n}}} \r\n\r\nextends linearly.","type_of_failure":"OtherFailure","blocking":[]} >It'd be really convenient to be able to specify these like we can with `minimal` pragmas, mixing ands and ors. I wind up with a combinatorial explosion of such annotations for the cases where it works when I have large numbers of patterns.
I have at least one use case where something that would be a trivial pattern to express with one (complicated) expression involving `` becomes 64 lines of complete pragmas, and every time I extend it this count doubles.
Consider what happens if you add a mix of actual and smart views of a data type:
```hs
{# language ViewPatterns, PatternSynonyms, GeneralizedNewtypeDeriving #}
newtype Delta = Delta Int deriving (Eq,Num)
instance Monoid Delta where
mempty = 0
mappend = (+)
data Exp = Var !Int  AP !Delta !Exp !Exp  LAM !Delta !Exp
rel 0 xs = xs
rel d (AP d' l r) = AP (d + d') l r
rel d (LAM d' b) = LAM (d + d') b
rel _ (Var n) = Var n
pattern Ap a b < AP d (rel d > a) (rel d > b) where
Ap a b = AP 0 a b
pattern Lam b < LAM d (rel d > b) where
Lam b = LAM 0 b
{# complete Var, AP, Lam #}
{# complete Var, Ap, LAM #}
{# complete Var, AP, LAM #}
```
Every data constructor I add with a smart view adds to the powerset of complete pragmas I should supply.
On the other hand with `` patterns:
```hs
{# complete Var, (Ap  AP), (Lam  LAM) #}
```
extends linearly.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1 
 Type  FeatureRequest 
 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":"{# complete #} should be able to handle  like {# minimal #}","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"It'd be really convenient to be able to specify these like we can with `minimal` pragmas, mixing ands and ors. I wind up with a combinatorial explosion of such annotations for the cases where it works when I have large numbers of patterns. \r\n\r\nI have at least one use case where something that would be a trivial pattern to express with one (complicated) expression involving `` becomes 64 lines of complete pragmas, and every time I extend it this count doubles.\r\n\r\nConsider what happens if you add a mix of actual and smart views of a data type:\r\n\r\n{{{#!hs\r\n{# language ViewPatterns, PatternSynonyms, GeneralizedNewtypeDeriving #}\r\n\r\nnewtype Delta = Delta Int deriving (Eq,Num)\r\n\r\ninstance Monoid Delta where\r\n mempty = 0\r\n mappend = (+)\r\n\r\ndata Exp = Var !Int  AP !Delta !Exp !Exp  LAM !Delta !Exp\r\n\r\nrel 0 xs = xs\r\nrel d (AP d' l r) = AP (d + d') l r\r\nrel d (LAM d' b) = LAM (d + d') b\r\nrel _ (Var n) = Var n\r\n\r\npattern Ap a b < AP d (rel d > a) (rel d > b) where\r\n Ap a b = AP 0 a b\r\n\r\npattern Lam b < LAM d (rel d > b) where\r\n Lam b = LAM 0 b\r\n\r\n{# complete Var, AP, Lam #}\r\n{# complete Var, Ap, LAM #}\r\n{# complete Var, AP, LAM #}\r\n}}}\r\n\r\nEvery data constructor I add with a smart view adds to the powerset of complete pragmas I should supply.\r\n\r\nOn the other hand with `` patterns:\r\n\r\n{{{#!hs\r\n{# complete Var, (Ap  AP), (Lam  LAM) #}\r\n}}} \r\n\r\nextends linearly.","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/14422{# complete #} should be able to be at least partially type directed20210305T04:17:03ZEdward Kmett{# complete #} should be able to be at least partially type directedThe fact that `{# complete #}` pragma that was added in#8779 is tied to the set of patterns only and not the types involved can make it rather awkward or impossible to use in practice.
Say I have a bunch of types that happen to share a common `(:<)` and `Empty` pattern, for views. I'd like to be able to say that for one particular type `{# complete (:<), Empty #}` holds, but since both aren't defined in the same module and neither one mentions my type, I'm stuck in the same `Wnoincompletepatterns` mess I was in before.
I cant move the pragma to the individual view patterns because in general they aren't known to be a complete pattern set.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1 
 Type  FeatureRequest 
 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":"{# complete #} should be able to be at least partially type directed","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"The fact that `{# complete #}` pragma that was added in#8779 is tied to the set of patterns only and not the types involved can make it rather awkward or impossible to use in practice.\r\n\r\nSay I have a bunch of types that happen to share a common `(:<)` and `Empty` pattern, for views. I'd like to be able to say that for one particular type `{# complete (:<), Empty #}` holds, but since both aren't defined in the same module and neither one mentions my type, I'm stuck in the same `Wnoincompletepatterns` mess I was in before. \r\n\r\nI cant move the pragma to the individual view patterns because in general they aren't known to be a complete pattern set.","type_of_failure":"OtherFailure","blocking":[]} >The fact that `{# complete #}` pragma that was added in#8779 is tied to the set of patterns only and not the types involved can make it rather awkward or impossible to use in practice.
Say I have a bunch of types that happen to share a common `(:<)` and `Empty` pattern, for views. I'd like to be able to say that for one particular type `{# complete (:<), Empty #}` holds, but since both aren't defined in the same module and neither one mentions my type, I'm stuck in the same `Wnoincompletepatterns` mess I was in before.
I cant move the pragma to the individual view patterns because in general they aren't known to be a complete pattern set.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1 
 Type  FeatureRequest 
 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":"{# complete #} should be able to be at least partially type directed","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"The fact that `{# complete #}` pragma that was added in#8779 is tied to the set of patterns only and not the types involved can make it rather awkward or impossible to use in practice.\r\n\r\nSay I have a bunch of types that happen to share a common `(:<)` and `Empty` pattern, for views. I'd like to be able to say that for one particular type `{# complete (:<), Empty #}` holds, but since both aren't defined in the same module and neither one mentions my type, I'm stuck in the same `Wnoincompletepatterns` mess I was in before. \r\n\r\nI cant move the pragma to the individual view patterns because in general they aren't known to be a complete pattern set.","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/14417Overly specific instances may not be resolved20190707T18:17:07ZDavid FeuerOverly specific instances may not be resolved```hs
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE UndecidableInstances #}
class A x
class A x => B x
class A x => C x
instance B x => C x
```
produces
```
BrokenSuper.hs:8:10: error:
• Could not deduce (A x)
arising from the superclasses of an instance declaration
from the context: B x
bound by the instance declaration at BrokenSuper.hs:8:1019
Possible fix: add (A x) to the context of the instance declaration
• In the instance declaration for ‘C x’

8  instance B x => C x
```
This was noticed in [this SO question](https://stackoverflow.com/questions/47093627/cannotdeducesuperclass) and reduced by Daniel Wagner.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  goldfire 
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Overly specific instances may not be resolved","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.4.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":["goldfire"],"type":"Bug","description":"{{{#!hs\r\n{# LANGUAGE FlexibleInstances #}\r\n{# LANGUAGE UndecidableInstances #}\r\nclass A x\r\nclass A x => B x\r\nclass A x => C x\r\ninstance B x => C x\r\n}}}\r\n\r\nproduces\r\n\r\n{{{\r\nBrokenSuper.hs:8:10: error:\r\n • Could not deduce (A x)\r\n arising from the superclasses of an instance declaration\r\n from the context: B x\r\n bound by the instance declaration at BrokenSuper.hs:8:1019\r\n Possible fix: add (A x) to the context of the instance declaration\r\n • In the instance declaration for ‘C x’\r\n \r\n8  instance B x => C x\r\n}}}\r\n\r\nThis was noticed in [https://stackoverflow.com/questions/47093627/cannotdeducesuperclass this SO question] and reduced by Daniel Wagner.","type_of_failure":"OtherFailure","blocking":[]} >```hs
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE UndecidableInstances #}
class A x
class A x => B x
class A x => C x
instance B x => C x
```
produces
```
BrokenSuper.hs:8:10: error:
• Could not deduce (A x)
arising from the superclasses of an instance declaration
from the context: B x
bound by the instance declaration at BrokenSuper.hs:8:1019
Possible fix: add (A x) to the context of the instance declaration
• In the instance declaration for ‘C x’

8  instance B x => C x
```
This was noticed in [this SO question](https://stackoverflow.com/questions/47093627/cannotdeducesuperclass) and reduced by Daniel Wagner.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  goldfire 
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Overly specific instances may not be resolved","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.4.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":["goldfire"],"type":"Bug","description":"{{{#!hs\r\n{# LANGUAGE FlexibleInstances #}\r\n{# LANGUAGE UndecidableInstances #}\r\nclass A x\r\nclass A x => B x\r\nclass A x => C x\r\ninstance B x => C x\r\n}}}\r\n\r\nproduces\r\n\r\n{{{\r\nBrokenSuper.hs:8:10: error:\r\n • Could not deduce (A x)\r\n arising from the superclasses of an instance declaration\r\n from the context: B x\r\n bound by the instance declaration at BrokenSuper.hs:8:1019\r\n Possible fix: add (A x) to the context of the instance declaration\r\n • In the instance declaration for ‘C x’\r\n \r\n8  instance B x => C x\r\n}}}\r\n\r\nThis was noticed in [https://stackoverflow.com/questions/47093627/cannotdeducesuperclass this SO question] and reduced by Daniel Wagner.","type_of_failure":"OtherFailure","blocking":[]} >8.4.1https://gitlab.haskell.org/ghc/ghc//issues/14395Redefining pattern synonym in GHCi triggers "‘p’ is untouchable" error20190707T18:17:11ZRyan ScottRedefining pattern synonym in GHCi triggers "‘p’ is untouchable" errorLoad this file into GHCi:
```hs
{# LANGUAGE GADTs #}
{# LANGUAGE PatternSynonyms #}
module Bug where
data Foo a where
FooInt :: Foo Int
pattern Bar :: () => (a ~ Int) => Foo a
pattern Bar = FooInt
```
And attempt to redefine `Bar` as follows:
```
$ /opt/ghc/8.2.1/bin/ghci Bug.hs
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Ok, 1 module loaded.
λ> pattern Bar = Nothing
<interactive>:1:15: error:
• Couldn't match expected type ‘p’ with actual type ‘Maybe a0’
‘p’ is untouchable
inside the constraints: a ~ Int
bound by a pattern with pattern synonym:
Bar :: forall a. () => a ~ Int => Foo a,
in an equation for ‘pattern’
at <interactive>:1:911
‘p’ is a rigid type variable bound by
the inferred type of pattern :: Foo a > p at <interactive>:1:121
Possible fix: add a type signature for ‘pattern’
• In the expression: Nothing
In an equation for ‘pattern’: pattern Bar = Nothing
• Relevant bindings include
pattern :: Foo a > p (bound at <interactive>:1:1)
```
There are two issues here:
1. There are several places in the error message that refer to a `pattern` with no name!
```
in an equation for ‘pattern’
```
```
the inferred type of pattern :: Foo a > p at <interactive>:1:121
```
```
• Relevant bindings include
pattern :: Foo a > p (bound at <interactive>:1:1)
```
1. Why is this error happening in the first place? The error message mentions the type `Foo a > p`, but in `pattern Bar = Nothing`, there isn't anything that should touch `Foo`.
Note that this bug does not occur if a slightly different (but ostensibly equivalent) type signature for `Bar` is given in the original source file:
```hs
{# LANGUAGE GADTs #}
{# LANGUAGE PatternSynonyms #}
module Works where
data Foo a where
FooInt :: Foo Int
pattern Bar :: Foo Int
pattern Bar = FooInt
```
```
λ> pattern Bar = Nothing
λ> :i Bar
pattern Bar :: Foo Int
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Redefining pattern synonym in GHCi triggers \"‘p’ is untouchable\" error","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["PatternSynonyms"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Load this file into GHCi:\r\n\r\n{{{#!hs\r\n{# LANGUAGE GADTs #}\r\n{# LANGUAGE PatternSynonyms #}\r\nmodule Bug where\r\n\r\ndata Foo a where\r\n FooInt :: Foo Int\r\n\r\npattern Bar :: () => (a ~ Int) => Foo a\r\npattern Bar = FooInt\r\n}}}\r\n\r\nAnd attempt to redefine `Bar` as follows:\r\n\r\n{{{\r\n$ /opt/ghc/8.2.1/bin/ghci Bug.hs\r\nGHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\nOk, 1 module loaded.\r\nλ> pattern Bar = Nothing\r\n\r\n<interactive>:1:15: error:\r\n • Couldn't match expected type ‘p’ with actual type ‘Maybe a0’\r\n ‘p’ is untouchable\r\n inside the constraints: a ~ Int\r\n bound by a pattern with pattern synonym:\r\n Bar :: forall a. () => a ~ Int => Foo a,\r\n in an equation for ‘pattern’\r\n at <interactive>:1:911\r\n ‘p’ is a rigid type variable bound by\r\n the inferred type of pattern :: Foo a > p at <interactive>:1:121\r\n Possible fix: add a type signature for ‘pattern’\r\n • In the expression: Nothing\r\n In an equation for ‘pattern’: pattern Bar = Nothing\r\n • Relevant bindings include\r\n pattern :: Foo a > p (bound at <interactive>:1:1)\r\n}}}\r\n\r\nThere are two issues here:\r\n\r\n1. There are several places in the error message that refer to a `pattern` with no name!\r\n\r\n{{{\r\n in an equation for ‘pattern’\r\n}}}\r\n{{{\r\n the inferred type of pattern :: Foo a > p at <interactive>:1:121\r\n}}}\r\n{{{\r\n • Relevant bindings include\r\n pattern :: Foo a > p (bound at <interactive>:1:1)\r\n}}}\r\n\r\n2. Why is this error happening in the first place? The error message mentions the type `Foo a > p`, but in `pattern Bar = Nothing`, there isn't anything that should touch `Foo`.\r\n\r\nNote that this bug does not occur if a slightly different (but ostensibly equivalent) type signature for `Bar` is given in the original source file:\r\n\r\n{{{#!hs\r\n{# LANGUAGE GADTs #}\r\n{# LANGUAGE PatternSynonyms #}\r\nmodule Works where\r\n\r\ndata Foo a where\r\n FooInt :: Foo Int\r\n\r\npattern Bar :: Foo Int\r\npattern Bar = FooInt\r\n}}}\r\n{{{\r\nλ> pattern Bar = Nothing\r\nλ> :i Bar\r\npattern Bar :: Foo Int\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >Load this file into GHCi:
```hs
{# LANGUAGE GADTs #}
{# LANGUAGE PatternSynonyms #}
module Bug where
data Foo a where
FooInt :: Foo Int
pattern Bar :: () => (a ~ Int) => Foo a
pattern Bar = FooInt
```
And attempt to redefine `Bar` as follows:
```
$ /opt/ghc/8.2.1/bin/ghci Bug.hs
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Ok, 1 module loaded.
λ> pattern Bar = Nothing
<interactive>:1:15: error:
• Couldn't match expected type ‘p’ with actual type ‘Maybe a0’
‘p’ is untouchable
inside the constraints: a ~ Int
bound by a pattern with pattern synonym:
Bar :: forall a. () => a ~ Int => Foo a,
in an equation for ‘pattern’
at <interactive>:1:911
‘p’ is a rigid type variable bound by
the inferred type of pattern :: Foo a > p at <interactive>:1:121
Possible fix: add a type signature for ‘pattern’
• In the expression: Nothing
In an equation for ‘pattern’: pattern Bar = Nothing
• Relevant bindings include
pattern :: Foo a > p (bound at <interactive>:1:1)
```
There are two issues here:
1. There are several places in the error message that refer to a `pattern` with no name!
```
in an equation for ‘pattern’
```
```
the inferred type of pattern :: Foo a > p at <interactive>:1:121
```
```
• Relevant bindings include
pattern :: Foo a > p (bound at <interactive>:1:1)
```
1. Why is this error happening in the first place? The error message mentions the type `Foo a > p`, but in `pattern Bar = Nothing`, there isn't anything that should touch `Foo`.
Note that this bug does not occur if a slightly different (but ostensibly equivalent) type signature for `Bar` is given in the original source file:
```hs
{# LANGUAGE GADTs #}
{# LANGUAGE PatternSynonyms #}
module Works where
data Foo a where
FooInt :: Foo Int
pattern Bar :: Foo Int
pattern Bar = FooInt
```
```
λ> pattern Bar = Nothing
λ> :i Bar
pattern Bar :: Foo Int
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Redefining pattern synonym in GHCi triggers \"‘p’ is untouchable\" error","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["PatternSynonyms"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Load this file into GHCi:\r\n\r\n{{{#!hs\r\n{# LANGUAGE GADTs #}\r\n{# LANGUAGE PatternSynonyms #}\r\nmodule Bug where\r\n\r\ndata Foo a where\r\n FooInt :: Foo Int\r\n\r\npattern Bar :: () => (a ~ Int) => Foo a\r\npattern Bar = FooInt\r\n}}}\r\n\r\nAnd attempt to redefine `Bar` as follows:\r\n\r\n{{{\r\n$ /opt/ghc/8.2.1/bin/ghci Bug.hs\r\nGHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\nOk, 1 module loaded.\r\nλ> pattern Bar = Nothing\r\n\r\n<interactive>:1:15: error:\r\n • Couldn't match expected type ‘p’ with actual type ‘Maybe a0’\r\n ‘p’ is untouchable\r\n inside the constraints: a ~ Int\r\n bound by a pattern with pattern synonym:\r\n Bar :: forall a. () => a ~ Int => Foo a,\r\n in an equation for ‘pattern’\r\n at <interactive>:1:911\r\n ‘p’ is a rigid type variable bound by\r\n the inferred type of pattern :: Foo a > p at <interactive>:1:121\r\n Possible fix: add a type signature for ‘pattern’\r\n • In the expression: Nothing\r\n In an equation for ‘pattern’: pattern Bar = Nothing\r\n • Relevant bindings include\r\n pattern :: Foo a > p (bound at <interactive>:1:1)\r\n}}}\r\n\r\nThere are two issues here:\r\n\r\n1. There are several places in the error message that refer to a `pattern` with no name!\r\n\r\n{{{\r\n in an equation for ‘pattern’\r\n}}}\r\n{{{\r\n the inferred type of pattern :: Foo a > p at <interactive>:1:121\r\n}}}\r\n{{{\r\n • Relevant bindings include\r\n pattern :: Foo a > p (bound at <interactive>:1:1)\r\n}}}\r\n\r\n2. Why is this error happening in the first place? The error message mentions the type `Foo a > p`, but in `pattern Bar = Nothing`, there isn't anything that should touch `Foo`.\r\n\r\nNote that this bug does not occur if a slightly different (but ostensibly equivalent) type signature for `Bar` is given in the original source file:\r\n\r\n{{{#!hs\r\n{# LANGUAGE GADTs #}\r\n{# LANGUAGE PatternSynonyms #}\r\nmodule Works where\r\n\r\ndata Foo a where\r\n FooInt :: Foo Int\r\n\r\npattern Bar :: Foo Int\r\npattern Bar = FooInt\r\n}}}\r\n{{{\r\nλ> pattern Bar = Nothing\r\nλ> :i Bar\r\npattern Bar :: Foo Int\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/14394Inferred type for pattern synonym has redundant equality constraint20190707T18:17:11ZRyan ScottInferred type for pattern synonym has redundant equality constraintLoad this file into GHCi:
```hs
{# LANGUAGE GADTs #}
{# LANGUAGE PatternSynonyms #}
module Bug where
import Data.Type.Equality
pattern Foo = HRefl
```
```
$ /opt/ghc/8.2.1/bin/ghci Bug.hs
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Ok, 1 module loaded.
λ> :i Foo
pattern Foo :: () => (* ~ *, b ~ a) => a :~~: b
```
Notice that the type signature for `Foo` has an entirely redundant `* ~ *` constraint. The same does not happen if `TypeInType` is enabled.
```hs
{# LANGUAGE GADTs #}
{# LANGUAGE PatternSynonyms #}
{# LANGUAGE TypeInType #}
module Works where
import Data.Type.Equality
pattern Foo = HRefl
```
```
λ> :i Foo
pattern Foo :: forall k2 k1 (a :: k1) (b :: k2). () => (k2 ~ k1,
(b :: k2) ~~ (a :: k1)) => a :~~: b
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Inferred type for pattern synonym has redundant equality constraint","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["PatternSynonyms,","TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Load this file into GHCi:\r\n\r\n{{{#!hs\r\n{# LANGUAGE GADTs #}\r\n{# LANGUAGE PatternSynonyms #}\r\nmodule Bug where\r\n\r\nimport Data.Type.Equality\r\n\r\npattern Foo = HRefl\r\n}}}\r\n{{{\r\n$ /opt/ghc/8.2.1/bin/ghci Bug.hs\r\nGHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\nOk, 1 module loaded.\r\nλ> :i Foo\r\npattern Foo :: () => (* ~ *, b ~ a) => a :~~: b\r\n}}}\r\n\r\nNotice that the type signature for `Foo` has an entirely redundant `* ~ *` constraint. The same does not happen if `TypeInType` is enabled.\r\n\r\n{{{#!hs\r\n{# LANGUAGE GADTs #}\r\n{# LANGUAGE PatternSynonyms #}\r\n{# LANGUAGE TypeInType #}\r\nmodule Works where\r\n\r\nimport Data.Type.Equality\r\n\r\npattern Foo = HRefl\r\n}}}\r\n{{{\r\nλ> :i Foo\r\npattern Foo :: forall k2 k1 (a :: k1) (b :: k2). () => (k2 ~ k1,\r\n (b :: k2) ~~ (a :: k1)) => a :~~: b\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >Load this file into GHCi:
```hs
{# LANGUAGE GADTs #}
{# LANGUAGE PatternSynonyms #}
module Bug where
import Data.Type.Equality
pattern Foo = HRefl
```
```
$ /opt/ghc/8.2.1/bin/ghci Bug.hs
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Ok, 1 module loaded.
λ> :i Foo
pattern Foo :: () => (* ~ *, b ~ a) => a :~~: b
```
Notice that the type signature for `Foo` has an entirely redundant `* ~ *` constraint. The same does not happen if `TypeInType` is enabled.
```hs
{# LANGUAGE GADTs #}
{# LANGUAGE PatternSynonyms #}
{# LANGUAGE TypeInType #}
module Works where
import Data.Type.Equality
pattern Foo = HRefl
```
```
λ> :i Foo
pattern Foo :: forall k2 k1 (a :: k1) (b :: k2). () => (k2 ~ k1,
(b :: k2) ~~ (a :: k1)) => a :~~: b
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Inferred type for pattern synonym has redundant equality constraint","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["PatternSynonyms,","TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Load this file into GHCi:\r\n\r\n{{{#!hs\r\n{# LANGUAGE GADTs #}\r\n{# LANGUAGE PatternSynonyms #}\r\nmodule Bug where\r\n\r\nimport Data.Type.Equality\r\n\r\npattern Foo = HRefl\r\n}}}\r\n{{{\r\n$ /opt/ghc/8.2.1/bin/ghci Bug.hs\r\nGHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\nOk, 1 module loaded.\r\nλ> :i Foo\r\npattern Foo :: () => (* ~ *, b ~ a) => a :~~: b\r\n}}}\r\n\r\nNotice that the type signature for `Foo` has an entirely redundant `* ~ *` constraint. The same does not happen if `TypeInType` is enabled.\r\n\r\n{{{#!hs\r\n{# LANGUAGE GADTs #}\r\n{# LANGUAGE PatternSynonyms #}\r\n{# LANGUAGE TypeInType #}\r\nmodule Works where\r\n\r\nimport Data.Type.Equality\r\n\r\npattern Foo = HRefl\r\n}}}\r\n{{{\r\nλ> :i Foo\r\npattern Foo :: forall k2 k1 (a :: k1) (b :: k2). () => (k2 ~ k1,\r\n (b :: k2) ~~ (a :: k1)) => a :~~: b\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/14369GHC warns an injective type family "may not be injective"20190707T18:17:17ZRyan ScottGHC warns an injective type family "may not be injective"```hs
{# LANGUAGE AllowAmbiguousTypes #}
{# LANGUAGE GADTs #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeApplications #}
{# LANGUAGE TypeFamilyDependencies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
data family Sing (a :: k)
data instance Sing (z :: Maybe a) where
SNothing :: Sing Nothing
SJust :: Sing x > Sing (Just x)
class SingKind k where
type Demote k = r  r > k
fromSing :: Sing (a :: k) > Demote k
instance SingKind a => SingKind (Maybe a) where
type Demote (Maybe a) = Maybe (Demote a)
fromSing SNothing = Nothing
fromSing (SJust x) = Just (fromSing x)
f :: forall (x :: forall a. Maybe a) a. SingKind a => Sing x > Maybe (Demote a)
f = fromSing
```
```
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main ( Bug.hs, interpreted )
Bug.hs:26:5: error:
• Couldn't match type ‘Demote a’ with ‘Demote a1’
Expected type: Sing (x a) > Maybe (Demote a1)
Actual type: Sing (x a) > Demote (Maybe a)
NB: ‘Demote’ is a type function, and may not be injective
• In the expression: fromSing
In an equation for ‘f’: f = fromSing
• Relevant bindings include
f :: Sing (x a) > Maybe (Demote a1) (bound at Bug.hs:26:1)

26  f = fromSing
 ^^^^^^^^
```
That `NB: ‘Demote’ is a type function, and may not be injective` suggestion shouldn't be shown here, since `Demote` is definitely injective.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"GHC warns an injective type family \"may not be injective\"","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["InjectiveFamilies"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{# LANGUAGE AllowAmbiguousTypes #}\r\n{# LANGUAGE GADTs #}\r\n{# LANGUAGE RankNTypes #}\r\n{# LANGUAGE ScopedTypeVariables #}\r\n{# LANGUAGE TypeApplications #}\r\n{# LANGUAGE TypeFamilyDependencies #}\r\n{# LANGUAGE TypeInType #}\r\n{# LANGUAGE TypeOperators #}\r\n\r\ndata family Sing (a :: k)\r\n\r\ndata instance Sing (z :: Maybe a) where\r\n SNothing :: Sing Nothing\r\n SJust :: Sing x > Sing (Just x)\r\n\r\nclass SingKind k where\r\n type Demote k = r  r > k\r\n fromSing :: Sing (a :: k) > Demote k\r\n\r\ninstance SingKind a => SingKind (Maybe a) where\r\n type Demote (Maybe a) = Maybe (Demote a)\r\n fromSing SNothing = Nothing\r\n fromSing (SJust x) = Just (fromSing x)\r\n\r\nf :: forall (x :: forall a. Maybe a) a. SingKind a => Sing x > Maybe (Demote a)\r\nf = fromSing\r\n}}}\r\n{{{\r\nGHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Main ( Bug.hs, interpreted )\r\n\r\nBug.hs:26:5: error:\r\n • Couldn't match type ‘Demote a’ with ‘Demote a1’\r\n Expected type: Sing (x a) > Maybe (Demote a1)\r\n Actual type: Sing (x a) > Demote (Maybe a)\r\n NB: ‘Demote’ is a type function, and may not be injective\r\n • In the expression: fromSing\r\n In an equation for ‘f’: f = fromSing\r\n • Relevant bindings include\r\n f :: Sing (x a) > Maybe (Demote a1) (bound at Bug.hs:26:1)\r\n \r\n26  f = fromSing\r\n  ^^^^^^^^\r\n}}}\r\n\r\nThat `NB: ‘Demote’ is a type function, and may not be injective` suggestion shouldn't be shown here, since `Demote` is definitely injective.","type_of_failure":"OtherFailure","blocking":[]} >```hs
{# LANGUAGE AllowAmbiguousTypes #}
{# LANGUAGE GADTs #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeApplications #}
{# LANGUAGE TypeFamilyDependencies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
data family Sing (a :: k)
data instance Sing (z :: Maybe a) where
SNothing :: Sing Nothing
SJust :: Sing x > Sing (Just x)
class SingKind k where
type Demote k = r  r > k
fromSing :: Sing (a :: k) > Demote k
instance SingKind a => SingKind (Maybe a) where
type Demote (Maybe a) = Maybe (Demote a)
fromSing SNothing = Nothing
fromSing (SJust x) = Just (fromSing x)
f :: forall (x :: forall a. Maybe a) a. SingKind a => Sing x > Maybe (Demote a)
f = fromSing
```
```
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main ( Bug.hs, interpreted )
Bug.hs:26:5: error:
• Couldn't match type ‘Demote a’ with ‘Demote a1’
Expected type: Sing (x a) > Maybe (Demote a1)
Actual type: Sing (x a) > Demote (Maybe a)
NB: ‘Demote’ is a type function, and may not be injective
• In the expression: fromSing
In an equation for ‘f’: f = fromSing
• Relevant bindings include
f :: Sing (x a) > Maybe (Demote a1) (bound at Bug.hs:26:1)

26  f = fromSing
 ^^^^^^^^
```
That `NB: ‘Demote’ is a type function, and may not be injective` suggestion shouldn't be shown here, since `Demote` is definitely injective.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"GHC warns an injective type family \"may not be injective\"","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["InjectiveFamilies"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{# LANGUAGE AllowAmbiguousTypes #}\r\n{# LANGUAGE GADTs #}\r\n{# LANGUAGE RankNTypes #}\r\n{# LANGUAGE ScopedTypeVariables #}\r\n{# LANGUAGE TypeApplications #}\r\n{# LANGUAGE TypeFamilyDependencies #}\r\n{# LANGUAGE TypeInType #}\r\n{# LANGUAGE TypeOperators #}\r\n\r\ndata family Sing (a :: k)\r\n\r\ndata instance Sing (z :: Maybe a) where\r\n SNothing :: Sing Nothing\r\n SJust :: Sing x > Sing (Just x)\r\n\r\nclass SingKind k where\r\n type Demote k = r  r > k\r\n fromSing :: Sing (a :: k) > Demote k\r\n\r\ninstance SingKind a => SingKind (Maybe a) where\r\n type Demote (Maybe a) = Maybe (Demote a)\r\n fromSing SNothing = Nothing\r\n fromSing (SJust x) = Just (fromSing x)\r\n\r\nf :: forall (x :: forall a. Maybe a) a. SingKind a => Sing x > Maybe (Demote a)\r\nf = fromSing\r\n}}}\r\n{{{\r\nGHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Main ( Bug.hs, interpreted )\r\n\r\nBug.hs:26:5: error:\r\n • Couldn't match type ‘Demote a’ with ‘Demote a1’\r\n Expected type: Sing (x a) > Maybe (Demote a1)\r\n Actual type: Sing (x a) > Demote (Maybe a)\r\n NB: ‘Demote’ is a type function, and may not be injective\r\n • In the expression: fromSing\r\n In an equation for ‘f’: f = fromSing\r\n • Relevant bindings include\r\n f :: Sing (x a) > Maybe (Demote a1) (bound at Bug.hs:26:1)\r\n \r\n26  f = fromSing\r\n  ^^^^^^^^\r\n}}}\r\n\r\nThat `NB: ‘Demote’ is a type function, and may not be injective` suggestion shouldn't be shown here, since `Demote` is definitely injective.","type_of_failure":"OtherFailure","blocking":[]} >8.4.1https://gitlab.haskell.org/ghc/ghc//issues/14368GHC 8.2.1 doesn't inform you when the monomorphism restriction kicks in anymore20190707T18:17:18ZRyan ScottGHC 8.2.1 doesn't inform you when the monomorphism restriction kicks in anymoreThis program doesn't typecheck due to the monomorphism restriction:
```hs
f = (==)
```
In GHC 8.0.2, the error message was quite helpful in informing you of this fact:
```
GHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main ( Bug.hs, interpreted )
Bug.hs:1:1: error:
• Ambiguous type variable ‘a0’ arising from a use of ‘==’
prevents the constraint ‘(Eq a0)’ from being solved.
Probable fix: use a type annotation to specify what ‘a0’ should be.
These potential instances exist:
instance Eq Ordering  Defined in ‘GHC.Classes’
instance Eq Integer
 Defined in ‘integergmp1.0.0.1:GHC.Integer.Type’
instance Eq a => Eq (Maybe a)  Defined in ‘GHC.Base’
...plus 22 others
...plus 7 instances involving outofscope types
(use fprintpotentialinstances to see them all)
• When instantiating ‘f’, initially inferred to have
this overlygeneral type:
forall a. Eq a => a > a > Bool
NB: This instantiation can be caused by the monomorphism restriction.
```
Notice the `NB: This instantiation can be caused by the monomorphism restriction` part. But in GHC 8.2.1, this advice has mysteriously vanished!
```
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main ( Bug.hs, interpreted )
Bug.hs:1:5: error:
• Ambiguous type variable ‘a0’ arising from a use of ‘==’
prevents the constraint ‘(Eq a0)’ from being solved.
Relevant bindings include
f :: a0 > a0 > Bool (bound at Bug.hs:1:1)
Probable fix: use a type annotation to specify what ‘a0’ should be.
These potential instances exist:
instance Eq Ordering  Defined in ‘GHC.Classes’
instance Eq Integer
 Defined in ‘integergmp1.0.1.0:GHC.Integer.Type’
instance Eq a => Eq (Maybe a)  Defined in ‘GHC.Base’
...plus 22 others
...plus 9 instances involving outofscope types
(use fprintpotentialinstances to see them all)
• In the expression: (==)
In an equation for ‘f’: f = (==)

1  f = (==)
 ^^^^
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"GHC 8.2.1 doesn't inform you when the monomorphism restriction kicks in anymore","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This program doesn't typecheck due to the monomorphism restriction:\r\n\r\n{{{#!hs\r\nf = (==)\r\n}}}\r\n\r\nIn GHC 8.0.2, the error message was quite helpful in informing you of this fact:\r\n\r\n{{{\r\nGHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Main ( Bug.hs, interpreted )\r\n\r\nBug.hs:1:1: error:\r\n • Ambiguous type variable ‘a0’ arising from a use of ‘==’\r\n prevents the constraint ‘(Eq a0)’ from being solved.\r\n Probable fix: use a type annotation to specify what ‘a0’ should be.\r\n These potential instances exist:\r\n instance Eq Ordering  Defined in ‘GHC.Classes’\r\n instance Eq Integer\r\n  Defined in ‘integergmp1.0.0.1:GHC.Integer.Type’\r\n instance Eq a => Eq (Maybe a)  Defined in ‘GHC.Base’\r\n ...plus 22 others\r\n ...plus 7 instances involving outofscope types\r\n (use fprintpotentialinstances to see them all)\r\n • When instantiating ‘f’, initially inferred to have\r\n this overlygeneral type:\r\n forall a. Eq a => a > a > Bool\r\n NB: This instantiation can be caused by the monomorphism restriction.\r\n}}}\r\n\r\nNotice the `NB: This instantiation can be caused by the monomorphism restriction` part. But in GHC 8.2.1, this advice has mysteriously vanished!\r\n\r\n{{{\r\nGHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Main ( Bug.hs, interpreted )\r\n\r\nBug.hs:1:5: error:\r\n • Ambiguous type variable ‘a0’ arising from a use of ‘==’\r\n prevents the constraint ‘(Eq a0)’ from being solved.\r\n Relevant bindings include\r\n f :: a0 > a0 > Bool (bound at Bug.hs:1:1)\r\n Probable fix: use a type annotation to specify what ‘a0’ should be.\r\n These potential instances exist:\r\n instance Eq Ordering  Defined in ‘GHC.Classes’\r\n instance Eq Integer\r\n  Defined in ‘integergmp1.0.1.0:GHC.Integer.Type’\r\n instance Eq a => Eq (Maybe a)  Defined in ‘GHC.Base’\r\n ...plus 22 others\r\n ...plus 9 instances involving outofscope types\r\n (use fprintpotentialinstances to see them all)\r\n • In the expression: (==)\r\n In an equation for ‘f’: f = (==)\r\n \r\n1  f = (==)\r\n  ^^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >This program doesn't typecheck due to the monomorphism restriction:
```hs
f = (==)
```
In GHC 8.0.2, the error message was quite helpful in informing you of this fact:
```
GHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main ( Bug.hs, interpreted )
Bug.hs:1:1: error:
• Ambiguous type variable ‘a0’ arising from a use of ‘==’
prevents the constraint ‘(Eq a0)’ from being solved.
Probable fix: use a type annotation to specify what ‘a0’ should be.
These potential instances exist:
instance Eq Ordering  Defined in ‘GHC.Classes’
instance Eq Integer
 Defined in ‘integergmp1.0.0.1:GHC.Integer.Type’
instance Eq a => Eq (Maybe a)  Defined in ‘GHC.Base’
...plus 22 others
...plus 7 instances involving outofscope types
(use fprintpotentialinstances to see them all)
• When instantiating ‘f’, initially inferred to have
this overlygeneral type:
forall a. Eq a => a > a > Bool
NB: This instantiation can be caused by the monomorphism restriction.
```
Notice the `NB: This instantiation can be caused by the monomorphism restriction` part. But in GHC 8.2.1, this advice has mysteriously vanished!
```
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main ( Bug.hs, interpreted )
Bug.hs:1:5: error:
• Ambiguous type variable ‘a0’ arising from a use of ‘==’
prevents the constraint ‘(Eq a0)’ from being solved.
Relevant bindings include
f :: a0 > a0 > Bool (bound at Bug.hs:1:1)
Probable fix: use a type annotation to specify what ‘a0’ should be.
These potential instances exist:
instance Eq Ordering  Defined in ‘GHC.Classes’
instance Eq Integer
 Defined in ‘integergmp1.0.1.0:GHC.Integer.Type’
instance Eq a => Eq (Maybe a)  Defined in ‘GHC.Base’
...plus 22 others
...plus 9 instances involving outofscope types
(use fprintpotentialinstances to see them all)
• In the expression: (==)
In an equation for ‘f’: f = (==)

1  f = (==)
 ^^^^
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"GHC 8.2.1 doesn't inform you when the monomorphism restriction kicks in anymore","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This program doesn't typecheck due to the monomorphism restriction:\r\n\r\n{{{#!hs\r\nf = (==)\r\n}}}\r\n\r\nIn GHC 8.0.2, the error message was quite helpful in informing you of this fact:\r\n\r\n{{{\r\nGHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Main ( Bug.hs, interpreted )\r\n\r\nBug.hs:1:1: error:\r\n • Ambiguous type variable ‘a0’ arising from a use of ‘==’\r\n prevents the constraint ‘(Eq a0)’ from being solved.\r\n Probable fix: use a type annotation to specify what ‘a0’ should be.\r\n These potential instances exist:\r\n instance Eq Ordering  Defined in ‘GHC.Classes’\r\n instance Eq Integer\r\n  Defined in ‘integergmp1.0.0.1:GHC.Integer.Type’\r\n instance Eq a => Eq (Maybe a)  Defined in ‘GHC.Base’\r\n ...plus 22 others\r\n ...plus 7 instances involving outofscope types\r\n (use fprintpotentialinstances to see them all)\r\n • When instantiating ‘f’, initially inferred to have\r\n this overlygeneral type:\r\n forall a. Eq a => a > a > Bool\r\n NB: This instantiation can be caused by the monomorphism restriction.\r\n}}}\r\n\r\nNotice the `NB: This instantiation can be caused by the monomorphism restriction` part. But in GHC 8.2.1, this advice has mysteriously vanished!\r\n\r\n{{{\r\nGHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Main ( Bug.hs, interpreted )\r\n\r\nBug.hs:1:5: error:\r\n • Ambiguous type variable ‘a0’ arising from a use of ‘==’\r\n prevents the constraint ‘(Eq a0)’ from being solved.\r\n Relevant bindings include\r\n f :: a0 > a0 > Bool (bound at Bug.hs:1:1)\r\n Probable fix: use a type annotation to specify what ‘a0’ should be.\r\n These potential instances exist:\r\n instance Eq Ordering  Defined in ‘GHC.Classes’\r\n instance Eq Integer\r\n  Defined in ‘integergmp1.0.1.0:GHC.Integer.Type’\r\n instance Eq a => Eq (Maybe a)  Defined in ‘GHC.Base’\r\n ...plus 22 others\r\n ...plus 9 instances involving outofscope types\r\n (use fprintpotentialinstances to see them all)\r\n • In the expression: (==)\r\n In an equation for ‘f’: f = (==)\r\n \r\n1  f = (==)\r\n  ^^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/14366Type family equation refuses to unify wildcard type patterns20190707T18:17:18ZRyan ScottType family equation refuses to unify wildcard type patternsThis typechecks:
```hs
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
import Data.Kind
import Data.Type.Equality
type family Cast (e :: a :~: b) (x :: a) :: b where
Cast Refl x = x
```
However, if you try to make the kinds `a` and `b` explicit arguments to `Cast`:
```hs
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
import Data.Kind
import Data.Type.Equality
type family Cast (a :: Type) (b :: Type) (e :: a :~: b) (x :: a) :: b where
Cast _ _ Refl x = x
```
Then GHC gets confused:
```
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/ryanglscott/.ghci
[1 of 1] Compiling Main ( Bug.hs, interpreted )
Bug.hs:9:12: error:
• Expected kind ‘_ :~: _1’, but ‘'Refl’ has kind ‘_ :~: _’
• In the third argument of ‘Cast’, namely ‘Refl’
In the type family declaration for ‘Cast’

9  Cast _ _ Refl x = x
 ^^^^
```
A workaround is to explicitly write out what should be inferred by the underscores:
```hs
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
import Data.Kind
import Data.Type.Equality
type family Cast (a :: Type) (b :: Type) (e :: a :~: b) (x :: a) :: b where
Cast a a Refl x = x
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Type family equation refuses to unify wildcard type patterns","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["TypeFamilies,","TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This typechecks:\r\n\r\n{{{#!hs\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeInType #}\r\n{# LANGUAGE TypeOperators #}\r\n\r\nimport Data.Kind\r\nimport Data.Type.Equality\r\n\r\ntype family Cast (e :: a :~: b) (x :: a) :: b where\r\n Cast Refl x = x\r\n}}}\r\n\r\nHowever, if you try to make the kinds `a` and `b` explicit arguments to `Cast`:\r\n\r\n{{{#!hs\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeInType #}\r\n{# LANGUAGE TypeOperators #}\r\n\r\nimport Data.Kind\r\nimport Data.Type.Equality\r\n\r\ntype family Cast (a :: Type) (b :: Type) (e :: a :~: b) (x :: a) :: b where\r\n Cast _ _ Refl x = x\r\n}}}\r\n\r\nThen GHC gets confused:\r\n\r\n{{{\r\nGHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/ryanglscott/.ghci\r\n[1 of 1] Compiling Main ( Bug.hs, interpreted )\r\n\r\nBug.hs:9:12: error:\r\n • Expected kind ‘_ :~: _1’, but ‘'Refl’ has kind ‘_ :~: _’\r\n • In the third argument of ‘Cast’, namely ‘Refl’\r\n In the type family declaration for ‘Cast’\r\n \r\n9  Cast _ _ Refl x = x\r\n  ^^^^\r\n}}}\r\n\r\nA workaround is to explicitly write out what should be inferred by the underscores:\r\n\r\n{{{#!hs\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeInType #}\r\n{# LANGUAGE TypeOperators #}\r\n\r\nimport Data.Kind\r\nimport Data.Type.Equality\r\n\r\ntype family Cast (a :: Type) (b :: Type) (e :: a :~: b) (x :: a) :: b where\r\n Cast a a Refl x = x\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >This typechecks:
```hs
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
import Data.Kind
import Data.Type.Equality
type family Cast (e :: a :~: b) (x :: a) :: b where
Cast Refl x = x
```
However, if you try to make the kinds `a` and `b` explicit arguments to `Cast`:
```hs
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
import Data.Kind
import Data.Type.Equality
type family Cast (a :: Type) (b :: Type) (e :: a :~: b) (x :: a) :: b where
Cast _ _ Refl x = x
```
Then GHC gets confused:
```
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/ryanglscott/.ghci
[1 of 1] Compiling Main ( Bug.hs, interpreted )
Bug.hs:9:12: error:
• Expected kind ‘_ :~: _1’, but ‘'Refl’ has kind ‘_ :~: _’
• In the third argument of ‘Cast’, namely ‘Refl’
In the type family declaration for ‘Cast’

9  Cast _ _ Refl x = x
 ^^^^
```
A workaround is to explicitly write out what should be inferred by the underscores:
```hs
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
import Data.Kind
import Data.Type.Equality
type family Cast (a :: Type) (b :: Type) (e :: a :~: b) (x :: a) :: b where
Cast a a Refl x = x
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Type family equation refuses to unify wildcard type patterns","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["TypeFamilies,","TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This typechecks:\r\n\r\n{{{#!hs\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeInType #}\r\n{# LANGUAGE TypeOperators #}\r\n\r\nimport Data.Kind\r\nimport Data.Type.Equality\r\n\r\ntype family Cast (e :: a :~: b) (x :: a) :: b where\r\n Cast Refl x = x\r\n}}}\r\n\r\nHowever, if you try to make the kinds `a` and `b` explicit arguments to `Cast`:\r\n\r\n{{{#!hs\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeInType #}\r\n{# LANGUAGE TypeOperators #}\r\n\r\nimport Data.Kind\r\nimport Data.Type.Equality\r\n\r\ntype family Cast (a :: Type) (b :: Type) (e :: a :~: b) (x :: a) :: b where\r\n Cast _ _ Refl x = x\r\n}}}\r\n\r\nThen GHC gets confused:\r\n\r\n{{{\r\nGHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/ryanglscott/.ghci\r\n[1 of 1] Compiling Main ( Bug.hs, interpreted )\r\n\r\nBug.hs:9:12: error:\r\n • Expected kind ‘_ :~: _1’, but ‘'Refl’ has kind ‘_ :~: _’\r\n • In the third argument of ‘Cast’, namely ‘Refl’\r\n In the type family declaration for ‘Cast’\r\n \r\n9  Cast _ _ Refl x = x\r\n  ^^^^\r\n}}}\r\n\r\nA workaround is to explicitly write out what should be inferred by the underscores:\r\n\r\n{{{#!hs\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeInType #}\r\n{# LANGUAGE TypeOperators #}\r\n\r\nimport Data.Kind\r\nimport Data.Type.Equality\r\n\r\ntype family Cast (a :: Type) (b :: Type) (e :: a :~: b) (x :: a) :: b where\r\n Cast a a Refl x = x\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >8.8.1https://gitlab.haskell.org/ghc/ghc//issues/14354Unexpected type inference behavior with XTypeApplications20190707T18:17:21ZmbwUnexpected type inference behavior with XTypeApplicationsIn the following snippet, type inference of the let bound identity function after applying a type unexpectedly fails:
```hs
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
[...]
*Main> :set XTypeApplications
*Main> :t id @Int
id @Int :: Int > Int
*Main> let the = id
*Main> :t the @Int
<interactive>:1:1: error:
• Cannot apply expression of type ‘a0 > a0’
to a visible type argument ‘Int’
• In the expression: the @Int
*Main> :t _ @Int
```
Note that it works with `id`, but not with `the`. I would expect to be able to write something like `the @Double 42`, for instance.
For completeness' sake and since I don't know if it is related or relevant, with GHC 8.0.2, a panic is easily triggered:
```hs
Prelude> :set XTypeApplications
Prelude> :t _ @Int
ghc: panic! (the 'impossible' happened)
(GHC version 8.0.2 for x86_64unknownlinux):
initTc: unsolved constraints
WC {wc_insol = [W] __a15d :: t_a15c[tau:3] (CHoleCan: _)}
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
```
This however does not happen with GHC 8.2.1.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Unexpected type inference behavior with XTypeApplications","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"In the following snippet, type inference of the let bound identity function after applying a type unexpectedly fails:\r\n\r\n{{{#!hs\r\nGHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help\r\n[...]\r\n*Main> :set XTypeApplications \r\n*Main> :t id @Int\r\nid @Int :: Int > Int\r\n*Main> let the = id\r\n*Main> :t the @Int\r\n\r\n<interactive>:1:1: error:\r\n • Cannot apply expression of type ‘a0 > a0’\r\n to a visible type argument ‘Int’\r\n • In the expression: the @Int\r\n*Main> :t _ @Int\r\n}}}\r\n\r\nNote that it works with `id`, but not with `the`. I would expect to be able to write something like `the @Double 42`, for instance.\r\n\r\nFor completeness' sake and since I don't know if it is related or relevant, with GHC 8.0.2, a panic is easily triggered:\r\n\r\n{{{#!hs\r\nPrelude> :set XTypeApplications \r\nPrelude> :t _ @Int\r\nghc: panic! (the 'impossible' happened)\r\n (GHC version 8.0.2 for x86_64unknownlinux):\r\n\tinitTc: unsolved constraints\r\n WC {wc_insol = [W] __a15d :: t_a15c[tau:3] (CHoleCan: _)}\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n}}}\r\n\r\nThis however does not happen with GHC 8.2.1.","type_of_failure":"OtherFailure","blocking":[]} >In the following snippet, type inference of the let bound identity function after applying a type unexpectedly fails:
```hs
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
[...]
*Main> :set XTypeApplications
*Main> :t id @Int
id @Int :: Int > Int
*Main> let the = id
*Main> :t the @Int
<interactive>:1:1: error:
• Cannot apply expression of type ‘a0 > a0’
to a visible type argument ‘Int’
• In the expression: the @Int
*Main> :t _ @Int
```
Note that it works with `id`, but not with `the`. I would expect to be able to write something like `the @Double 42`, for instance.
For completeness' sake and since I don't know if it is related or relevant, with GHC 8.0.2, a panic is easily triggered:
```hs
Prelude> :set XTypeApplications
Prelude> :t _ @Int
ghc: panic! (the 'impossible' happened)
(GHC version 8.0.2 for x86_64unknownlinux):
initTc: unsolved constraints
WC {wc_insol = [W] __a15d :: t_a15c[tau:3] (CHoleCan: _)}
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
```
This however does not happen with GHC 8.2.1.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Unexpected type inference behavior with XTypeApplications","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"In the following snippet, type inference of the let bound identity function after applying a type unexpectedly fails:\r\n\r\n{{{#!hs\r\nGHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help\r\n[...]\r\n*Main> :set XTypeApplications \r\n*Main> :t id @Int\r\nid @Int :: Int > Int\r\n*Main> let the = id\r\n*Main> :t the @Int\r\n\r\n<interactive>:1:1: error:\r\n • Cannot apply expression of type ‘a0 > a0’\r\n to a visible type argument ‘Int’\r\n • In the expression: the @Int\r\n*Main> :t _ @Int\r\n}}}\r\n\r\nNote that it works with `id`, but not with `the`. I would expect to be able to write something like `the @Double 42`, for instance.\r\n\r\nFor completeness' sake and since I don't know if it is related or relevant, with GHC 8.0.2, a panic is easily triggered:\r\n\r\n{{{#!hs\r\nPrelude> :set XTypeApplications \r\nPrelude> :t _ @Int\r\nghc: panic! (the 'impossible' happened)\r\n (GHC version 8.0.2 for x86_64unknownlinux):\r\n\tinitTc: unsolved constraints\r\n WC {wc_insol = [W] __a15d :: t_a15c[tau:3] (CHoleCan: _)}\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n}}}\r\n\r\nThis however does not happen with GHC 8.2.1.","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/14352Higherrank kind ascription oddities20190707T18:17:21ZRyan ScottHigherrank kind ascription odditiesGHC accepts these two definitions:
```hs
{# LANGUAGE RankNTypes #}
{# LANGUAGE TypeInType #}
module Bug where
import Data.Proxy
f :: forall (x :: forall a. a > Int). Proxy x
f = Proxy
g :: forall (x :: forall a. a > Int). Proxy (x :: forall b. b > Int)
g = Proxy
```
However, it does not accept this one, which (AFAICT) should be equivalent to the two above:
```hs
h :: forall x. Proxy (x :: forall b. b > Int)
h = Proxy
```
```
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:13:23: error:
• Expected kind ‘forall b. b > Int’, but ‘x’ has kind ‘k0’
• In the first argument of ‘Proxy’, namely
‘(x :: forall b. b > Int)’
In the type signature:
h :: forall x. Proxy (x :: forall b. b > Int)

13  h :: forall x. Proxy (x :: forall b. b > Int)
 ^
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Higherrank kind ascription oddities","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"GHC accepts these two definitions:\r\n\r\n{{{#!hs\r\n{# LANGUAGE RankNTypes #}\r\n{# LANGUAGE TypeInType #}\r\nmodule Bug where\r\n\r\nimport Data.Proxy\r\n\r\nf :: forall (x :: forall a. a > Int). Proxy x\r\nf = Proxy\r\n\r\ng :: forall (x :: forall a. a > Int). Proxy (x :: forall b. b > Int)\r\ng = Proxy\r\n}}}\r\n\r\nHowever, it does not accept this one, which (AFAICT) should be equivalent to the two above:\r\n\r\n{{{#!hs\r\nh :: forall x. Proxy (x :: forall b. b > Int)\r\nh = Proxy\r\n}}}\r\n\r\n{{{\r\nGHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\n\r\nBug.hs:13:23: error:\r\n • Expected kind ‘forall b. b > Int’, but ‘x’ has kind ‘k0’\r\n • In the first argument of ‘Proxy’, namely\r\n ‘(x :: forall b. b > Int)’\r\n In the type signature:\r\n h :: forall x. Proxy (x :: forall b. b > Int)\r\n \r\n13  h :: forall x. Proxy (x :: forall b. b > Int)\r\n  ^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >GHC accepts these two definitions:
```hs
{# LANGUAGE RankNTypes #}
{# LANGUAGE TypeInType #}
module Bug where
import Data.Proxy
f :: forall (x :: forall a. a > Int). Proxy x
f = Proxy
g :: forall (x :: forall a. a > Int). Proxy (x :: forall b. b > Int)
g = Proxy
```
However, it does not accept this one, which (AFAICT) should be equivalent to the two above:
```hs
h :: forall x. Proxy (x :: forall b. b > Int)
h = Proxy
```
```
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:13:23: error:
• Expected kind ‘forall b. b > Int’, but ‘x’ has kind ‘k0’
• In the first argument of ‘Proxy’, namely
‘(x :: forall b. b > Int)’
In the type signature:
h :: forall x. Proxy (x :: forall b. b > Int)

13  h :: forall x. Proxy (x :: forall b. b > Int)
 ^
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Higherrank kind ascription oddities","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"GHC accepts these two definitions:\r\n\r\n{{{#!hs\r\n{# LANGUAGE RankNTypes #}\r\n{# LANGUAGE TypeInType #}\r\nmodule Bug where\r\n\r\nimport Data.Proxy\r\n\r\nf :: forall (x :: forall a. a > Int). Proxy x\r\nf = Proxy\r\n\r\ng :: forall (x :: forall a. a > Int). Proxy (x :: forall b. b > Int)\r\ng = Proxy\r\n}}}\r\n\r\nHowever, it does not accept this one, which (AFAICT) should be equivalent to the two above:\r\n\r\n{{{#!hs\r\nh :: forall x. Proxy (x :: forall b. b > Int)\r\nh = Proxy\r\n}}}\r\n\r\n{{{\r\nGHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\n\r\nBug.hs:13:23: error:\r\n • Expected kind ‘forall b. b > Int’, but ‘x’ has kind ‘k0’\r\n • In the first argument of ‘Proxy’, namely\r\n ‘(x :: forall b. b > Int)’\r\n In the type signature:\r\n h :: forall x. Proxy (x :: forall b. b > Int)\r\n \r\n13  h :: forall x. Proxy (x :: forall b. b > Int)\r\n  ^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/14348Polykinded definitions silently introduce extra type arguments captured by T...20190707T18:17:22ZgallaisPolykinded definitions silently introduce extra type arguments captured by TypeApplicationsThe first type argument of a polykinded definition is not the one explicitly quantified over in the definition but rather the implicitly inserted kind.
This leads to the puzzling error message "Expected a type, but ‘a’ has kind ‘k’" when ghc actually expected a kind.
```haskell
{# LANGUAGE GADTs, PolyKinds, ScopedTypeVariables, TypeApplications #}
data EQ :: k > k > * where
Refl :: EQ a a
data Wrap (a :: k) = Wrap (EQ a a)
wrap :: forall (a :: k). Wrap a
wrap = Wrap @a Refl  fails
 wrap = Wrap @k @a Refl  works
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Polykinded definitions silently introduce extra type arguments captured by TypeApplications","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The first type argument of a polykinded definition is not the one explicitly quantified over in the definition but rather the implicitly inserted kind.\r\n\r\nThis leads to the puzzling error message \"Expected a type, but ‘a’ has kind ‘k’\" when ghc actually expected a kind.\r\n\r\n{{{#!haskell\r\n{# LANGUAGE GADTs, PolyKinds, ScopedTypeVariables, TypeApplications #}\r\n\r\ndata EQ :: k > k > * where\r\n Refl :: EQ a a\r\n\r\ndata Wrap (a :: k) = Wrap (EQ a a)\r\n\r\nwrap :: forall (a :: k). Wrap a\r\nwrap = Wrap @a Refl  fails\r\n wrap = Wrap @k @a Refl  works\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >The first type argument of a polykinded definition is not the one explicitly quantified over in the definition but rather the implicitly inserted kind.
This leads to the puzzling error message "Expected a type, but ‘a’ has kind ‘k’" when ghc actually expected a kind.
```haskell
{# LANGUAGE GADTs, PolyKinds, ScopedTypeVariables, TypeApplications #}
data EQ :: k > k > * where
Refl :: EQ a a
data Wrap (a :: k) = Wrap (EQ a a)
wrap :: forall (a :: k). Wrap a
wrap = Wrap @a Refl  fails
 wrap = Wrap @k @a Refl  works
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Polykinded definitions silently introduce extra type arguments captured by TypeApplications","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The first type argument of a polykinded definition is not the one explicitly quantified over in the definition but rather the implicitly inserted kind.\r\n\r\nThis leads to the puzzling error message \"Expected a type, but ‘a’ has kind ‘k’\" when ghc actually expected a kind.\r\n\r\n{{{#!haskell\r\n{# LANGUAGE GADTs, PolyKinds, ScopedTypeVariables, TypeApplications #}\r\n\r\ndata EQ :: k > k > * where\r\n Refl :: EQ a a\r\n\r\ndata Wrap (a :: k) = Wrap (EQ a a)\r\n\r\nwrap :: forall (a :: k). Wrap a\r\nwrap = Wrap @a Refl  fails\r\n wrap = Wrap @k @a Refl  works\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/14340Rename AND typecheck types before values20190707T18:17:24ZEdward Z. YangRename AND typecheck types before valuesIn a few cases, we get in trouble during renaming of values because we don't have access to information that would be computed during typechecking. Two examples of this:
 #13905  Here, we need to determine if a Name is a newtype constructor or data type constructor during renaming (desugaring of applicative do), which is not known until after typechecking
 #12088  Perhaps? We want to rename and typecheck instance declarations at the same time, since they can occur between the type declarations.
One nit: you can't compute SCCs until you rename. But if you just rename ALL of the types at once, then SCC them, that should be fine.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1 
 Type  Task 
 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":"Rename AND typecheck types before values","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Task","description":"In a few cases, we get in trouble during renaming of values because we don't have access to information that would be computed during typechecking. Two examples of this:\r\n\r\n* https://ghc.haskell.org/trac/ghc/ticket/13905  Here, we need to determine if a Name is a newtype constructor or data type constructor during renaming (desugaring of applicative do), which is not known until after typechecking\r\n\r\n* https://ghc.haskell.org/trac/ghc/ticket/12088  Perhaps? We want to rename and typecheck instance declarations at the same time, since they can occur between the type declarations.\r\n\r\nOne nit: you can't compute SCCs until you rename. But if you just rename ALL of the types at once, then SCC them, that should be fine.","type_of_failure":"OtherFailure","blocking":[]} >In a few cases, we get in trouble during renaming of values because we don't have access to information that would be computed during typechecking. Two examples of this:
 #13905  Here, we need to determine if a Name is a newtype constructor or data type constructor during renaming (desugaring of applicative do), which is not known until after typechecking
 #12088  Perhaps? We want to rename and typecheck instance declarations at the same time, since they can occur between the type declarations.
One nit: you can't compute SCCs until you rename. But if you just rename ALL of the types at once, then SCC them, that should be fine.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1 
 Type  Task 
 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":"Rename AND typecheck types before values","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Task","description":"In a few cases, we get in trouble during renaming of values because we don't have access to information that would be computed during typechecking. Two examples of this:\r\n\r\n* https://ghc.haskell.org/trac/ghc/ticket/13905  Here, we need to determine if a Name is a newtype constructor or data type constructor during renaming (desugaring of applicative do), which is not known until after typechecking\r\n\r\n* https://ghc.haskell.org/trac/ghc/ticket/12088  Perhaps? We want to rename and typecheck instance declarations at the same time, since they can occur between the type declarations.\r\n\r\nOne nit: you can't compute SCCs until you rename. But if you just rename ALL of the types at once, then SCC them, that should be fine.","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/14332Deriving clauses can have forall types20190707T18:17:26ZRyan ScottDeriving clauses can have forall typesI made a horrifying discovery today: GHC accepts this code!
```hs
{# LANGUAGE DeriveAnyClass #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE RankNTypes #}
{# OPTIONS_GHC ddumpderiv #}
module Bug1 where
class C a b
data D a = D deriving ((forall a. C a))
```
```
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug1 ( Bug.hs, interpreted )
==================== Derived instances ====================
Derived class instances:
instance Bug1.C a1 (Bug1.D a2) where
Derived type family instances:
Ok, 1 module loaded.
```
It gets even worse with this example:
```hs
{# LANGUAGE DeriveGeneric #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE TypeInType #}
{# OPTIONS_GHC ddumpderiv fprintexplicitkinds #}
module Bug1 where
import Data.Kind
import GHC.Generics
data Proxy (a :: k) = Proxy
deriving ((forall k. (Generic1 :: (k > Type) > Constraint)))
```
```
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug1 ( Bug.hs, interpreted )
==================== Derived instances ====================
Derived class instances:
instance GHC.Generics.Generic1 k (Bug1.Proxy k) where
GHC.Generics.from1 x_a3ip
= GHC.Generics.M1
(case x_a3ip of { Bug1.Proxy > GHC.Generics.M1 GHC.Generics.U1 })
GHC.Generics.to1 (GHC.Generics.M1 x_a3iq)
= case x_a3iq of {
(GHC.Generics.M1 GHC.Generics.U1) > Bug1.Proxy }
Derived type family instances:
type GHC.Generics.Rep1 k_a2mY (Bug1.Proxy k_a2mY) = GHC.Generics.D1
k_a2mY
('GHC.Generics.MetaData
"Proxy" "Bug1" "main" 'GHC.Types.False)
(GHC.Generics.C1
k_a2mY
('GHC.Generics.MetaCons
"Proxy"
'GHC.Generics.PrefixI
'GHC.Types.False)
(GHC.Generics.U1 k_a2mY))
Ok, 1 module loaded.
```
In this example, the `forall`'d `k` from the `deriving` clause is discarded and then unified with the `k` from `data Proxy (a :: k)`.
All of this is incredibly unsettling. We really shouldn't be allowing `forall` types in `deriving` clauses in the first place.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Deriving clauses can have forall types","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["deriving"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I made a horrifying discovery today: GHC accepts this code!\r\n\r\n{{{#!hs\r\n{# LANGUAGE DeriveAnyClass #}\r\n{# LANGUAGE MultiParamTypeClasses #}\r\n{# LANGUAGE RankNTypes #}\r\n{# OPTIONS_GHC ddumpderiv #}\r\nmodule Bug1 where\r\n\r\nclass C a b\r\n\r\ndata D a = D deriving ((forall a. C a))\r\n}}}\r\n{{{\r\nGHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug1 ( Bug.hs, interpreted )\r\n\r\n==================== Derived instances ====================\r\nDerived class instances:\r\n instance Bug1.C a1 (Bug1.D a2) where\r\n \r\n\r\nDerived type family instances:\r\n\r\n\r\nOk, 1 module loaded.\r\n}}}\r\n\r\nIt gets even worse with this example:\r\n\r\n{{{#!hs\r\n{# LANGUAGE DeriveGeneric #}\r\n{# LANGUAGE RankNTypes #}\r\n{# LANGUAGE TypeInType #}\r\n{# OPTIONS_GHC ddumpderiv fprintexplicitkinds #}\r\nmodule Bug1 where\r\n\r\nimport Data.Kind\r\nimport GHC.Generics\r\n\r\ndata Proxy (a :: k) = Proxy\r\n deriving ((forall k. (Generic1 :: (k > Type) > Constraint)))\r\n}}}\r\n{{{\r\nGHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug1 ( Bug.hs, interpreted )\r\n\r\n==================== Derived instances ====================\r\nDerived class instances:\r\n instance GHC.Generics.Generic1 k (Bug1.Proxy k) where\r\n GHC.Generics.from1 x_a3ip\r\n = GHC.Generics.M1\r\n (case x_a3ip of { Bug1.Proxy > GHC.Generics.M1 GHC.Generics.U1 })\r\n GHC.Generics.to1 (GHC.Generics.M1 x_a3iq)\r\n = case x_a3iq of {\r\n (GHC.Generics.M1 GHC.Generics.U1) > Bug1.Proxy }\r\n \r\n\r\nDerived type family instances:\r\n type GHC.Generics.Rep1 k_a2mY (Bug1.Proxy k_a2mY) = GHC.Generics.D1\r\n k_a2mY\r\n ('GHC.Generics.MetaData\r\n \"Proxy\" \"Bug1\" \"main\" 'GHC.Types.False)\r\n (GHC.Generics.C1\r\n k_a2mY\r\n ('GHC.Generics.MetaCons\r\n \"Proxy\"\r\n 'GHC.Generics.PrefixI\r\n 'GHC.Types.False)\r\n (GHC.Generics.U1 k_a2mY))\r\n\r\n\r\nOk, 1 module loaded.\r\n}}}\r\n\r\nIn this example, the `forall`'d `k` from the `deriving` clause is discarded and then unified with the `k` from `data Proxy (a :: k)`.\r\n\r\nAll of this is incredibly unsettling. We really shouldn't be allowing `forall` types in `deriving` clauses in the first place.","type_of_failure":"OtherFailure","blocking":[]} >I made a horrifying discovery today: GHC accepts this code!
```hs
{# LANGUAGE DeriveAnyClass #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE RankNTypes #}
{# OPTIONS_GHC ddumpderiv #}
module Bug1 where
class C a b
data D a = D deriving ((forall a. C a))
```
```
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug1 ( Bug.hs, interpreted )
==================== Derived instances ====================
Derived class instances:
instance Bug1.C a1 (Bug1.D a2) where
Derived type family instances:
Ok, 1 module loaded.
```
It gets even worse with this example:
```hs
{# LANGUAGE DeriveGeneric #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE TypeInType #}
{# OPTIONS_GHC ddumpderiv fprintexplicitkinds #}
module Bug1 where
import Data.Kind
import GHC.Generics
data Proxy (a :: k) = Proxy
deriving ((forall k. (Generic1 :: (k > Type) > Constraint)))
```
```
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug1 ( Bug.hs, interpreted )
==================== Derived instances ====================
Derived class instances:
instance GHC.Generics.Generic1 k (Bug1.Proxy k) where
GHC.Generics.from1 x_a3ip
= GHC.Generics.M1
(case x_a3ip of { Bug1.Proxy > GHC.Generics.M1 GHC.Generics.U1 })
GHC.Generics.to1 (GHC.Generics.M1 x_a3iq)
= case x_a3iq of {
(GHC.Generics.M1 GHC.Generics.U1) > Bug1.Proxy }
Derived type family instances:
type GHC.Generics.Rep1 k_a2mY (Bug1.Proxy k_a2mY) = GHC.Generics.D1
k_a2mY
('GHC.Generics.MetaData
"Proxy" "Bug1" "main" 'GHC.Types.False)
(GHC.Generics.C1
k_a2mY
('GHC.Generics.MetaCons
"Proxy"
'GHC.Generics.PrefixI
'GHC.Types.False)
(GHC.Generics.U1 k_a2mY))
Ok, 1 module loaded.
```
In this example, the `forall`'d `k` from the `deriving` clause is discarded and then unified with the `k` from `data Proxy (a :: k)`.
All of this is incredibly unsettling. We really shouldn't be allowing `forall` types in `deriving` clauses in the first place.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Deriving clauses can have forall types","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["deriving"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I made a horrifying discovery today: GHC accepts this code!\r\n\r\n{{{#!hs\r\n{# LANGUAGE DeriveAnyClass #}\r\n{# LANGUAGE MultiParamTypeClasses #}\r\n{# LANGUAGE RankNTypes #}\r\n{# OPTIONS_GHC ddumpderiv #}\r\nmodule Bug1 where\r\n\r\nclass C a b\r\n\r\ndata D a = D deriving ((forall a. C a))\r\n}}}\r\n{{{\r\nGHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug1 ( Bug.hs, interpreted )\r\n\r\n==================== Derived instances ====================\r\nDerived class instances:\r\n instance Bug1.C a1 (Bug1.D a2) where\r\n \r\n\r\nDerived type family instances:\r\n\r\n\r\nOk, 1 module loaded.\r\n}}}\r\n\r\nIt gets even worse with this example:\r\n\r\n{{{#!hs\r\n{# LANGUAGE DeriveGeneric #}\r\n{# LANGUAGE RankNTypes #}\r\n{# LANGUAGE TypeInType #}\r\n{# OPTIONS_GHC ddumpderiv fprintexplicitkinds #}\r\nmodule Bug1 where\r\n\r\nimport Data.Kind\r\nimport GHC.Generics\r\n\r\ndata Proxy (a :: k) = Proxy\r\n deriving ((forall k. (Generic1 :: (k > Type) > Constraint)))\r\n}}}\r\n{{{\r\nGHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug1 ( Bug.hs, interpreted )\r\n\r\n==================== Derived instances ====================\r\nDerived class instances:\r\n instance GHC.Generics.Generic1 k (Bug1.Proxy k) where\r\n GHC.Generics.from1 x_a3ip\r\n = GHC.Generics.M1\r\n (case x_a3ip of { Bug1.Proxy > GHC.Generics.M1 GHC.Generics.U1 })\r\n GHC.Generics.to1 (GHC.Generics.M1 x_a3iq)\r\n = case x_a3iq of {\r\n (GHC.Generics.M1 GHC.Generics.U1) > Bug1.Proxy }\r\n \r\n\r\nDerived type family instances:\r\n type GHC.Generics.Rep1 k_a2mY (Bug1.Proxy k_a2mY) = GHC.Generics.D1\r\n k_a2mY\r\n ('GHC.Generics.MetaData\r\n \"Proxy\" \"Bug1\" \"main\" 'GHC.Types.False)\r\n (GHC.Generics.C1\r\n k_a2mY\r\n ('GHC.Generics.MetaCons\r\n \"Proxy\"\r\n 'GHC.Generics.PrefixI\r\n 'GHC.Types.False)\r\n (GHC.Generics.U1 k_a2mY))\r\n\r\n\r\nOk, 1 module loaded.\r\n}}}\r\n\r\nIn this example, the `forall`'d `k` from the `deriving` clause is discarded and then unified with the `k` from `data Proxy (a :: k)`.\r\n\r\nAll of this is incredibly unsettling. We really shouldn't be allowing `forall` types in `deriving` clauses in the first place.","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/14331Overzealous freefloating kind check causes deriving clause to be rejected20200123T19:27:39ZRyan ScottOverzealous freefloating kind check causes deriving clause to be rejectedGHC rejects this program:
```hs
{# LANGUAGE DeriveAnyClass #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE PolyKinds #}
module Bug where
class C a b
data D = D deriving (C (a :: k))
```
```
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:8:1: error:
Kind variable ‘k’ is implicitly bound in datatype
‘D’, but does not appear as the kind of any
of its type variables. Perhaps you meant
to bind it (with TypeInType) explicitly somewhere?

8  data D = D deriving (C (a :: k))
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
But it really shouldn't, since it's quite possible to write the code that is should generate:
```hs
instance C (a :: k) D
```
Curiously, this does not appear to happen for data family instances, as this typechecks:
```hs
{# LANGUAGE DeriveAnyClass #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE TypeFamilies #}
module Bug where
class C a b
data family D1
data instance D1 = D1 deriving (C (a :: k))
class E where
data D2
instance E where
data D2 = D2 deriving (C (a :: k))
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Overzealous freefloating kind check causes deriving clause to be rejected","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["deriving"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"GHC rejects this program:\r\n\r\n{{{#!hs\r\n{# LANGUAGE DeriveAnyClass #}\r\n{# LANGUAGE MultiParamTypeClasses #}\r\n{# LANGUAGE PolyKinds #}\r\nmodule Bug where\r\n\r\nclass C a b\r\n\r\ndata D = D deriving (C (a :: k))\r\n}}}\r\n\r\n{{{\r\nGHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\n\r\nBug.hs:8:1: error:\r\n Kind variable ‘k’ is implicitly bound in datatype\r\n ‘D’, but does not appear as the kind of any\r\n of its type variables. Perhaps you meant\r\n to bind it (with TypeInType) explicitly somewhere?\r\n \r\n8  data D = D deriving (C (a :: k))\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nBut it really shouldn't, since it's quite possible to write the code that is should generate:\r\n\r\n{{{#!hs\r\ninstance C (a :: k) D\r\n}}}\r\n\r\nCuriously, this does not appear to happen for data family instances, as this typechecks:\r\n\r\n{{{#!hs\r\n{# LANGUAGE DeriveAnyClass #}\r\n{# LANGUAGE MultiParamTypeClasses #}\r\n{# LANGUAGE PolyKinds #}\r\n{# LANGUAGE TypeFamilies #}\r\nmodule Bug where\r\n\r\nclass C a b\r\n\r\ndata family D1\r\ndata instance D1 = D1 deriving (C (a :: k))\r\n\r\nclass E where\r\n data D2\r\n\r\ninstance E where\r\n data D2 = D2 deriving (C (a :: k))\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >GHC rejects this program:
```hs
{# LANGUAGE DeriveAnyClass #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE PolyKinds #}
module Bug where
class C a b
data D = D deriving (C (a :: k))
```
```
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:8:1: error:
Kind variable ‘k’ is implicitly bound in datatype
‘D’, but does not appear as the kind of any
of its type variables. Perhaps you meant
to bind it (with TypeInType) explicitly somewhere?

8  data D = D deriving (C (a :: k))
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
But it really shouldn't, since it's quite possible to write the code that is should generate:
```hs
instance C (a :: k) D
```
Curiously, this does not appear to happen for data family instances, as this typechecks:
```hs
{# LANGUAGE DeriveAnyClass #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE TypeFamilies #}
module Bug where
class C a b
data family D1
data instance D1 = D1 deriving (C (a :: k))
class E where
data D2
instance E where
data D2 = D2 deriving (C (a :: k))
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Overzealous freefloating kind check causes deriving clause to be rejected","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["deriving"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"GHC rejects this program:\r\n\r\n{{{#!hs\r\n{# LANGUAGE DeriveAnyClass #}\r\n{# LANGUAGE MultiParamTypeClasses #}\r\n{# LANGUAGE PolyKinds #}\r\nmodule Bug where\r\n\r\nclass C a b\r\n\r\ndata D = D deriving (C (a :: k))\r\n}}}\r\n\r\n{{{\r\nGHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\n\r\nBug.hs:8:1: error:\r\n Kind variable ‘k’ is implicitly bound in datatype\r\n ‘D’, but does not appear as the kind of any\r\n of its type variables. Perhaps you meant\r\n to bind it (with TypeInType) explicitly somewhere?\r\n \r\n8  data D = D deriving (C (a :: k))\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nBut it really shouldn't, since it's quite possible to write the code that is should generate:\r\n\r\n{{{#!hs\r\ninstance C (a :: k) D\r\n}}}\r\n\r\nCuriously, this does not appear to happen for data family instances, as this typechecks:\r\n\r\n{{{#!hs\r\n{# LANGUAGE DeriveAnyClass #}\r\n{# LANGUAGE MultiParamTypeClasses #}\r\n{# LANGUAGE PolyKinds #}\r\n{# LANGUAGE TypeFamilies #}\r\nmodule Bug where\r\n\r\nclass C a b\r\n\r\ndata family D1\r\ndata instance D1 = D1 deriving (C (a :: k))\r\n\r\nclass E where\r\n data D2\r\n\r\ninstance E where\r\n data D2 = D2 deriving (C (a :: k))\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/14327Type error in program caused by unrelated definition20190707T18:17:27ZAlexis KingType error in program caused by unrelated definition*Adapted from [this Stack Overflow question](https://stackoverflow.com/q/46595162/465378).*
The following program raises two type errors:
```hs
import Prelude hiding (readFile, writeFile)
import Control.Monad.Free
import Data.Functor.Sum
data FileSystemF a
= ReadFile FilePath (String > a)
 WriteFile FilePath String a
deriving (Functor)
data ConsoleF a
= WriteLine String a
deriving (Functor)
data CloudF a
= GetStackInfo String (String > a)
deriving (Functor)
type App = Free (Sum FileSystemF (Sum ConsoleF CloudF))
readFile :: FilePath > App String
readFile path = liftF (InL (ReadFile path id))
writeFile :: FilePath > String > App ()
writeFile path contents = liftF (InL (WriteFile path contents ()))
writeLine :: String > App ()
writeLine line = liftF (InR (WriteLine line ()))
```
```
/private/tmp/freesandbox/src/FreeSandbox.hs:26:27: error:
• Couldn't match type ‘ConsoleF’ with ‘Sum ConsoleF CloudF’
arising from a functional dependency between constraints:
‘MonadFree
(Sum FileSystemF (Sum ConsoleF CloudF))
(Free (Sum FileSystemF (Sum ConsoleF CloudF)))’
arising from a use of ‘liftF’ at src/FreeSandbox.hs:26:2766
‘MonadFree
(Sum FileSystemF ConsoleF)
(Free (Sum FileSystemF (Sum ConsoleF CloudF)))’
arising from a use of ‘liftF’ at src/FreeSandbox.hs:29:1848
• In the expression: liftF (InL (WriteFile path contents ()))
In an equation for ‘writeFile’:
writeFile path contents = liftF (InL (WriteFile path contents ()))

26  writeFile path contents = liftF (InL (WriteFile path contents ()))
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
/private/tmp/freesandbox/src/FreeSandbox.hs:29:18: error:
• Couldn't match type ‘Sum ConsoleF CloudF’ with ‘ConsoleF’
arising from a functional dependency between:
constraint ‘MonadFree
(Sum FileSystemF ConsoleF)
(Free (Sum FileSystemF (Sum ConsoleF CloudF)))’
arising from a use of ‘liftF’
instance ‘MonadFree f (Free f)’ at <no location info>
• In the expression: liftF (InR (WriteLine line ()))
In an equation for ‘writeLine’:
writeLine line = liftF (InR (WriteLine line ()))

29  writeLine line = liftF (InR (WriteLine line ()))
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
The second of the two errors (the one on line 29) makes sense—it’s an error I would expect (there is a missing use of `InL`). However, the first error seems incorrect, as the definition of `writeFile` is, in fact, welltyped. In fact, if the definition of `writeLine` is commented out, the program typechecks! It gets weirder: if the definition of `writeLine` is moved in between the definitions of `readFile` and `writeFile`, then the unexpected error is reported for the definition of *`readFile`*, and if `writeLine` is moved above both of them, then the error isn’t reported at all!
This implies that a welltyped function (`writeFile`) can actually become illtyped after the addition of an unrelated, illtyped definition (`writeLine`). That seems like a bug to me.
I was able to reproduce this issue on GHC 7.10.3, 8.0.2, and 8.2.1.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Type error in program caused by unrelated definition","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"''Adapted from [https://stackoverflow.com/q/46595162/465378 this Stack Overflow question].''\r\n\r\nThe following program raises two type errors:\r\n\r\n{{{#!hs\r\nimport Prelude hiding (readFile, writeFile)\r\nimport Control.Monad.Free\r\nimport Data.Functor.Sum\r\n\r\ndata FileSystemF a\r\n = ReadFile FilePath (String > a)\r\n  WriteFile FilePath String a\r\n deriving (Functor)\r\n\r\ndata ConsoleF a\r\n = WriteLine String a\r\n deriving (Functor)\r\n\r\ndata CloudF a\r\n = GetStackInfo String (String > a)\r\n deriving (Functor)\r\n\r\ntype App = Free (Sum FileSystemF (Sum ConsoleF CloudF))\r\n\r\nreadFile :: FilePath > App String\r\nreadFile path = liftF (InL (ReadFile path id))\r\n\r\nwriteFile :: FilePath > String > App ()\r\nwriteFile path contents = liftF (InL (WriteFile path contents ()))\r\n\r\nwriteLine :: String > App ()\r\nwriteLine line = liftF (InR (WriteLine line ()))\r\n}}}\r\n{{{\r\n/private/tmp/freesandbox/src/FreeSandbox.hs:26:27: error:\r\n • Couldn't match type ‘ConsoleF’ with ‘Sum ConsoleF CloudF’\r\n arising from a functional dependency between constraints:\r\n ‘MonadFree\r\n (Sum FileSystemF (Sum ConsoleF CloudF))\r\n (Free (Sum FileSystemF (Sum ConsoleF CloudF)))’\r\n arising from a use of ‘liftF’ at src/FreeSandbox.hs:26:2766\r\n ‘MonadFree\r\n (Sum FileSystemF ConsoleF)\r\n (Free (Sum FileSystemF (Sum ConsoleF CloudF)))’\r\n arising from a use of ‘liftF’ at src/FreeSandbox.hs:29:1848\r\n • In the expression: liftF (InL (WriteFile path contents ()))\r\n In an equation for ‘writeFile’:\r\n writeFile path contents = liftF (InL (WriteFile path contents ()))\r\n \r\n26  writeFile path contents = liftF (InL (WriteFile path contents ()))\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n\r\n/private/tmp/freesandbox/src/FreeSandbox.hs:29:18: error:\r\n • Couldn't match type ‘Sum ConsoleF CloudF’ with ‘ConsoleF’\r\n arising from a functional dependency between:\r\n constraint ‘MonadFree\r\n (Sum FileSystemF ConsoleF)\r\n (Free (Sum FileSystemF (Sum ConsoleF CloudF)))’\r\n arising from a use of ‘liftF’\r\n instance ‘MonadFree f (Free f)’ at <no location info>\r\n • In the expression: liftF (InR (WriteLine line ()))\r\n In an equation for ‘writeLine’:\r\n writeLine line = liftF (InR (WriteLine line ()))\r\n \r\n29  writeLine line = liftF (InR (WriteLine line ()))\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nThe second of the two errors (the one on line 29) makes sense—it’s an error I would expect (there is a missing use of `InL`). However, the first error seems incorrect, as the definition of `writeFile` is, in fact, welltyped. In fact, if the definition of `writeLine` is commented out, the program typechecks! It gets weirder: if the definition of `writeLine` is moved in between the definitions of `readFile` and `writeFile`, then the unexpected error is reported for the definition of ''`readFile`'', and if `writeLine` is moved above both of them, then the error isn’t reported at all!\r\n\r\nThis implies that a welltyped function (`writeFile`) can actually become illtyped after the addition of an unrelated, illtyped definition (`writeLine`). That seems like a bug to me.\r\n\r\nI was able to reproduce this issue on GHC 7.10.3, 8.0.2, and 8.2.1.","type_of_failure":"OtherFailure","blocking":[]} >*Adapted from [this Stack Overflow question](https://stackoverflow.com/q/46595162/465378).*
The following program raises two type errors:
```hs
import Prelude hiding (readFile, writeFile)
import Control.Monad.Free
import Data.Functor.Sum
data FileSystemF a
= ReadFile FilePath (String > a)
 WriteFile FilePath String a
deriving (Functor)
data ConsoleF a
= WriteLine String a
deriving (Functor)
data CloudF a
= GetStackInfo String (String > a)
deriving (Functor)
type App = Free (Sum FileSystemF (Sum ConsoleF CloudF))
readFile :: FilePath > App String
readFile path = liftF (InL (ReadFile path id))
writeFile :: FilePath > String > App ()
writeFile path contents = liftF (InL (WriteFile path contents ()))
writeLine :: String > App ()
writeLine line = liftF (InR (WriteLine line ()))
```
```
/private/tmp/freesandbox/src/FreeSandbox.hs:26:27: error:
• Couldn't match type ‘ConsoleF’ with ‘Sum ConsoleF CloudF’
arising from a functional dependency between constraints:
‘MonadFree
(Sum FileSystemF (Sum ConsoleF CloudF))
(Free (Sum FileSystemF (Sum ConsoleF CloudF)))’
arising from a use of ‘liftF’ at src/FreeSandbox.hs:26:2766
‘MonadFree
(Sum FileSystemF ConsoleF)
(Free (Sum FileSystemF (Sum ConsoleF CloudF)))’
arising from a use of ‘liftF’ at src/FreeSandbox.hs:29:1848
• In the expression: liftF (InL (WriteFile path contents ()))
In an equation for ‘writeFile’:
writeFile path contents = liftF (InL (WriteFile path contents ()))

26  writeFile path contents = liftF (InL (WriteFile path contents ()))
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
/private/tmp/freesandbox/src/FreeSandbox.hs:29:18: error:
• Couldn't match type ‘Sum ConsoleF CloudF’ with ‘ConsoleF’
arising from a functional dependency between:
constraint ‘MonadFree
(Sum FileSystemF ConsoleF)
(Free (Sum FileSystemF (Sum ConsoleF CloudF)))’
arising from a use of ‘liftF’
instance ‘MonadFree f (Free f)’ at <no location info>
• In the expression: liftF (InR (WriteLine line ()))
In an equation for ‘writeLine’:
writeLine line = liftF (InR (WriteLine line ()))

29  writeLine line = liftF (InR (WriteLine line ()))
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
The second of the two errors (the one on line 29) makes sense—it’s an error I would expect (there is a missing use of `InL`). However, the first error seems incorrect, as the definition of `writeFile` is, in fact, welltyped. In fact, if the definition of `writeLine` is commented out, the program typechecks! It gets weirder: if the definition of `writeLine` is moved in between the definitions of `readFile` and `writeFile`, then the unexpected error is reported for the definition of *`readFile`*, and if `writeLine` is moved above both of them, then the error isn’t reported at all!
This implies that a welltyped function (`writeFile`) can actually become illtyped after the addition of an unrelated, illtyped definition (`writeLine`). That seems like a bug to me.
I was able to reproduce this issue on GHC 7.10.3, 8.0.2, and 8.2.1.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Type error in program caused by unrelated definition","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"''Adapted from [https://stackoverflow.com/q/46595162/465378 this Stack Overflow question].''\r\n\r\nThe following program raises two type errors:\r\n\r\n{{{#!hs\r\nimport Prelude hiding (readFile, writeFile)\r\nimport Control.Monad.Free\r\nimport Data.Functor.Sum\r\n\r\ndata FileSystemF a\r\n = ReadFile FilePath (String > a)\r\n  WriteFile FilePath String a\r\n deriving (Functor)\r\n\r\ndata ConsoleF a\r\n = WriteLine String a\r\n deriving (Functor)\r\n\r\ndata CloudF a\r\n = GetStackInfo String (String > a)\r\n deriving (Functor)\r\n\r\ntype App = Free (Sum FileSystemF (Sum ConsoleF CloudF))\r\n\r\nreadFile :: FilePath > App String\r\nreadFile path = liftF (InL (ReadFile path id))\r\n\r\nwriteFile :: FilePath > String > App ()\r\nwriteFile path contents = liftF (InL (WriteFile path contents ()))\r\n\r\nwriteLine :: String > App ()\r\nwriteLine line = liftF (InR (WriteLine line ()))\r\n}}}\r\n{{{\r\n/private/tmp/freesandbox/src/FreeSandbox.hs:26:27: error:\r\n • Couldn't match type ‘ConsoleF’ with ‘Sum ConsoleF CloudF’\r\n arising from a functional dependency between constraints:\r\n ‘MonadFree\r\n (Sum FileSystemF (Sum ConsoleF CloudF))\r\n (Free (Sum FileSystemF (Sum ConsoleF CloudF)))’\r\n arising from a use of ‘liftF’ at src/FreeSandbox.hs:26:2766\r\n ‘MonadFree\r\n (Sum FileSystemF ConsoleF)\r\n (Free (Sum FileSystemF (Sum ConsoleF CloudF)))’\r\n arising from a use of ‘liftF’ at src/FreeSandbox.hs:29:1848\r\n • In the expression: liftF (InL (WriteFile path contents ()))\r\n In an equation for ‘writeFile’:\r\n writeFile path contents = liftF (InL (WriteFile path contents ()))\r\n \r\n26  writeFile path contents = liftF (InL (WriteFile path contents ()))\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n\r\n/private/tmp/freesandbox/src/FreeSandbox.hs:29:18: error:\r\n • Couldn't match type ‘Sum ConsoleF CloudF’ with ‘ConsoleF’\r\n arising from a functional dependency between:\r\n constraint ‘MonadFree\r\n (Sum FileSystemF ConsoleF)\r\n (Free (Sum FileSystemF (Sum ConsoleF CloudF)))’\r\n arising from a use of ‘liftF’\r\n instance ‘MonadFree f (Free f)’ at <no location info>\r\n • In the expression: liftF (InR (WriteLine line ()))\r\n In an equation for ‘writeLine’:\r\n writeLine line = liftF (InR (WriteLine line ()))\r\n \r\n29  writeLine line = liftF (InR (WriteLine line ()))\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nThe second of the two errors (the one on line 29) makes sense—it’s an error I would expect (there is a missing use of `InL`). However, the first error seems incorrect, as the definition of `writeFile` is, in fact, welltyped. In fact, if the definition of `writeLine` is commented out, the program typechecks! It gets weirder: if the definition of `writeLine` is moved in between the definitions of `readFile` and `writeFile`, then the unexpected error is reported for the definition of ''`readFile`'', and if `writeLine` is moved above both of them, then the error isn’t reported at all!\r\n\r\nThis implies that a welltyped function (`writeFile`) can actually become illtyped after the addition of an unrelated, illtyped definition (`writeLine`). That seems like a bug to me.\r\n\r\nI was able to reproduce this issue on GHC 7.10.3, 8.0.2, and 8.2.1.","type_of_failure":"OtherFailure","blocking":[]} >8.4.1https://gitlab.haskell.org/ghc/ghc//issues/14323Occurs check regressions in GHC 8.2.1 (and HEAD)20190707T18:17:28ZRyan ScottOccurs check regressions in GHC 8.2.1 (and HEAD)Inspired by adamse's comment at #14317\##14323, I've discovered some programs which behave differently on GHC 8.0.2, 8.2.1, and HEAD.

First, there's this program:
```hs
{# LANGUAGE GADTs #}
hm1 :: b ~ f b => b > f b
hm1 x = x
```
On GHC 8.0.2, this compiles (with a warning):
```
GHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main ( Bug.hs, interpreted )
Bug.hs:4:1: warning: [Woverlappingpatterns]
Pattern match is redundant
In an equation for ‘hm1’: hm1 x = ...
```
But on GHC 8.2.1, it errors:
```
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main ( Bug.hs, interpreted )
Bug.hs:4:9: error:
• Could not deduce: b ~ f b
from the context: b ~ f b
bound by the type signature for:
hm1 :: forall b (f :: * > *). b ~ f b => b > f b
at Bug.hs:3:126
‘b’ is a rigid type variable bound by
the type signature for:
hm1 :: forall b (f :: * > *). b ~ f b => b > f b
at Bug.hs:3:126
• In the expression: x
In an equation for ‘hm1’: hm1 x = x
• Relevant bindings include
x :: b (bound at Bug.hs:4:5)
hm1 :: b > f b (bound at Bug.hs:4:1)

4  hm1 x = x
 ^
```
And on GHC HEAD, it fails with a different error!
```
GHCi, version 8.3.20171004: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main ( Bug.hs, interpreted )
Bug.hs:4:9: error:
• Occurs check: cannot construct the infinite type: b ~ f b
• In the expression: x
In an equation for ‘hm1’: hm1 x = x
• Relevant bindings include
x :: b (bound at Bug.hs:4:5)
hm1 :: b > f b (bound at Bug.hs:4:1)

4  hm1 x = x
 ^
```
The same errors occur if you give `hm1` the type `hm1 :: b ~ f b => f b > b`.

What happens if you try `Coercible` instead of `(~)`? Consider this variant of the program above:
```hs
{# LANGUAGE GADTs #}
import Data.Coerce
hm2 :: Coercible b (f b) => b > f b
hm2 = coerce
```
On GHC 8.0.2, 8.2.1, and HEAD, this compiles (without warnings). Good. But if you change the type to use the symmetric version of that constraint:
```hs
{# LANGUAGE GADTs #}
import Data.Coerce
hm3 :: Coercible (f b) b => b > f b
hm3 = coerce
```
Then on GHC 8.0.2, it compiles without warnings, but on 8.2.1 and HEAD it fails!
Here is the error with 8.2.1:
```
Bug3.hs:6:7: error:
• Could not deduce: Coercible b (f b)
arising from a use of ‘coerce’
from the context: Coercible (f b) b
bound by the type signature for:
hm3 :: forall (f :: * > *) b. Coercible (f b) b => b > f b
at Bug3.hs:5:136
‘b’ is a rigid type variable bound by
the type signature for:
hm3 :: forall (f :: * > *) b. Coercible (f b) b => b > f b
at Bug3.hs:5:136
• In the expression: coerce
In an equation for ‘hm3’: hm3 = coerce
• Relevant bindings include hm3 :: b > f b (bound at Bug3.hs:6:1)

6  hm3 = coerce
 ^^^^^^
```
And on HEAD:
```
Bug3.hs:6:7: error:
• Occurs check: cannot construct the infinite type: b ~ f b
arising from a use of ‘coerce’
• In the expression: coerce
In an equation for ‘hm3’: hm3 = coerce
• Relevant bindings include hm3 :: b > f b (bound at Bug3.hs:6:1)

6  hm3 = coerce
 ^^^^^^
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Occurs check regressions in GHC 8.2.1 (and HEAD)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Inspired by adamse's comment at https://ghc.haskell.org/trac/ghc/ticket/14317#comment:3, I've discovered some programs which behave differently on GHC 8.0.2, 8.2.1, and HEAD.\r\n\r\n\r\n\r\nFirst, there's this program:\r\n\r\n{{{#!hs\r\n{# LANGUAGE GADTs #}\r\n\r\nhm1 :: b ~ f b => b > f b\r\nhm1 x = x\r\n}}}\r\n\r\nOn GHC 8.0.2, this compiles (with a warning):\r\n\r\n{{{\r\nGHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Main ( Bug.hs, interpreted )\r\n\r\nBug.hs:4:1: warning: [Woverlappingpatterns]\r\n Pattern match is redundant\r\n In an equation for ‘hm1’: hm1 x = ...\r\n}}}\r\n\r\nBut on GHC 8.2.1, it errors:\r\n\r\n{{{\r\nGHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Main ( Bug.hs, interpreted )\r\n\r\nBug.hs:4:9: error:\r\n • Could not deduce: b ~ f b\r\n from the context: b ~ f b\r\n bound by the type signature for:\r\n hm1 :: forall b (f :: * > *). b ~ f b => b > f b\r\n at Bug.hs:3:126\r\n ‘b’ is a rigid type variable bound by\r\n the type signature for:\r\n hm1 :: forall b (f :: * > *). b ~ f b => b > f b\r\n at Bug.hs:3:126\r\n • In the expression: x\r\n In an equation for ‘hm1’: hm1 x = x\r\n • Relevant bindings include\r\n x :: b (bound at Bug.hs:4:5)\r\n hm1 :: b > f b (bound at Bug.hs:4:1)\r\n \r\n4  hm1 x = x\r\n  ^\r\n}}}\r\n\r\nAnd on GHC HEAD, it fails with a different error!\r\n\r\n{{{\r\nGHCi, version 8.3.20171004: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Main ( Bug.hs, interpreted )\r\n\r\nBug.hs:4:9: error:\r\n • Occurs check: cannot construct the infinite type: b ~ f b\r\n • In the expression: x\r\n In an equation for ‘hm1’: hm1 x = x\r\n • Relevant bindings include\r\n x :: b (bound at Bug.hs:4:5)\r\n hm1 :: b > f b (bound at Bug.hs:4:1)\r\n \r\n4  hm1 x = x\r\n  ^\r\n}}}\r\n\r\nThe same errors occur if you give `hm1` the type `hm1 :: b ~ f b => f b > b`.\r\n\r\n\r\n\r\nWhat happens if you try `Coercible` instead of `(~)`? Consider this variant of the program above:\r\n\r\n{{{#!hs\r\n{# LANGUAGE GADTs #}\r\n\r\nimport Data.Coerce\r\n\r\nhm2 :: Coercible b (f b) => b > f b\r\nhm2 = coerce\r\n}}}\r\n\r\nOn GHC 8.0.2, 8.2.1, and HEAD, this compiles (without warnings). Good. But if you change the type to use the symmetric version of that constraint:\r\n\r\n{{{#!hs\r\n{# LANGUAGE GADTs #}\r\n\r\nimport Data.Coerce\r\n\r\nhm3 :: Coercible (f b) b => b > f b\r\nhm3 = coerce\r\n}}}\r\n\r\nThen on GHC 8.0.2, it compiles without warnings, but on 8.2.1 and HEAD it fails!\r\n\r\nHere is the error with 8.2.1:\r\n\r\n{{{\r\nBug3.hs:6:7: error:\r\n • Could not deduce: Coercible b (f b)\r\n arising from a use of ‘coerce’\r\n from the context: Coercible (f b) b\r\n bound by the type signature for:\r\n hm3 :: forall (f :: * > *) b. Coercible (f b) b => b > f b\r\n at Bug3.hs:5:136\r\n ‘b’ is a rigid type variable bound by\r\n the type signature for:\r\n hm3 :: forall (f :: * > *) b. Coercible (f b) b => b > f b\r\n at Bug3.hs:5:136\r\n • In the expression: coerce\r\n In an equation for ‘hm3’: hm3 = coerce\r\n • Relevant bindings include hm3 :: b > f b (bound at Bug3.hs:6:1)\r\n \r\n6  hm3 = coerce\r\n  ^^^^^^\r\n}}}\r\n\r\nAnd on HEAD:\r\n\r\n{{{\r\nBug3.hs:6:7: error:\r\n • Occurs check: cannot construct the infinite type: b ~ f b\r\n arising from a use of ‘coerce’\r\n • In the expression: coerce\r\n In an equation for ‘hm3’: hm3 = coerce\r\n • Relevant bindings include hm3 :: b > f b (bound at Bug3.hs:6:1)\r\n \r\n6  hm3 = coerce\r\n  ^^^^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >Inspired by adamse's comment at #14317\##14323, I've discovered some programs which behave differently on GHC 8.0.2, 8.2.1, and HEAD.

First, there's this program:
```hs
{# LANGUAGE GADTs #}
hm1 :: b ~ f b => b > f b
hm1 x = x
```
On GHC 8.0.2, this compiles (with a warning):
```
GHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main ( Bug.hs, interpreted )
Bug.hs:4:1: warning: [Woverlappingpatterns]
Pattern match is redundant
In an equation for ‘hm1’: hm1 x = ...
```
But on GHC 8.2.1, it errors:
```
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main ( Bug.hs, interpreted )
Bug.hs:4:9: error:
• Could not deduce: b ~ f b
from the context: b ~ f b
bound by the type signature for:
hm1 :: forall b (f :: * > *). b ~ f b => b > f b
at Bug.hs:3:126
‘b’ is a rigid type variable bound by
the type signature for:
hm1 :: forall b (f :: * > *). b ~ f b => b > f b
at Bug.hs:3:126
• In the expression: x
In an equation for ‘hm1’: hm1 x = x
• Relevant bindings include
x :: b (bound at Bug.hs:4:5)
hm1 :: b > f b (bound at Bug.hs:4:1)

4  hm1 x = x
 ^
```
And on GHC HEAD, it fails with a different error!
```
GHCi, version 8.3.20171004: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main ( Bug.hs, interpreted )
Bug.hs:4:9: error:
• Occurs check: cannot construct the infinite type: b ~ f b
• In the expression: x
In an equation for ‘hm1’: hm1 x = x
• Relevant bindings include
x :: b (bound at Bug.hs:4:5)
hm1 :: b > f b (bound at Bug.hs:4:1)

4  hm1 x = x
 ^
```
The same errors occur if you give `hm1` the type `hm1 :: b ~ f b => f b > b`.

What happens if you try `Coercible` instead of `(~)`? Consider this variant of the program above:
```hs
{# LANGUAGE GADTs #}
import Data.Coerce
hm2 :: Coercible b (f b) => b > f b
hm2 = coerce
```
On GHC 8.0.2, 8.2.1, and HEAD, this compiles (without warnings). Good. But if you change the type to use the symmetric version of that constraint:
```hs
{# LANGUAGE GADTs #}
import Data.Coerce
hm3 :: Coercible (f b) b => b > f b
hm3 = coerce
```
Then on GHC 8.0.2, it compiles without warnings, but on 8.2.1 and HEAD it fails!
Here is the error with 8.2.1:
```
Bug3.hs:6:7: error:
• Could not deduce: Coercible b (f b)
arising from a use of ‘coerce’
from the context: Coercible (f b) b
bound by the type signature for:
hm3 :: forall (f :: * > *) b. Coercible (f b) b => b > f b
at Bug3.hs:5:136
‘b’ is a rigid type variable bound by
the type signature for:
hm3 :: forall (f :: * > *) b. Coercible (f b) b => b > f b
at Bug3.hs:5:136
• In the expression: coerce
In an equation for ‘hm3’: hm3 = coerce
• Relevant bindings include hm3 :: b > f b (bound at Bug3.hs:6:1)

6  hm3 = coerce
 ^^^^^^
```
And on HEAD:
```
Bug3.hs:6:7: error:
• Occurs check: cannot construct the infinite type: b ~ f b
arising from a use of ‘coerce’
• In the expression: coerce
In an equation for ‘hm3’: hm3 = coerce
• Relevant bindings include hm3 :: b > f b (bound at Bug3.hs:6:1)

6  hm3 = coerce
 ^^^^^^
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Occurs check regressions in GHC 8.2.1 (and HEAD)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Inspired by adamse's comment at https://ghc.haskell.org/trac/ghc/ticket/14317#comment:3, I've discovered some programs which behave differently on GHC 8.0.2, 8.2.1, and HEAD.\r\n\r\n\r\n\r\nFirst, there's this program:\r\n\r\n{{{#!hs\r\n{# LANGUAGE GADTs #}\r\n\r\nhm1 :: b ~ f b => b > f b\r\nhm1 x = x\r\n}}}\r\n\r\nOn GHC 8.0.2, this compiles (with a warning):\r\n\r\n{{{\r\nGHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Main ( Bug.hs, interpreted )\r\n\r\nBug.hs:4:1: warning: [Woverlappingpatterns]\r\n Pattern match is redundant\r\n In an equation for ‘hm1’: hm1 x = ...\r\n}}}\r\n\r\nBut on GHC 8.2.1, it errors:\r\n\r\n{{{\r\nGHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Main ( Bug.hs, interpreted )\r\n\r\nBug.hs:4:9: error:\r\n • Could not deduce: b ~ f b\r\n from the context: b ~ f b\r\n bound by the type signature for:\r\n hm1 :: forall b (f :: * > *). b ~ f b => b > f b\r\n at Bug.hs:3:126\r\n ‘b’ is a rigid type variable bound by\r\n the type signature for:\r\n hm1 :: forall b (f :: * > *). b ~ f b => b > f b\r\n at Bug.hs:3:126\r\n • In the expression: x\r\n In an equation for ‘hm1’: hm1 x = x\r\n • Relevant bindings include\r\n x :: b (bound at Bug.hs:4:5)\r\n hm1 :: b > f b (bound at Bug.hs:4:1)\r\n \r\n4  hm1 x = x\r\n  ^\r\n}}}\r\n\r\nAnd on GHC HEAD, it fails with a different error!\r\n\r\n{{{\r\nGHCi, version 8.3.20171004: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Main ( Bug.hs, interpreted )\r\n\r\nBug.hs:4:9: error:\r\n • Occurs check: cannot construct the infinite type: b ~ f b\r\n • In the expression: x\r\n In an equation for ‘hm1’: hm1 x = x\r\n • Relevant bindings include\r\n x :: b (bound at Bug.hs:4:5)\r\n hm1 :: b > f b (bound at Bug.hs:4:1)\r\n \r\n4  hm1 x = x\r\n  ^\r\n}}}\r\n\r\nThe same errors occur if you give `hm1` the type `hm1 :: b ~ f b => f b > b`.\r\n\r\n\r\n\r\nWhat happens if you try `Coercible` instead of `(~)`? Consider this variant of the program above:\r\n\r\n{{{#!hs\r\n{# LANGUAGE GADTs #}\r\n\r\nimport Data.Coerce\r\n\r\nhm2 :: Coercible b (f b) => b > f b\r\nhm2 = coerce\r\n}}}\r\n\r\nOn GHC 8.0.2, 8.2.1, and HEAD, this compiles (without warnings). Good. But if you change the type to use the symmetric version of that constraint:\r\n\r\n{{{#!hs\r\n{# LANGUAGE GADTs #}\r\n\r\nimport Data.Coerce\r\n\r\nhm3 :: Coercible (f b) b => b > f b\r\nhm3 = coerce\r\n}}}\r\n\r\nThen on GHC 8.0.2, it compiles without warnings, but on 8.2.1 and HEAD it fails!\r\n\r\nHere is the error with 8.2.1:\r\n\r\n{{{\r\nBug3.hs:6:7: error:\r\n • Could not deduce: Coercible b (f b)\r\n arising from a use of ‘coerce’\r\n from the context: Coercible (f b) b\r\n bound by the type signature for:\r\n hm3 :: forall (f :: * > *) b. Coercible (f b) b => b > f b\r\n at Bug3.hs:5:136\r\n ‘b’ is a rigid type variable bound by\r\n the type signature for:\r\n hm3 :: forall (f :: * > *) b. Coercible (f b) b => b > f b\r\n at Bug3.hs:5:136\r\n • In the expression: coerce\r\n In an equation for ‘hm3’: hm3 = coerce\r\n • Relevant bindings include hm3 :: b > f b (bound at Bug3.hs:6:1)\r\n \r\n6  hm3 = coerce\r\n  ^^^^^^\r\n}}}\r\n\r\nAnd on HEAD:\r\n\r\n{{{\r\nBug3.hs:6:7: error:\r\n • Occurs check: cannot construct the infinite type: b ~ f b\r\n arising from a use of ‘coerce’\r\n • In the expression: coerce\r\n In an equation for ‘hm3’: hm3 = coerce\r\n • Relevant bindings include hm3 :: b > f b (bound at Bug3.hs:6:1)\r\n \r\n6  hm3 = coerce\r\n  ^^^^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >8.4.1https://gitlab.haskell.org/ghc/ghc//issues/14322Simplifying an instance context makes a rewrite rule no longer typecheck20190707T18:17:29ZRyan ScottSimplifying an instance context makes a rewrite rule no longer typecheckThis code (taken from the `reducers` package) compiles:
```hs
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE MultiParamTypeClasses #}
import Prelude (Applicative(..), Functor(..), (.))
class Semigroup m where
(<>) :: m > m > m
class Semigroup m => Reducer c m where
snoc :: m > c > m
newtype Traversal f = Traversal { getTraversal :: f () }
instance Applicative f => Semigroup (Traversal f) where
Traversal a <> Traversal b = Traversal (a *> b)
instance Applicative f => Reducer (f a) (Traversal f) where
Traversal a `snoc` b = Traversal (() <$ (a *> b))
snocTraversal :: Reducer (f ()) (Traversal f) => Traversal f > f () > Traversal f
snocTraversal a = (<>) a . Traversal
{# RULES "snocTraversal" snoc = snocTraversal #}
```
But on GHC 8.2.1 and later, it gives this warning:
```
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main ( Bug.hs, interpreted )
Bug.hs:21:18: warning: [Wsimplifiableclassconstraints]
• The constraint ‘Reducer (f ()) (Traversal f)’
matches an instance declaration
instance Applicative f => Reducer (f a) (Traversal f)
 Defined at Bug.hs:18:10
This makes type inference for inner bindings fragile;
either use MonoLocalBinds, or simplify it using the instance
• In the type signature:
snocTraversal :: Reducer (f ()) (Traversal f) =>
Traversal f > f () > Traversal f

21  snocTraversal :: Reducer (f ()) (Traversal f) => Traversal f > f () > Traversal f
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
I decided to follow GHC's orders and reduce the `Reducer (f ()) (Traversal f)` context to just `Applicative f`:
```hs
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE MultiParamTypeClasses #}
import Prelude (Applicative(..), Functor(..), (.))
class Semigroup m where
(<>) :: m > m > m
class Semigroup m => Reducer c m where
snoc :: m > c > m
newtype Traversal f = Traversal { getTraversal :: f () }
instance Applicative f => Semigroup (Traversal f) where
Traversal a <> Traversal b = Traversal (a *> b)
instance Applicative f => Reducer (f a) (Traversal f) where
Traversal a `snoc` b = Traversal (() <$ (a *> b))
snocTraversal :: Applicative f => Traversal f > f () > Traversal f
snocTraversal a = (<>) a . Traversal
{# RULES "snocTraversal" snoc = snocTraversal #}
```
But after doing so, the file no longer typechecks!
```
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main ( Bug.hs, interpreted )
Bug.hs:23:34: error:
• Could not deduce (Applicative f)
arising from a use of ‘snocTraversal’
from the context: Reducer (f ()) (Traversal f)
bound by the RULE "snocTraversal" at Bug.hs:23:1146
Possible fix:
add (Applicative f) to the context of the RULE "snocTraversal"
• In the expression: snocTraversal
When checking the transformation rule "snocTraversal"

23  {# RULES "snocTraversal" snoc = snocTraversal #}
 ^^^^^^^^^^^^^
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Simplifying an instance context makes a rewrite rule no longer typecheck","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This code (taken from the `reducers` package) compiles:\r\n\r\n{{{#!hs\r\n{# LANGUAGE FlexibleContexts #}\r\n{# LANGUAGE FlexibleInstances #}\r\n{# LANGUAGE MultiParamTypeClasses #}\r\n\r\nimport Prelude (Applicative(..), Functor(..), (.))\r\n\r\nclass Semigroup m where\r\n (<>) :: m > m > m\r\n\r\nclass Semigroup m => Reducer c m where\r\n snoc :: m > c > m\r\n\r\nnewtype Traversal f = Traversal { getTraversal :: f () }\r\n\r\ninstance Applicative f => Semigroup (Traversal f) where\r\n Traversal a <> Traversal b = Traversal (a *> b)\r\n\r\ninstance Applicative f => Reducer (f a) (Traversal f) where\r\n Traversal a `snoc` b = Traversal (() <$ (a *> b))\r\n\r\nsnocTraversal :: Reducer (f ()) (Traversal f) => Traversal f > f () > Traversal f\r\nsnocTraversal a = (<>) a . Traversal\r\n{# RULES \"snocTraversal\" snoc = snocTraversal #}\r\n}}}\r\n\r\nBut on GHC 8.2.1 and later, it gives this warning:\r\n\r\n{{{\r\nGHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Main ( Bug.hs, interpreted )\r\n\r\nBug.hs:21:18: warning: [Wsimplifiableclassconstraints]\r\n • The constraint ‘Reducer (f ()) (Traversal f)’\r\n matches an instance declaration\r\n instance Applicative f => Reducer (f a) (Traversal f)\r\n  Defined at Bug.hs:18:10\r\n This makes type inference for inner bindings fragile;\r\n either use MonoLocalBinds, or simplify it using the instance\r\n • In the type signature:\r\n snocTraversal :: Reducer (f ()) (Traversal f) =>\r\n Traversal f > f () > Traversal f\r\n \r\n21  snocTraversal :: Reducer (f ()) (Traversal f) => Traversal f > f () > Traversal f\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nI decided to follow GHC's orders and reduce the `Reducer (f ()) (Traversal f)` context to just `Applicative f`:\r\n\r\n{{{#!hs\r\n{# LANGUAGE FlexibleContexts #}\r\n{# LANGUAGE FlexibleInstances #}\r\n{# LANGUAGE MultiParamTypeClasses #}\r\n\r\nimport Prelude (Applicative(..), Functor(..), (.))\r\n\r\nclass Semigroup m where\r\n (<>) :: m > m > m\r\n\r\nclass Semigroup m => Reducer c m where\r\n snoc :: m > c > m\r\n\r\nnewtype Traversal f = Traversal { getTraversal :: f () }\r\n\r\ninstance Applicative f => Semigroup (Traversal f) where\r\n Traversal a <> Traversal b = Traversal (a *> b)\r\n\r\ninstance Applicative f => Reducer (f a) (Traversal f) where\r\n Traversal a `snoc` b = Traversal (() <$ (a *> b))\r\n\r\nsnocTraversal :: Applicative f => Traversal f > f () > Traversal f\r\nsnocTraversal a = (<>) a . Traversal\r\n{# RULES \"snocTraversal\" snoc = snocTraversal #}\r\n}}}\r\n\r\nBut after doing so, the file no longer typechecks!\r\n\r\n{{{\r\nGHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Main ( Bug.hs, interpreted )\r\n\r\nBug.hs:23:34: error:\r\n • Could not deduce (Applicative f)\r\n arising from a use of ‘snocTraversal’\r\n from the context: Reducer (f ()) (Traversal f)\r\n bound by the RULE \"snocTraversal\" at Bug.hs:23:1146\r\n Possible fix:\r\n add (Applicative f) to the context of the RULE \"snocTraversal\"\r\n • In the expression: snocTraversal\r\n When checking the transformation rule \"snocTraversal\"\r\n \r\n23  {# RULES \"snocTraversal\" snoc = snocTraversal #}\r\n  ^^^^^^^^^^^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >This code (taken from the `reducers` package) compiles:
```hs
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE MultiParamTypeClasses #}
import Prelude (Applicative(..), Functor(..), (.))
class Semigroup m where
(<>) :: m > m > m
class Semigroup m => Reducer c m where
snoc :: m > c > m
newtype Traversal f = Traversal { getTraversal :: f () }
instance Applicative f => Semigroup (Traversal f) where
Traversal a <> Traversal b = Traversal (a *> b)
instance Applicative f => Reducer (f a) (Traversal f) where
Traversal a `snoc` b = Traversal (() <$ (a *> b))
snocTraversal :: Reducer (f ()) (Traversal f) => Traversal f > f () > Traversal f
snocTraversal a = (<>) a . Traversal
{# RULES "snocTraversal" snoc = snocTraversal #}
```
But on GHC 8.2.1 and later, it gives this warning:
```
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main ( Bug.hs, interpreted )
Bug.hs:21:18: warning: [Wsimplifiableclassconstraints]
• The constraint ‘Reducer (f ()) (Traversal f)’
matches an instance declaration
instance Applicative f => Reducer (f a) (Traversal f)
 Defined at Bug.hs:18:10
This makes type inference for inner bindings fragile;
either use MonoLocalBinds, or simplify it using the instance
• In the type signature:
snocTraversal :: Reducer (f ()) (Traversal f) =>
Traversal f > f () > Traversal f

21  snocTraversal :: Reducer (f ()) (Traversal f) => Traversal f > f () > Traversal f
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
I decided to follow GHC's orders and reduce the `Reducer (f ()) (Traversal f)` context to just `Applicative f`:
```hs
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE MultiParamTypeClasses #}
import Prelude (Applicative(..), Functor(..), (.))
class Semigroup m where
(<>) :: m > m > m
class Semigroup m => Reducer c m where
snoc :: m > c > m
newtype Traversal f = Traversal { getTraversal :: f () }
instance Applicative f => Semigroup (Traversal f) where
Traversal a <> Traversal b = Traversal (a *> b)
instance Applicative f => Reducer (f a) (Traversal f) where
Traversal a `snoc` b = Traversal (() <$ (a *> b))
snocTraversal :: Applicative f => Traversal f > f () > Traversal f
snocTraversal a = (<>) a . Traversal
{# RULES "snocTraversal" snoc = snocTraversal #}
```
But after doing so, the file no longer typechecks!
```
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main ( Bug.hs, interpreted )
Bug.hs:23:34: error:
• Could not deduce (Applicative f)
arising from a use of ‘snocTraversal’
from the context: Reducer (f ()) (Traversal f)
bound by the RULE "snocTraversal" at Bug.hs:23:1146
Possible fix:
add (Applicative f) to the context of the RULE "snocTraversal"
• In the expression: snocTraversal
When checking the transformation rule "snocTraversal"

23  {# RULES "snocTraversal" snoc = snocTraversal #}
 ^^^^^^^^^^^^^
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Simplifying an instance context makes a rewrite rule no longer typecheck","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This code (taken from the `reducers` package) compiles:\r\n\r\n{{{#!hs\r\n{# LANGUAGE FlexibleContexts #}\r\n{# LANGUAGE FlexibleInstances #}\r\n{# LANGUAGE MultiParamTypeClasses #}\r\n\r\nimport Prelude (Applicative(..), Functor(..), (.))\r\n\r\nclass Semigroup m where\r\n (<>) :: m > m > m\r\n\r\nclass Semigroup m => Reducer c m where\r\n snoc :: m > c > m\r\n\r\nnewtype Traversal f = Traversal { getTraversal :: f () }\r\n\r\ninstance Applicative f => Semigroup (Traversal f) where\r\n Traversal a <> Traversal b = Traversal (a *> b)\r\n\r\ninstance Applicative f => Reducer (f a) (Traversal f) where\r\n Traversal a `snoc` b = Traversal (() <$ (a *> b))\r\n\r\nsnocTraversal :: Reducer (f ()) (Traversal f) => Traversal f > f () > Traversal f\r\nsnocTraversal a = (<>) a . Traversal\r\n{# RULES \"snocTraversal\" snoc = snocTraversal #}\r\n}}}\r\n\r\nBut on GHC 8.2.1 and later, it gives this warning:\r\n\r\n{{{\r\nGHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Main ( Bug.hs, interpreted )\r\n\r\nBug.hs:21:18: warning: [Wsimplifiableclassconstraints]\r\n • The constraint ‘Reducer (f ()) (Traversal f)’\r\n matches an instance declaration\r\n instance Applicative f => Reducer (f a) (Traversal f)\r\n  Defined at Bug.hs:18:10\r\n This makes type inference for inner bindings fragile;\r\n either use MonoLocalBinds, or simplify it using the instance\r\n • In the type signature:\r\n snocTraversal :: Reducer (f ()) (Traversal f) =>\r\n Traversal f > f () > Traversal f\r\n \r\n21  snocTraversal :: Reducer (f ()) (Traversal f) => Traversal f > f () > Traversal f\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nI decided to follow GHC's orders and reduce the `Reducer (f ()) (Traversal f)` context to just `Applicative f`:\r\n\r\n{{{#!hs\r\n{# LANGUAGE FlexibleContexts #}\r\n{# LANGUAGE FlexibleInstances #}\r\n{# LANGUAGE MultiParamTypeClasses #}\r\n\r\nimport Prelude (Applicative(..), Functor(..), (.))\r\n\r\nclass Semigroup m where\r\n (<>) :: m > m > m\r\n\r\nclass Semigroup m => Reducer c m where\r\n snoc :: m > c > m\r\n\r\nnewtype Traversal f = Traversal { getTraversal :: f () }\r\n\r\ninstance Applicative f => Semigroup (Traversal f) where\r\n Traversal a <> Traversal b = Traversal (a *> b)\r\n\r\ninstance Applicative f => Reducer (f a) (Traversal f) where\r\n Traversal a `snoc` b = Traversal (() <$ (a *> b))\r\n\r\nsnocTraversal :: Applicative f => Traversal f > f () > Traversal f\r\nsnocTraversal a = (<>) a . Traversal\r\n{# RULES \"snocTraversal\" snoc = snocTraversal #}\r\n}}}\r\n\r\nBut after doing so, the file no longer typechecks!\r\n\r\n{{{\r\nGHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Main ( Bug.hs, interpreted )\r\n\r\nBug.hs:23:34: error:\r\n • Could not deduce (Applicative f)\r\n arising from a use of ‘snocTraversal’\r\n from the context: Reducer (f ()) (Traversal f)\r\n bound by the RULE \"snocTraversal\" at Bug.hs:23:1146\r\n Possible fix:\r\n add (Applicative f) to the context of the RULE \"snocTraversal\"\r\n • In the expression: snocTraversal\r\n When checking the transformation rule \"snocTraversal\"\r\n \r\n23  {# RULES \"snocTraversal\" snoc = snocTraversal #}\r\n  ^^^^^^^^^^^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/14320Brackets change meaning of valueconstructor type20201005T16:52:45Znr@eecs.harvard.eduBrackets change meaning of valueconstructor typeSome legacy code from GHC 7.x does not compile under 8.0 or 8.2.
The issue seems to be that I have wrapped brackets around the type
of a value constructor, and 8.x does not want to see those brackets.
To try to learn if this change was deliberate, I have searched the release notes. Found nothing.
I am hoping this is an actual bug, as I would hope to be able to wrap any type or term in brackets without changing its meaning (except of course for fixity).
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  Linux 
 Architecture  x86_64 (amd64) 
</details>
<! {"blocked_by":[],"summary":"Brackets change meaning of valueconstructor type","status":"New","operating_system":"Linux","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["GADT,","existential","type"],"differentials":[],"test_case":"","architecture":"x86_64 (amd64)","cc":[""],"type":"Bug","description":"Some legacy code from GHC 7.x does not compile under 8.0 or 8.2.\r\nThe issue seems to be that I have wrapped brackets around the type\r\nof a value constructor, and 8.x does not want to see those brackets.\r\n\r\nTo try to learn if this change was deliberate, I have searched the release notes. Found nothing.\r\n\r\nI am hoping this is an actual bug, as I would hope to be able to wrap any type or term in brackets without changing its meaning (except of course for fixity).","type_of_failure":"OtherFailure","blocking":[]} >Some legacy code from GHC 7.x does not compile under 8.0 or 8.2.
The issue seems to be that I have wrapped brackets around the type
of a value constructor, and 8.x does not want to see those brackets.
To try to learn if this change was deliberate, I have searched the release notes. Found nothing.
I am hoping this is an actual bug, as I would hope to be able to wrap any type or term in brackets without changing its meaning (except of course for fixity).
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  Linux 
 Architecture  x86_64 (amd64) 
</details>
<! {"blocked_by":[],"summary":"Brackets change meaning of valueconstructor type","status":"New","operating_system":"Linux","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["GADT,","existential","type"],"differentials":[],"test_case":"","architecture":"x86_64 (amd64)","cc":[""],"type":"Bug","description":"Some legacy code from GHC 7.x does not compile under 8.0 or 8.2.\r\nThe issue seems to be that I have wrapped brackets around the type\r\nof a value constructor, and 8.x does not want to see those brackets.\r\n\r\nTo try to learn if this change was deliberate, I have searched the release notes. Found nothing.\r\n\r\nI am hoping this is an actual bug, as I would hope to be able to wrap any type or term in brackets without changing its meaning (except of course for fixity).","type_of_failure":"OtherFailure","blocking":[]} >8.4.1https://gitlab.haskell.org/ghc/ghc//issues/14319Stuck type families can lead to lousy error messages20200123T19:27:40ZDavid FeuerStuck type families can lead to lousy error messagesI first noticed this problem at the type level:
```hs
{# language TypeFamilies, TypeInType, ScopedTypeVariables #}
module ArityError where
import Data.Kind
import GHC.TypeLits
import Data.Proxy
type family F (s :: Symbol) :: Type
type family G (s :: Symbol) :: F s
type instance G "Hi" = Maybe
```
This produces the error message
```hs
ArityError.hs:10:24: error:
• Expecting one more argument to ‘Maybe’
Expected kind ‘F "Hi"’, but ‘Maybe’ has kind ‘* > *’
• In the type ‘Maybe’
In the type instance declaration for ‘G’

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

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

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

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

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

14  f _ _ = undefined
 ^^^^^^^^^^^^^^^^^
```
The claim that `Proxy s > F s` has only one argument is bogus; we only know that it has *at least* one argument. The fix (I imagine) is to refrain from reporting arity errors when we don't know enough about the relevant arities.