GHC issueshttps://gitlab.haskell.org/ghc/ghc//issues20201114T10:00:44Zhttps://gitlab.haskell.org/ghc/ghc//issues/16887GHC panic: "StgCmmEnv: variable not found"  Something with MonoLocalBinds, t...20201114T10:00:44ZBerengalGHC panic: "StgCmmEnv: variable not found"  Something with MonoLocalBinds, type inference and fdefertypeerrors# Summary
GHC panics on some modules with GADTs enabled, top level declarations without type annotations and fdefertypeerrors enabled.
# Steps to reproduce
The smallest module I could find to trigger the bug:
```
{# LANGUAGE GADTs #}
breaks = pure "anything polymorphic"
main = do
putStrLn "could be anything"
breaks
putStrLn "also could be anything"
```
Command and output:
```
▶ ghc fdefertypeerrors Panic.hs
[1 of 1] Compiling Main ( Panic.hs, Panic.o )
ghc: panic! (the 'impossible' happened)
(GHC version 8.6.5 for x86_64unknownlinux):
StgCmmEnv: variable not found
$dMonad_a1ce
local binds for:
$trModule
whatever_rq4
$trModule1_r1p6
$trModule2_r1pj
$trModule3_r1pk
$trModule4_r1pl
sat_s1rx
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable
pprPanic, called at compiler/codeGen/StgCmmEnv.hs:149:9 in ghc:StgCmmEnv
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
```
This compiles fine without `fdefertypeerrors`, or with type signatures for either `breaks` or `main`, or without GADTs enabled. GHCi loads the module without problem, but panics whenever it needs to use any symbol from the module, including unrelated symbols.
# Expected behavior
I expect GHC not to panic.
# Environment
* GHC version used: 8.6.5
Optional:
* Operating System: Arch linux
* System Architecture: x86_64# Summary
GHC panics on some modules with GADTs enabled, top level declarations without type annotations and fdefertypeerrors enabled.
# Steps to reproduce
The smallest module I could find to trigger the bug:
```
{# LANGUAGE GADTs #}
breaks = pure "anything polymorphic"
main = do
putStrLn "could be anything"
breaks
putStrLn "also could be anything"
```
Command and output:
```
▶ ghc fdefertypeerrors Panic.hs
[1 of 1] Compiling Main ( Panic.hs, Panic.o )
ghc: panic! (the 'impossible' happened)
(GHC version 8.6.5 for x86_64unknownlinux):
StgCmmEnv: variable not found
$dMonad_a1ce
local binds for:
$trModule
whatever_rq4
$trModule1_r1p6
$trModule2_r1pj
$trModule3_r1pk
$trModule4_r1pl
sat_s1rx
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable
pprPanic, called at compiler/codeGen/StgCmmEnv.hs:149:9 in ghc:StgCmmEnv
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
```
This compiles fine without `fdefertypeerrors`, or with type signatures for either `breaks` or `main`, or without GADTs enabled. GHCi loads the module without problem, but panics whenever it needs to use any symbol from the module, including unrelated symbols.
# Expected behavior
I expect GHC not to panic.
# Environment
* GHC version used: 8.6.5
Optional:
* Operating System: Arch linux
* System Architecture: x86_64https://gitlab.haskell.org/ghc/ghc//issues/16422Inconsistent results with inaccessible code due to (~) vs. (~~)20190902T11:50:43ZRyan ScottInconsistent results with inaccessible code due to (~) vs. (~~)The following code typechecks:
```haskell
{# LANGUAGE GADTs #}
{# LANGUAGE TypeOperators #}
module Bug where
import Data.Type.Equality
data T = (Int ~ Char) => MkT { fld :: Int }
```
```
$ /opt/ghc/8.6.3/bin/ghci Bug.hs
GHCi, version 8.6.3: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:7:32: warning: [Winaccessiblecode]
• Couldn't match type ‘Int’ with ‘Char’
Inaccessible code in
a pattern with constructor: MkT :: (Int ~ Char) => Int > T,
in an equation for ‘fld’
• In the pattern: MkT {fld = fld}
In an equation for ‘fld’: fld MkT {fld = fld} = fld

7  data T = (Int ~ Char) => MkT { fld :: Int }
 ^^^
```
It produces a warning, of course, since there's no way to ever actually invoke `fld`.
The interesting part of this is that if you replace `~` with `~~` in this program, then GHC will switch from accepting to rejecting it:
```haskell
data T = (Int ~~ Char) => MkT { fld :: Int }
```
```
$ /opt/ghc/8.6.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:7:10: error:
• Couldn't match expected type ‘Char’ with actual type ‘Int’
• In the ambiguity check for ‘MkT’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the definition of data constructor ‘MkT’
In the data type declaration for ‘T’

7  data T = (Int ~~ Char) => MkT { fld :: Int }
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
This feels strangely inconsistent.

A similar phenomenon occurs in function definitions. This function is accepted (with no warnings):
```haskell
{# LANGUAGE GADTs #}
{# LANGUAGE TypeOperators #}
module Bug where
import Data.Type.Equality
f :: (Int ~ Char) => () > ()
f () = ()
```
But it is no longer accepted when `~` is swapped out with `~~`:
```haskell
f :: (Int ~~ Char) => () > ()
f () = ()
```
```
$ /opt/ghc/8.6.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:7:6: error:
• Couldn't match expected type ‘Char’ with actual type ‘Int’
• In the ambiguity check for ‘f’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature: f :: (Int ~~ Char) => () > ()

7  f :: (Int ~~ Char) => () > ()
 ^^^^^^^^^^^^^^^^^^^^^^^^^
```The following code typechecks:
```haskell
{# LANGUAGE GADTs #}
{# LANGUAGE TypeOperators #}
module Bug where
import Data.Type.Equality
data T = (Int ~ Char) => MkT { fld :: Int }
```
```
$ /opt/ghc/8.6.3/bin/ghci Bug.hs
GHCi, version 8.6.3: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:7:32: warning: [Winaccessiblecode]
• Couldn't match type ‘Int’ with ‘Char’
Inaccessible code in
a pattern with constructor: MkT :: (Int ~ Char) => Int > T,
in an equation for ‘fld’
• In the pattern: MkT {fld = fld}
In an equation for ‘fld’: fld MkT {fld = fld} = fld

7  data T = (Int ~ Char) => MkT { fld :: Int }
 ^^^
```
It produces a warning, of course, since there's no way to ever actually invoke `fld`.
The interesting part of this is that if you replace `~` with `~~` in this program, then GHC will switch from accepting to rejecting it:
```haskell
data T = (Int ~~ Char) => MkT { fld :: Int }
```
```
$ /opt/ghc/8.6.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:7:10: error:
• Couldn't match expected type ‘Char’ with actual type ‘Int’
• In the ambiguity check for ‘MkT’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the definition of data constructor ‘MkT’
In the data type declaration for ‘T’

7  data T = (Int ~~ Char) => MkT { fld :: Int }
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
This feels strangely inconsistent.

A similar phenomenon occurs in function definitions. This function is accepted (with no warnings):
```haskell
{# LANGUAGE GADTs #}
{# LANGUAGE TypeOperators #}
module Bug where
import Data.Type.Equality
f :: (Int ~ Char) => () > ()
f () = ()
```
But it is no longer accepted when `~` is swapped out with `~~`:
```haskell
f :: (Int ~~ Char) => () > ()
f () = ()
```
```
$ /opt/ghc/8.6.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:7:6: error:
• Couldn't match expected type ‘Char’ with actual type ‘Int’
• In the ambiguity check for ‘f’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature: f :: (Int ~~ Char) => () > ()

7  f :: (Int ~~ Char) => () > ()
 ^^^^^^^^^^^^^^^^^^^^^^^^^
```https://gitlab.haskell.org/ghc/ghc//issues/16374Cannot deduce constraint from itself with polykinded type family20190707T18:00:20ZrolandCannot deduce constraint from itself with polykinded type familyCompiling
```hs
{# LANGUAGE PolyKinds, TypeFamilies #}
module Eq where
type family F a :: k where
withEq :: F Int ~ F Bool => a
withEq = undefined
```
gives an arguably confusing error message:
```
Eq.hs:7:11: error:
• Could not deduce: F Int ~ F Bool
from the context: F Int ~ F Bool
bound by the type signature for:
withEq :: forall k a. (F Int ~ F Bool) => a
at Eq.hs:7:1129
NB: ‘F’ is a noninjective type family
The type variable ‘k0’ is ambiguous
• In the ambiguity check for ‘withEq’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature: withEq :: F Int ~ F Bool => a
```
I'm not claiming this program should necessarily typecheck, but "Cannot deduce X from the context X" induces headscratching.
Replacing `k` with `*` in the definition of `F` makes the error go away.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Cannot deduce constraint from itself with polykinded type family","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Compiling\r\n{{{#!hs\r\n{# LANGUAGE PolyKinds, TypeFamilies #}\r\n\r\nmodule Eq where\r\n\r\ntype family F a :: k where\r\n\r\nwithEq :: F Int ~ F Bool => a\r\nwithEq = undefined\r\n}}}\r\n\r\ngives an arguably confusing error message:\r\n\r\n{{{\r\nEq.hs:7:11: error:\r\n • Could not deduce: F Int ~ F Bool\r\n from the context: F Int ~ F Bool\r\n bound by the type signature for:\r\n withEq :: forall k a. (F Int ~ F Bool) => a\r\n at Eq.hs:7:1129\r\n NB: ‘F’ is a noninjective type family\r\n The type variable ‘k0’ is ambiguous\r\n • In the ambiguity check for ‘withEq’\r\n To defer the ambiguity check to use sites, enable AllowAmbiguousTypes\r\n In the type signature: withEq :: F Int ~ F Bool => a\r\n}}}\r\n\r\nI'm not claiming this program should necessarily typecheck, but \"Cannot deduce X from the context X\" induces headscratching.\r\n\r\nReplacing `k` with `*` in the definition of `F` makes the error go away.","type_of_failure":"OtherFailure","blocking":[]} >Compiling
```hs
{# LANGUAGE PolyKinds, TypeFamilies #}
module Eq where
type family F a :: k where
withEq :: F Int ~ F Bool => a
withEq = undefined
```
gives an arguably confusing error message:
```
Eq.hs:7:11: error:
• Could not deduce: F Int ~ F Bool
from the context: F Int ~ F Bool
bound by the type signature for:
withEq :: forall k a. (F Int ~ F Bool) => a
at Eq.hs:7:1129
NB: ‘F’ is a noninjective type family
The type variable ‘k0’ is ambiguous
• In the ambiguity check for ‘withEq’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature: withEq :: F Int ~ F Bool => a
```
I'm not claiming this program should necessarily typecheck, but "Cannot deduce X from the context X" induces headscratching.
Replacing `k` with `*` in the definition of `F` makes the error go away.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Cannot deduce constraint from itself with polykinded type family","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Compiling\r\n{{{#!hs\r\n{# LANGUAGE PolyKinds, TypeFamilies #}\r\n\r\nmodule Eq where\r\n\r\ntype family F a :: k where\r\n\r\nwithEq :: F Int ~ F Bool => a\r\nwithEq = undefined\r\n}}}\r\n\r\ngives an arguably confusing error message:\r\n\r\n{{{\r\nEq.hs:7:11: error:\r\n • Could not deduce: F Int ~ F Bool\r\n from the context: F Int ~ F Bool\r\n bound by the type signature for:\r\n withEq :: forall k a. (F Int ~ F Bool) => a\r\n at Eq.hs:7:1129\r\n NB: ‘F’ is a noninjective type family\r\n The type variable ‘k0’ is ambiguous\r\n • In the ambiguity check for ‘withEq’\r\n To defer the ambiguity check to use sites, enable AllowAmbiguousTypes\r\n In the type signature: withEq :: F Int ~ F Bool => a\r\n}}}\r\n\r\nI'm not claiming this program should necessarily typecheck, but \"Cannot deduce X from the context X\" induces headscratching.\r\n\r\nReplacing `k` with `*` in the definition of `F` makes the error go away.","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/16371GHC should be more forgiving with visible dependent quantification in visible...20201109T15:26:20ZRyan ScottGHC should be more forgiving with visible dependent quantification in visible type applicationsGHC HEAD currently rejects the following code:
```hs
{# LANGUAGE ImpredicativeTypes #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeApplications #}
module Bug where
import Data.Kind
import Data.Proxy
f :: forall k (a :: k). Proxy a
f = Proxy
g :: forall (a :: forall x > x > Type). Proxy a
g = f @(forall x > x > Type) @a
```
```
GHCi, version 8.9.20190227: https://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:14:6: error:
• Illegal visible, dependent quantification in the type of a term:
forall x > x > *
(GHC does not yet support this)
• In the type signature:
g :: forall (a :: forall x > x > Type). Proxy a

14  g :: forall (a :: forall x > x > Type). Proxy a
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
This test is implemented in `TcValidity.vdqAllowed`.
But GHC is being too conservative here. `forall x > x > *` _isn't_ the type of a term here, but rather the kind of a type variable, and it's perfectly admissible to use visible dependent quantification in such a scenario.
The immediate reason that this happens is because of this code:
```hs
vdqAllowed (TypeAppCtxt {}) = False
```
Unfortunately, fixing this bug isn't as simply as changing `False` to `True`. If you do that, then GHC becomes _too_ forgiving and allows things like this:
```hs
{# LANGUAGE ImpredicativeTypes #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE TypeApplications #}
lol :: forall a. a
lol = undefined
t2 = lol @(forall a > a > a)
```
Here, visible dependent quantification is leaking into the type of a term, which we definitely don't want to happen.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.9 
 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 should be more forgiving with visible dependent quantification in visible type applications","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.9","keywords":["VisibleDependentQuantification"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"GHC HEAD currently rejects the following code:\r\n\r\n{{{#!hs\r\n{# LANGUAGE ImpredicativeTypes #}\r\n{# LANGUAGE PolyKinds #}\r\n{# LANGUAGE RankNTypes #}\r\n{# LANGUAGE ScopedTypeVariables #}\r\n{# LANGUAGE TypeApplications #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\nimport Data.Proxy\r\n\r\nf :: forall k a. Proxy a\r\nf = Proxy\r\n\r\ng :: forall (a :: forall x > x > Type). Proxy a\r\ng = f @(forall x > x > Type) @a\r\n}}}\r\n{{{\r\nGHCi, version 8.9.20190227: https://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:14:6: error:\r\n • Illegal visible, dependent quantification in the type of a term:\r\n forall x > x > *\r\n (GHC does not yet support this)\r\n • In the type signature:\r\n g :: forall (a :: forall x > x > Type). Proxy a\r\n \r\n14  g :: forall (a :: forall x > x > Type). Proxy a\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nBut GHC is being too conservative here. `forall x > x > *` //isn't// the type of a term here, but rather the kind of a type variable, and it's perfectly admissible to use visible dependent quantification in such a scenario.\r\n\r\nThe immediate reason that this happens is because of this code:\r\n\r\n{{{#!hs\r\nvdqAllowed (TypeAppCtxt {}) = False\r\n}}}\r\n\r\nUnfortunately, fixing this bug isn't as simply as changing `False` to `True`. If you do that, then GHC becomes //too// forgiving and allows things like this:\r\n\r\n{{{#!hs\r\n{# LANGUAGE ImpredicativeTypes #}\r\n{# LANGUAGE PolyKinds #}\r\n{# LANGUAGE RankNTypes #}\r\n{# LANGUAGE TypeApplications #}\r\n\r\nlol :: forall a. a\r\nlol = undefined\r\n\r\nt2 = lol @(forall a > a > a)\r\n}}}\r\n\r\nHere, visible dependent quantification is leaking into the type of a term, which we definitely don't want to happen.","type_of_failure":"OtherFailure","blocking":[]} >GHC HEAD currently rejects the following code:
```hs
{# LANGUAGE ImpredicativeTypes #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeApplications #}
module Bug where
import Data.Kind
import Data.Proxy
f :: forall k (a :: k). Proxy a
f = Proxy
g :: forall (a :: forall x > x > Type). Proxy a
g = f @(forall x > x > Type) @a
```
```
GHCi, version 8.9.20190227: https://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:14:6: error:
• Illegal visible, dependent quantification in the type of a term:
forall x > x > *
(GHC does not yet support this)
• In the type signature:
g :: forall (a :: forall x > x > Type). Proxy a

14  g :: forall (a :: forall x > x > Type). Proxy a
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
This test is implemented in `TcValidity.vdqAllowed`.
But GHC is being too conservative here. `forall x > x > *` _isn't_ the type of a term here, but rather the kind of a type variable, and it's perfectly admissible to use visible dependent quantification in such a scenario.
The immediate reason that this happens is because of this code:
```hs
vdqAllowed (TypeAppCtxt {}) = False
```
Unfortunately, fixing this bug isn't as simply as changing `False` to `True`. If you do that, then GHC becomes _too_ forgiving and allows things like this:
```hs
{# LANGUAGE ImpredicativeTypes #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE TypeApplications #}
lol :: forall a. a
lol = undefined
t2 = lol @(forall a > a > a)
```
Here, visible dependent quantification is leaking into the type of a term, which we definitely don't want to happen.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.9 
 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 should be more forgiving with visible dependent quantification in visible type applications","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.9","keywords":["VisibleDependentQuantification"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"GHC HEAD currently rejects the following code:\r\n\r\n{{{#!hs\r\n{# LANGUAGE ImpredicativeTypes #}\r\n{# LANGUAGE PolyKinds #}\r\n{# LANGUAGE RankNTypes #}\r\n{# LANGUAGE ScopedTypeVariables #}\r\n{# LANGUAGE TypeApplications #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\nimport Data.Proxy\r\n\r\nf :: forall k a. Proxy a\r\nf = Proxy\r\n\r\ng :: forall (a :: forall x > x > Type). Proxy a\r\ng = f @(forall x > x > Type) @a\r\n}}}\r\n{{{\r\nGHCi, version 8.9.20190227: https://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:14:6: error:\r\n • Illegal visible, dependent quantification in the type of a term:\r\n forall x > x > *\r\n (GHC does not yet support this)\r\n • In the type signature:\r\n g :: forall (a :: forall x > x > Type). Proxy a\r\n \r\n14  g :: forall (a :: forall x > x > Type). Proxy a\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nBut GHC is being too conservative here. `forall x > x > *` //isn't// the type of a term here, but rather the kind of a type variable, and it's perfectly admissible to use visible dependent quantification in such a scenario.\r\n\r\nThe immediate reason that this happens is because of this code:\r\n\r\n{{{#!hs\r\nvdqAllowed (TypeAppCtxt {}) = False\r\n}}}\r\n\r\nUnfortunately, fixing this bug isn't as simply as changing `False` to `True`. If you do that, then GHC becomes //too// forgiving and allows things like this:\r\n\r\n{{{#!hs\r\n{# LANGUAGE ImpredicativeTypes #}\r\n{# LANGUAGE PolyKinds #}\r\n{# LANGUAGE RankNTypes #}\r\n{# LANGUAGE TypeApplications #}\r\n\r\nlol :: forall a. a\r\nlol = undefined\r\n\r\nt2 = lol @(forall a > a > a)\r\n}}}\r\n\r\nHere, visible dependent quantification is leaking into the type of a term, which we definitely don't want to happen.","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/16232Add setField to HasField20210228T21:59:24ZAdam GundryAdd setField to HasFieldThis ticket is to track the implementation of https://github.com/ghcproposals/ghcproposals/blob/master/proposals/0042recordsetfield.rst
I've made a start on the implementation but have a question on which I'd appreciate some input: how should the dictionary for `HasField` be generated?
To recap, recall that at present, `HasField x r a` is coercible to `r > a` so the dictionary can be constructed merely by taking the selector function for the field and wrapping it in an appropriate coercion.
With the proposal, `HasField x r a` will instead be represented as `r > (a > r, a)` where the first component of the tuple is an update function. The problem is how to define this update function in Core. This function should perform case analysis on the record data type, where each case replaces the value of the field being updated and preserves all the other fields. For example, given a data type `data T = MkT { foo :: Int, bar :: Bool }` we need to generate
```hs
\ r x > case r of MkT {foo = _, bar = bar} > MkT { foo = x, bar = bar }
```
The most obvious approach is to generate welltyped Core for the update function directly, but this seems to be rather complex, in particular because of the worker/wrapper distinction, as one ends up reconstructing much of the typechecking/desugaring for record pattern matching and construction. This also seems like a lot of work to do every time a `HasField` constraint is solved.
Would it be reasonable to generate update functions for fields at definition sites, as we do for selector functions? I've implemented this in the past, and it is relatively simple to generate renamed syntax to feed in to the typechecker. However, this would add some overhead for every field, even if `HasField` was not subsequently used, and would require some naming scheme for update functions.
Or are there other options? Is there some way to solve a `HasField` constraint and construct its dictionary by emitting renamed syntax for subsequent typechecking, such that subsequently solving similar constraints will use the same dictionary?
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.7 
 Type  FeatureRequest 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  NeilMitchell, simonpj 
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Add setField to HasField","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.10.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.7","keywords":["ORF"],"differentials":[],"test_case":"","architecture":"","cc":["NeilMitchell","simonpj"],"type":"FeatureRequest","description":"This ticket is to track the implementation of https://github.com/ghcproposals/ghcproposals/blob/master/proposals/0042recordsetfield.rst\r\n\r\nI've made a start on the implementation but have a question on which I'd appreciate some input: how should the dictionary for `HasField` be generated?\r\n\r\nTo recap, recall that at present, `HasField x r a` is coercible to `r > a` so the dictionary can be constructed merely by taking the selector function for the field and wrapping it in an appropriate coercion.\r\n\r\nWith the proposal, `HasField x r a` will instead be represented as `r > (a > r, a)` where the first component of the tuple is an update function. The problem is how to define this update function in Core. This function should perform case analysis on the record data type, where each case replaces the value of the field being updated and preserves all the other fields. For example, given a data type `data T = MkT { foo :: Int, bar :: Bool }` we need to generate\r\n{{{#!hs\r\n\\ r x > case r of MkT {foo = _, bar = bar} > MkT { foo = x, bar = bar }\r\n}}}\r\n\r\nThe most obvious approach is to generate welltyped Core for the update function directly, but this seems to be rather complex, in particular because of the worker/wrapper distinction, as one ends up reconstructing much of the typechecking/desugaring for record pattern matching and construction. This also seems like a lot of work to do every time a `HasField` constraint is solved.\r\n\r\nWould it be reasonable to generate update functions for fields at definition sites, as we do for selector functions? I've implemented this in the past, and it is relatively simple to generate renamed syntax to feed in to the typechecker. However, this would add some overhead for every field, even if `HasField` was not subsequently used, and would require some naming scheme for update functions.\r\n\r\nOr are there other options? Is there some way to solve a `HasField` constraint and construct its dictionary by emitting renamed syntax for subsequent typechecking, such that subsequently solving similar constraints will use the same dictionary?","type_of_failure":"OtherFailure","blocking":[]} >This ticket is to track the implementation of https://github.com/ghcproposals/ghcproposals/blob/master/proposals/0042recordsetfield.rst
I've made a start on the implementation but have a question on which I'd appreciate some input: how should the dictionary for `HasField` be generated?
To recap, recall that at present, `HasField x r a` is coercible to `r > a` so the dictionary can be constructed merely by taking the selector function for the field and wrapping it in an appropriate coercion.
With the proposal, `HasField x r a` will instead be represented as `r > (a > r, a)` where the first component of the tuple is an update function. The problem is how to define this update function in Core. This function should perform case analysis on the record data type, where each case replaces the value of the field being updated and preserves all the other fields. For example, given a data type `data T = MkT { foo :: Int, bar :: Bool }` we need to generate
```hs
\ r x > case r of MkT {foo = _, bar = bar} > MkT { foo = x, bar = bar }
```
The most obvious approach is to generate welltyped Core for the update function directly, but this seems to be rather complex, in particular because of the worker/wrapper distinction, as one ends up reconstructing much of the typechecking/desugaring for record pattern matching and construction. This also seems like a lot of work to do every time a `HasField` constraint is solved.
Would it be reasonable to generate update functions for fields at definition sites, as we do for selector functions? I've implemented this in the past, and it is relatively simple to generate renamed syntax to feed in to the typechecker. However, this would add some overhead for every field, even if `HasField` was not subsequently used, and would require some naming scheme for update functions.
Or are there other options? Is there some way to solve a `HasField` constraint and construct its dictionary by emitting renamed syntax for subsequent typechecking, such that subsequently solving similar constraints will use the same dictionary?
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.7 
 Type  FeatureRequest 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  NeilMitchell, simonpj 
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Add setField to HasField","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.10.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.7","keywords":["ORF"],"differentials":[],"test_case":"","architecture":"","cc":["NeilMitchell","simonpj"],"type":"FeatureRequest","description":"This ticket is to track the implementation of https://github.com/ghcproposals/ghcproposals/blob/master/proposals/0042recordsetfield.rst\r\n\r\nI've made a start on the implementation but have a question on which I'd appreciate some input: how should the dictionary for `HasField` be generated?\r\n\r\nTo recap, recall that at present, `HasField x r a` is coercible to `r > a` so the dictionary can be constructed merely by taking the selector function for the field and wrapping it in an appropriate coercion.\r\n\r\nWith the proposal, `HasField x r a` will instead be represented as `r > (a > r, a)` where the first component of the tuple is an update function. The problem is how to define this update function in Core. This function should perform case analysis on the record data type, where each case replaces the value of the field being updated and preserves all the other fields. For example, given a data type `data T = MkT { foo :: Int, bar :: Bool }` we need to generate\r\n{{{#!hs\r\n\\ r x > case r of MkT {foo = _, bar = bar} > MkT { foo = x, bar = bar }\r\n}}}\r\n\r\nThe most obvious approach is to generate welltyped Core for the update function directly, but this seems to be rather complex, in particular because of the worker/wrapper distinction, as one ends up reconstructing much of the typechecking/desugaring for record pattern matching and construction. This also seems like a lot of work to do every time a `HasField` constraint is solved.\r\n\r\nWould it be reasonable to generate update functions for fields at definition sites, as we do for selector functions? I've implemented this in the past, and it is relatively simple to generate renamed syntax to feed in to the typechecker. However, this would add some overhead for every field, even if `HasField` was not subsequently used, and would require some naming scheme for update functions.\r\n\r\nOr are there other options? Is there some way to solve a `HasField` constraint and construct its dictionary by emitting renamed syntax for subsequent typechecking, such that subsequently solving similar constraints will use the same dictionary?","type_of_failure":"OtherFailure","blocking":[]} >Adam GundryAdam Gundryhttps://gitlab.haskell.org/ghc/ghc//issues/16154Wredundantconstraints: False positive20190707T18:01:16ZFumiaki KinoshitaWredundantconstraints: False positiveGHC produces a warning for the attached source, although it won't compile if the suggested constraints are removed:
```
redundantconstraint.hs:24:1: warning: [Wredundantconstraints]
• Redundant constraints: (KnownNat 42, Capture 42 p)
• In the type signature for:
foo :: Foo 42

24  foo :: Foo 42
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Wredundantconstraints: False positive","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"GHC produces a warning for the attached source, although it won't compile if the suggested constraints are removed:\r\n\r\n{{{\r\nredundantconstraint.hs:24:1: warning: [Wredundantconstraints]\r\n • Redundant constraints: (KnownNat 42, Capture 42 p)\r\n • In the type signature for:\r\n foo :: Foo 42\r\n \r\n24  foo :: Foo 42\r\n}}}\r\n","type_of_failure":"OtherFailure","blocking":[]} >GHC produces a warning for the attached source, although it won't compile if the suggested constraints are removed:
```
redundantconstraint.hs:24:1: warning: [Wredundantconstraints]
• Redundant constraints: (KnownNat 42, Capture 42 p)
• In the type signature for:
foo :: Foo 42

24  foo :: Foo 42
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Wredundantconstraints: False positive","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"GHC produces a warning for the attached source, although it won't compile if the suggested constraints are removed:\r\n\r\n{{{\r\nredundantconstraint.hs:24:1: warning: [Wredundantconstraints]\r\n • Redundant constraints: (KnownNat 42, Capture 42 p)\r\n • In the type signature for:\r\n foo :: Foo 42\r\n \r\n24  foo :: Foo 42\r\n}}}\r\n","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/16127Panic: piResultTys1 in compiler/types/Type.hs:1022:520200527T17:57:14ZSerge KosyrevPanic: piResultTys1 in compiler/types/Type.hs:1022:5I apologize in advance for a nonminimised repro.
The panic (with a small `ddumptctrace` excerpt, but full log also attached):
```
tcPolyExprNC
Check{Vocab
*
(k_a4TNy[tau:2] > Constraint)
i_a4TNv[tau:2]
(Present * k_a4TNy[tau:2] i_a4TNv[tau:2])}
tcSkolemise
tcInferId
voc_a4TB2 :: Vocab i_a4TMf[sk:1] (Present * * i_a4TMf[sk:1])
tcCheckId
voc_a4TB2
Vocab i_a4TMf[sk:1] (Present * * i_a4TMf[sk:1])
Check{Vocab
*
(k_a4TNy[tau:2] > Constraint)
i_a4TNv[tau:2]
(Present * k_a4TNy[tau:2] i_a4TNv[tau:2])}
tcWrapResult
Actual: Vocab i_a4TMf[sk:1] (Present * * i_a4TMf[sk:1])
Expected: Check{Vocab
*
(k_a4TNy[tau:2] > Constraint)
i_a4TNv[tau:2]
(Present * k_a4TNy[tau:2] i_a4TNv[tau:2])}
tc_sub_type_ds
ty_actual = Vocab i_a4TMf[sk:1] (Present * * i_a4TMf[sk:1])
ty_expected = Vocab
*
(k_a4TNy[tau:2] > Constraint)
i_a4TNv[tau:2]
(Present * k_a4TNy[tau:2] i_a4TNv[tau:2])
deeply_instantiate final subst
origin: arising from a use of ‘voc_a4TB2’
type: Vocab i_a4TMf[sk:1] (Present * * i_a4TMf[sk:1])
new type: Vocab i_a4TMf[sk:1] (Present * * i_a4TMf[sk:1])
subst: [TCvSubst
In scope: InScope {i_a4TMf}
Type env: []
Co env: []]
u_tys
tclvl 2
Vocab i_a4TMf[sk:1] (Present * * i_a4TMf[sk:1])
~
Vocab
*
(k_a4TNy[tau:2] > Constraint)
i_a4TNv[tau:2]
(Present * k_a4TNy[tau:2] i_a4TNv[tau:2])
arising from a type equality Vocab
i_a4TMf[sk:1] (Present * * i_a4TMf[sk:1])
~
Vocab
*
(k_a4TNy[tau:2] > Constraint)
i_a4TNv[tau:2]
(Present * k_a4TNy[tau:2] i_a4TNv[tau:2])
<no location info>: error:
ghc: panic! (the 'impossible' happened)
(GHC version 8.6.1 for x86_64unknownlinux):
piResultTys1
*
[i_a4TNv[tau:2], Present * k_a4TNy[tau:2] i_a4TNv[tau:2]]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable
pprPanic, called at compiler/types/Type.hs:1022:5 in ghc:Type
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
```
Repro (requires Nix & some download time, provides hard repro guarantees in return):
```
$ git clone https://github.com/deepfire/holotype
$ cd holotype
$ git reset hard 5c80e9239a3c18d67106920db8f832abc7bd9a93
$ nixshell
[nixshell:~/holotype]$ cabal build lib:holotype
```I apologize in advance for a nonminimised repro.
The panic (with a small `ddumptctrace` excerpt, but full log also attached):
```
tcPolyExprNC
Check{Vocab
*
(k_a4TNy[tau:2] > Constraint)
i_a4TNv[tau:2]
(Present * k_a4TNy[tau:2] i_a4TNv[tau:2])}
tcSkolemise
tcInferId
voc_a4TB2 :: Vocab i_a4TMf[sk:1] (Present * * i_a4TMf[sk:1])
tcCheckId
voc_a4TB2
Vocab i_a4TMf[sk:1] (Present * * i_a4TMf[sk:1])
Check{Vocab
*
(k_a4TNy[tau:2] > Constraint)
i_a4TNv[tau:2]
(Present * k_a4TNy[tau:2] i_a4TNv[tau:2])}
tcWrapResult
Actual: Vocab i_a4TMf[sk:1] (Present * * i_a4TMf[sk:1])
Expected: Check{Vocab
*
(k_a4TNy[tau:2] > Constraint)
i_a4TNv[tau:2]
(Present * k_a4TNy[tau:2] i_a4TNv[tau:2])}
tc_sub_type_ds
ty_actual = Vocab i_a4TMf[sk:1] (Present * * i_a4TMf[sk:1])
ty_expected = Vocab
*
(k_a4TNy[tau:2] > Constraint)
i_a4TNv[tau:2]
(Present * k_a4TNy[tau:2] i_a4TNv[tau:2])
deeply_instantiate final subst
origin: arising from a use of ‘voc_a4TB2’
type: Vocab i_a4TMf[sk:1] (Present * * i_a4TMf[sk:1])
new type: Vocab i_a4TMf[sk:1] (Present * * i_a4TMf[sk:1])
subst: [TCvSubst
In scope: InScope {i_a4TMf}
Type env: []
Co env: []]
u_tys
tclvl 2
Vocab i_a4TMf[sk:1] (Present * * i_a4TMf[sk:1])
~
Vocab
*
(k_a4TNy[tau:2] > Constraint)
i_a4TNv[tau:2]
(Present * k_a4TNy[tau:2] i_a4TNv[tau:2])
arising from a type equality Vocab
i_a4TMf[sk:1] (Present * * i_a4TMf[sk:1])
~
Vocab
*
(k_a4TNy[tau:2] > Constraint)
i_a4TNv[tau:2]
(Present * k_a4TNy[tau:2] i_a4TNv[tau:2])
<no location info>: error:
ghc: panic! (the 'impossible' happened)
(GHC version 8.6.1 for x86_64unknownlinux):
piResultTys1
*
[i_a4TNv[tau:2], Present * k_a4TNy[tau:2] i_a4TNv[tau:2]]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable
pprPanic, called at compiler/types/Type.hs:1022:5 in ghc:Type
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
```
Repro (requires Nix & some download time, provides hard repro guarantees in return):
```
$ git clone https://github.com/deepfire/holotype
$ cd holotype
$ git reset hard 5c80e9239a3c18d67106920db8f832abc7bd9a93
$ nixshell
[nixshell:~/holotype]$ cabal build lib:holotype
```https://gitlab.haskell.org/ghc/ghc//issues/16115Missing associated type instance not reported with error20200123T19:38:55ZDavid FeuerMissing associated type instance not reported with errorI noticed [this SO question](https://stackoverflow.com/questions/53987924/haskellcouldntmatchexpectedtypeitemnatwithactualtype) was caused by a warning disappearing as a result of the error it caused.
```hs
{# language TypeFamilies, DataKinds #}
module NoWarning where
data Nat = Zero  Succ Nat deriving Show
class FromList a where
type Item a :: *
fromList :: [Item a] > a
instance FromList Nat where
fromList [] = Zero
fromList (a:as) = Succ (fromList as :: Nat)
fish :: Nat
fish = fromList [(),(),()]
```
If you delete `fish`, you get a nice warning:
```
NoWarning.hs:8:1: warning: [Wmissingmethods]
• No explicit associated type or default declaration for ‘Item’
• In the instance declaration for ‘FromList Nat’

8  instance FromList Nat where
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^...
```
But with `fish`, all you get is
```
NoWarning.hs:13:18: error:
• Couldn't match expected type ‘Item Nat’ with actual type ‘()’
• In the expression: ()
In the first argument of ‘fromList’, namely ‘[(), (), ()]’
In the expression: fromList [(), (), ()]

13  fish = fromList [(),(),()]

```
That warning is the proper explanation of the problem, and it's just missing!
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Missing associated type instance not reported with error","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.10.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I noticed [https://stackoverflow.com/questions/53987924/haskellcouldntmatchexpectedtypeitemnatwithactualtype this SO question] was caused by a warning disappearing as a result of the error it caused.\r\n\r\n{{{#!hs\r\n{# language TypeFamilies, DataKinds #}\r\nmodule NoWarning where\r\ndata Nat = Zero  Succ Nat deriving Show\r\nclass FromList a where\r\n type Item a :: *\r\n fromList :: [Item a] > a\r\n\r\ninstance FromList Nat where\r\n fromList [] = Zero\r\n fromList (a:as) = Succ (fromList as :: Nat)\r\n\r\nfish :: Nat\r\nfish = fromList [(),(),()]\r\n}}}\r\n\r\nIf you delete `fish`, you get a nice warning:\r\n\r\n{{{\r\nNoWarning.hs:8:1: warning: [Wmissingmethods]\r\n • No explicit associated type or default declaration for ‘Item’\r\n • In the instance declaration for ‘FromList Nat’\r\n \r\n8  instance FromList Nat where\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^...\r\n\r\n}}}\r\n\r\nBut with `fish`, all you get is\r\n\r\n{{{\r\nNoWarning.hs:13:18: error:\r\n • Couldn't match expected type ‘Item Nat’ with actual type ‘()’\r\n • In the expression: ()\r\n In the first argument of ‘fromList’, namely ‘[(), (), ()]’\r\n In the expression: fromList [(), (), ()]\r\n \r\n13  fish = fromList [(),(),()]\r\n  \r\n}}}\r\n\r\nThat warning is the proper explanation of the problem, and it's just missing!","type_of_failure":"OtherFailure","blocking":[]} >I noticed [this SO question](https://stackoverflow.com/questions/53987924/haskellcouldntmatchexpectedtypeitemnatwithactualtype) was caused by a warning disappearing as a result of the error it caused.
```hs
{# language TypeFamilies, DataKinds #}
module NoWarning where
data Nat = Zero  Succ Nat deriving Show
class FromList a where
type Item a :: *
fromList :: [Item a] > a
instance FromList Nat where
fromList [] = Zero
fromList (a:as) = Succ (fromList as :: Nat)
fish :: Nat
fish = fromList [(),(),()]
```
If you delete `fish`, you get a nice warning:
```
NoWarning.hs:8:1: warning: [Wmissingmethods]
• No explicit associated type or default declaration for ‘Item’
• In the instance declaration for ‘FromList Nat’

8  instance FromList Nat where
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^...
```
But with `fish`, all you get is
```
NoWarning.hs:13:18: error:
• Couldn't match expected type ‘Item Nat’ with actual type ‘()’
• In the expression: ()
In the first argument of ‘fromList’, namely ‘[(), (), ()]’
In the expression: fromList [(), (), ()]

13  fish = fromList [(),(),()]

```
That warning is the proper explanation of the problem, and it's just missing!
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Missing associated type instance not reported with error","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.10.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I noticed [https://stackoverflow.com/questions/53987924/haskellcouldntmatchexpectedtypeitemnatwithactualtype this SO question] was caused by a warning disappearing as a result of the error it caused.\r\n\r\n{{{#!hs\r\n{# language TypeFamilies, DataKinds #}\r\nmodule NoWarning where\r\ndata Nat = Zero  Succ Nat deriving Show\r\nclass FromList a where\r\n type Item a :: *\r\n fromList :: [Item a] > a\r\n\r\ninstance FromList Nat where\r\n fromList [] = Zero\r\n fromList (a:as) = Succ (fromList as :: Nat)\r\n\r\nfish :: Nat\r\nfish = fromList [(),(),()]\r\n}}}\r\n\r\nIf you delete `fish`, you get a nice warning:\r\n\r\n{{{\r\nNoWarning.hs:8:1: warning: [Wmissingmethods]\r\n • No explicit associated type or default declaration for ‘Item’\r\n • In the instance declaration for ‘FromList Nat’\r\n \r\n8  instance FromList Nat where\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^...\r\n\r\n}}}\r\n\r\nBut with `fish`, all you get is\r\n\r\n{{{\r\nNoWarning.hs:13:18: error:\r\n • Couldn't match expected type ‘Item Nat’ with actual type ‘()’\r\n • In the expression: ()\r\n In the first argument of ‘fromList’, namely ‘[(), (), ()]’\r\n In the expression: fromList [(), (), ()]\r\n \r\n13  fish = fromList [(),(),()]\r\n  \r\n}}}\r\n\r\nThat warning is the proper explanation of the problem, and it's just missing!","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/15989Adding extra quantified constraints leads to resolution failure20190707T18:02:08ZerorAdding extra quantified constraints leads to resolution failure```
{# LANGUAGE QuantifiedConstraints, FlexibleContexts #}
import Control.Monad.Reader
data T x = T
ok :: ( forall x x'. MonadReader (T x) (m x') )
=> m y Bool
ok = fmap not (pure True)
bad :: ( forall x x'. MonadReader (T x) (m x')
, forall x. Monad (m x) )
=> m y Bool
bad = fmap not (pure True)
better :: ( forall x x'. MonadReader (T x) (m x')
, forall x. Applicative (m x)
, forall x. Functor (m x) )
=> m y Bool
better = fmap not (pure True)
```
`ok` and `better` compile, but `bad` fails to resolve, despite having strictly more in the context than `ok`:
```
BadQC.hs:15:7: error:
• Could not deduce (Functor (m y)) arising from a use of ‘fmap’
from the context: (forall x x'. MonadReader (T x) (m x'),
forall x. Monad (m x))
bound by the type signature for:
bad :: forall (m :: * > * > *) y.
(forall x x'. MonadReader (T x) (m x'), forall x. Monad (m x)) =>
m y Bool
at BadQC.hs:(12,1)(14,15)
• In the expression: fmap not (pure True)
In an equation for ‘bad’: bad = fmap not (pure True)

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

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

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

15  bad = fmap not (pure True)
 ^^^^^^^^^
Failed, no modules loaded.
```
Also:
 `( forall x. MonadReader (T x) (m x), forall x. Monad (m x) )` compiles — the error seems to require two quantified type variables
 `( forall x x'. Monad (m x), forall x. Monad (m x) )` reports an ambiguity error on the constraint, which makes sense; if I turn on `AllowAmbiguousTypes`, it fails with the same error as above — the error isn't caused by MPTCs, and it doesn't matter that `x'` is unused
 `( forall x x'. Foldable (m x), forall x. Monad (m x) )` and `( forall x x'. Monad (m x), forall x. Foldable (m x) )` compile — being in the same class hierarchy matters
 `( forall x x'. Applicative (m x), forall x. Monad (m x) )` fails on `fmap` (but not `pure`) — which is the superclass doesn't seem to matter8.6.3https://gitlab.haskell.org/ghc/ghc//issues/15708Crossmodule SPECIALZE pragmas aren't typechecked in O020190707T18:03:21ZregnatCrossmodule SPECIALZE pragmas aren't typechecked in O0If a module defines a `SPECIALIZE` pragma for a value defined in another module, then the signature of this pragma won't be typecheck by `ghc O0` (but it will be if the `SPECIALIZE` pragma is in the same module as the value).
For example, given
```hs
 Foo.hs
module Foo where
foo :: a > a
foo = id

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

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

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

5  {# SPECIALIZE foo :: Int > Bool #}
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
Tested on ghc 8.6.1 and 8.4.3
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Crossmodule SPECIALZE pragmas aren't typechecked in O0","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"If a module defines a `SPECIALIZE` pragma for a value defined in another module, then the signature of this pragma won't be typecheck by `ghc O0` (but it will be if the `SPECIALIZE` pragma is in the same module as the value).\r\n\r\nFor example, given\r\n\r\n{{{#!hs\r\n Foo.hs\r\nmodule Foo where\r\n\r\nfoo :: a > a\r\nfoo = id\r\n\r\n\r\n\r\n Bar.hs\r\nmodule Bar where\r\n\r\nimport Foo\r\n\r\n{# SPECIALIZE foo :: Int > Bool #}\r\n}}}\r\n\r\nrunning `ghc make Bar.hs` will run fine, while `ghc make O2 Bar.hs` will complain:\r\n\r\n{{{\r\nBar.hs:5:1: error:\r\n • Couldn't match type ‘Bool’ with ‘Int’\r\n Expected type: Int > Int\r\n Actual type: Int > Bool\r\n • In the SPECIALISE pragma {# SPECIALIZE foo :: Int > Bool #}\r\n \r\n5  {# SPECIALIZE foo :: Int > Bool #}\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nTested on ghc 8.6.1 and 8.4.3","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/15707More liberally kinded coercions for newtypes20190707T18:03:21ZmniipMore liberally kinded coercions for newtypesConsider the infinite data family (possible thanks to #12369):
```hs
data family I :: k > k
newtype instance I a = I0 (a)
newtype instance I a x = I1 (a x)
newtype instance I a x y = I2 (a x y)
newtype instance I a x y z = I3 (a x y z)
...
```
We end up with a family of etacontracted coercions:
```hs
forall (a :: *). a ~R I a
forall (a :: k > *). a ~R I a
forall (a :: k > l > *). a ~R I a
forall (a :: k > l > m > *). a ~R I a
...
```
What if we could somehow indicate that we desire a polykinded newtype (so to speak) with a coercion `forall (a :: k). a ~R I a`
Maybe even do so by default: `newtype I a = I0 a` would create such a polykinded coercion. Though the `I0` data constructor and pattern would still only use the \*kinded restriction of it.
We could then recover other constructors with:
```hs
i1 :: a x > I a x
i1 = coerce
...
```Consider the infinite data family (possible thanks to #12369):
```hs
data family I :: k > k
newtype instance I a = I0 (a)
newtype instance I a x = I1 (a x)
newtype instance I a x y = I2 (a x y)
newtype instance I a x y z = I3 (a x y z)
...
```
We end up with a family of etacontracted coercions:
```hs
forall (a :: *). a ~R I a
forall (a :: k > *). a ~R I a
forall (a :: k > l > *). a ~R I a
forall (a :: k > l > m > *). a ~R I a
...
```
What if we could somehow indicate that we desire a polykinded newtype (so to speak) with a coercion `forall (a :: k). a ~R I a`
Maybe even do so by default: `newtype I a = I0 a` would create such a polykinded coercion. Though the `I0` data constructor and pattern would still only use the \*kinded restriction of it.
We could then recover other constructors with:
```hs
i1 :: a x > I a x
i1 = coerce
...
```8.6.1https://gitlab.haskell.org/ghc/ghc//issues/15678Provide the provenance of unification variables in error messages when possible20210125T16:36:44ZRyan ScottProvide the provenance of unification variables in error messages when possibleConsider the following code:
```hs
module Foo where
x :: Int
x = const 42 _
```
When compiles, this gives the following suggestion:
```
$ /opt/ghc/8.6.1/bin/ghc Bug.hs
[1 of 1] Compiling Foo ( Bug.hs, Bug.o )
Bug.hs:4:14: error:
• Found hole: _ :: b0
Where: ‘b0’ is an ambiguous type variable
• In the second argument of ‘const’, namely ‘_’
In the expression: const 42 _
In an equation for ‘x’: x = const 42 _
• Relevant bindings include x :: Int (bound at Bug.hs:4:1)
Valid hole fits include
x :: Int (bound at Bug.hs:4:1)
otherwise :: Bool
(imported from ‘Prelude’ at Bug.hs:1:810
(and originally defined in ‘GHC.Base’))
False :: Bool
(imported from ‘Prelude’ at Bug.hs:1:810
(and originally defined in ‘GHC.Types’))
True :: Bool
(imported from ‘Prelude’ at Bug.hs:1:810
(and originally defined in ‘GHC.Types’))
lines :: String > [String]
(imported from ‘Prelude’ at Bug.hs:1:810
(and originally defined in ‘base4.12.0.0:Data.OldList’))
unlines :: [String] > String
(imported from ‘Prelude’ at Bug.hs:1:810
(and originally defined in ‘base4.12.0.0:Data.OldList’))
(Some hole fits suppressed; use fmaxvalidholefits=N or fnomaxvalidholefits)

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

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

8  yeah = yeahCoercible Coercion

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

8  yeah = yeahCoercible Coercion

```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Surprising failure combining QuantifiedConstraints with Coercible","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I don't understand what's going wrong here.\r\n\r\n{{{#!hs\r\n Fishy.hs\r\n{# language RankNTypes, QuantifiedConstraints, RoleAnnotations #}\r\nmodule Fishy (Yeah, yeahCoercible) where\r\nimport Data.Coerce\r\n\r\ndata Yeah_ a = Yeah_ Int\r\nnewtype Yeah a = Yeah (Yeah_ a)\r\ntype role Yeah representational\r\n\r\nyeahCoercible :: ((forall a b. Coercible (Yeah a) (Yeah b)) => r) > r\r\nyeahCoercible r = r\r\n\r\n\r\n Fishy2.hs\r\n\r\nmodule Fishy2 where\r\n\r\nimport Fishy\r\nimport Data.Type.Coercion\r\nimport Data.Coerce\r\n\r\nyeah :: Coercion [Yeah a] [Yeah b]\r\nyeah = yeahCoercible Coercion\r\n}}}\r\n\r\nI get\r\n\r\n{{{\r\nFishy2.hs:8:22: error:\r\n • Couldn't match representation of type ‘a’ with that of ‘b’\r\n arising from a use of ‘Coercion’\r\n ‘a’ is a rigid type variable bound by\r\n the type signature for:\r\n yeah :: forall a b. Coercion [Yeah a] [Yeah b]\r\n at Fishy2.hs:7:134\r\n ‘b’ is a rigid type variable bound by\r\n the type signature for:\r\n yeah :: forall a b. Coercion [Yeah a] [Yeah b]\r\n at Fishy2.hs:7:134\r\n • In the first argument of ‘yeahCoercible’, namely ‘Coercion’\r\n In the expression: yeahCoercible Coercion\r\n In an equation for ‘yeah’: yeah = yeahCoercible Coercion\r\n • Relevant bindings include\r\n yeah :: Coercion [Yeah a] [Yeah b] (bound at Fishy2.hs:8:1)\r\n \r\n8  yeah = yeahCoercible Coercion\r\n \r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >8.6.1https://gitlab.haskell.org/ghc/ghc//issues/15621Error message involving type families points to wrong location20210125T16:37:52ZRyan ScottError message involving type families points to wrong locationConsider the following program:
```hs
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeOperators #}
module Bug where
import Data.Type.Equality
type family F a
f :: ()
f =
let a :: F Int :~: F Int
a = Refl
b :: F Int :~: F Bool
b = Refl
in ()
```
This doesn't typecheck, which isn't surprising, since `F Int` doesn't equal `F Bool` in the definition of `b`. What //is// surprising is where the error message points to:
```
$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:12:11: error:
• Couldn't match type ‘F Int’ with ‘F Bool’
Expected type: F Int :~: F Int
Actual type: F Bool :~: F Bool
NB: ‘F’ is a noninjective type family
• In the expression: Refl
In an equation for ‘a’: a = Refl
In the expression:
let
a :: F Int :~: F Int
a = Refl
b :: F Int :~: F Bool
....
in ()

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

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

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

15  b = Refl
 ^^^^
```
The use of type families appears to be important to triggering this bug, since I can't observe this behavior without the use of `F`.
This is a regression that was introduced at some point between GHC 8.0.2 and 8.2.2, since 8.2.2 gives the incorrect error message shown above, while 8.0.2 points to the right location:
```
$ /opt/ghc/8.0.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:15:11: error:
• Couldn't match type ‘F Int’ with ‘F Bool’
Expected type: F Int :~: F Bool
Actual type: F Int :~: F Int
NB: ‘F’ is a type function, and may not be injective
• In the expression: Refl
In an equation for ‘b’: b = Refl
In the expression:
let
a :: F Int :~: F Int
a = Refl
b :: F Int :~: F Bool
....
in ()
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Error message involving type families points to wrong location","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["TypeFamilies"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider the following program:\r\n\r\n{{{#!hs\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeOperators #}\r\nmodule Bug where\r\n\r\nimport Data.Type.Equality\r\n\r\ntype family F a\r\n\r\nf :: ()\r\nf =\r\n let a :: F Int :~: F Int\r\n a = Refl\r\n\r\n b :: F Int :~: F Bool\r\n b = Refl\r\n in ()\r\n}}}\r\n\r\nThis doesn't typecheck, which isn't surprising, since `F Int` doesn't equal `F Bool` in the definition of `b`. What //is// surprising is where the error message points to:\r\n\r\n{{{\r\n$ /opt/ghc/8.4.3/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:12:11: error:\r\n • Couldn't match type ‘F Int’ with ‘F Bool’\r\n Expected type: F Int :~: F Int\r\n Actual type: F Bool :~: F Bool\r\n NB: ‘F’ is a noninjective type family\r\n • In the expression: Refl\r\n In an equation for ‘a’: a = Refl\r\n In the expression:\r\n let\r\n a :: F Int :~: F Int\r\n a = Refl\r\n b :: F Int :~: F Bool\r\n ....\r\n in ()\r\n \r\n12  a = Refl\r\n  ^^^^\r\n}}}\r\n\r\nThis claims that the error message arises from the definition of `a`, which is completely wrong! As evidence, if you comment out `b`, then the program typechecks again.\r\n\r\nAnother interesting facet of this bug is that if you comment out `a`:\r\n\r\n{{{#!hs\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeOperators #}\r\nmodule Bug where\r\n\r\nimport Data.Type.Equality\r\n\r\ntype family F a\r\n\r\nf :: ()\r\nf =\r\n let { a :: F Int :~: F Int\r\n a = Refl }\r\n\r\n b :: F Int :~: F Bool\r\n b = Refl\r\n in ()\r\n}}}\r\n\r\nThen the error message will actually point to `b` this time:\r\n\r\n{{{\r\n$ /opt/ghc/8.4.3/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:15:11: error:\r\n • Couldn't match type ‘F Int’ with ‘F Bool’\r\n Expected type: F Int :~: F Bool\r\n Actual type: F Bool :~: F Bool\r\n NB: ‘F’ is a noninjective type family\r\n • In the expression: Refl\r\n In an equation for ‘b’: b = Refl\r\n In the expression:\r\n let\r\n b :: F Int :~: F Bool\r\n b = Refl\r\n in ()\r\n \r\n15  b = Refl\r\n  ^^^^\r\n}}}\r\n\r\nThe use of type families appears to be important to triggering this bug, since I can't observe this behavior without the use of `F`.\r\n\r\nThis is a regression that was introduced at some point between GHC 8.0.2 and 8.2.2, since 8.2.2 gives the incorrect error message shown above, while 8.0.2 points to the right location:\r\n\r\n{{{\r\n$ /opt/ghc/8.0.2/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:15:11: error:\r\n • Couldn't match type ‘F Int’ with ‘F Bool’\r\n Expected type: F Int :~: F Bool\r\n Actual type: F Int :~: F Int\r\n NB: ‘F’ is a type function, and may not be injective\r\n • In the expression: Refl\r\n In an equation for ‘b’: b = Refl\r\n In the expression:\r\n let\r\n a :: F Int :~: F Int\r\n a = Refl\r\n b :: F Int :~: F Bool\r\n ....\r\n in ()\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >9.2.1https://gitlab.haskell.org/ghc/ghc//issues/15596When a type application cannot be applied to an identifier due to the absence...20210125T16:37:52ZkindaroWhen a type application cannot be applied to an identifier due to the absence of an explicit type signature, let the error just say so!Consider this code:
```hs
{# language TypeApplications #}
module TypeApplicationsErrorMessage where
f = (+)
g = f @Integer
```
This is what happens when I try to compile it:
```hs
% ghc TypeApplicationsErrorMessage.hs
[1 of 1] Compiling TypeApplicationsErrorMessage ( TypeApplicationsErrorMessage.hs, TypeApplicationsErrorMessage.o )
TypeApplicationsErrorMessage.hs:6:5: error:
• Cannot apply expression of type ‘a0 > a0 > a0’
to a visible type argument ‘Integer’
• In the expression: f @Integer
In an equation for ‘g’: g = f @Integer

6  g = f @Integer
 ^^^^^^^^^^
```
This error is easily fixed by supplying an explicit type signature to `f`. So, perhaps the error message could just say so?
I am observing this with `The Glorious Glasgow Haskell Compilation System, version 8.6.0.20180810`.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  
 Type  FeatureRequest 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"When a type application cannot be applied to an identifier due to the absence of an explicit type signature, let the error just say so!","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"Consider this code:\r\n\r\n{{{#!hs\r\n{# language TypeApplications #}\r\n\r\nmodule TypeApplicationsErrorMessage where\r\n\r\nf = (+)\r\ng = f @Integer\r\n}}}\r\n\r\nThis is what happens when I try to compile it:\r\n\r\n{{{#!hs\r\n% ghc TypeApplicationsErrorMessage.hs\r\n[1 of 1] Compiling TypeApplicationsErrorMessage ( TypeApplicationsErrorMessage.hs, TypeApplicationsErrorMessage.o )\r\n\r\nTypeApplicationsErrorMessage.hs:6:5: error:\r\n • Cannot apply expression of type ‘a0 > a0 > a0’\r\n to a visible type argument ‘Integer’\r\n • In the expression: f @Integer\r\n In an equation for ‘g’: g = f @Integer\r\n \r\n6  g = f @Integer\r\n  ^^^^^^^^^^\r\n}}}\r\n\r\nThis error is easily fixed by supplying an explicit type signature to `f`. So, perhaps the error message could just say so?\r\n\r\nI am observing this with `The Glorious Glasgow Haskell Compilation System, version 8.6.0.20180810`.","type_of_failure":"OtherFailure","blocking":[]} >Consider this code:
```hs
{# language TypeApplications #}
module TypeApplicationsErrorMessage where
f = (+)
g = f @Integer
```
This is what happens when I try to compile it:
```hs
% ghc TypeApplicationsErrorMessage.hs
[1 of 1] Compiling TypeApplicationsErrorMessage ( TypeApplicationsErrorMessage.hs, TypeApplicationsErrorMessage.o )
TypeApplicationsErrorMessage.hs:6:5: error:
• Cannot apply expression of type ‘a0 > a0 > a0’
to a visible type argument ‘Integer’
• In the expression: f @Integer
In an equation for ‘g’: g = f @Integer

6  g = f @Integer
 ^^^^^^^^^^
```
This error is easily fixed by supplying an explicit type signature to `f`. So, perhaps the error message could just say so?
I am observing this with `The Glorious Glasgow Haskell Compilation System, version 8.6.0.20180810`.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  
 Type  FeatureRequest 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"When a type application cannot be applied to an identifier due to the absence of an explicit type signature, let the error just say so!","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"Consider this code:\r\n\r\n{{{#!hs\r\n{# language TypeApplications #}\r\n\r\nmodule TypeApplicationsErrorMessage where\r\n\r\nf = (+)\r\ng = f @Integer\r\n}}}\r\n\r\nThis is what happens when I try to compile it:\r\n\r\n{{{#!hs\r\n% ghc TypeApplicationsErrorMessage.hs\r\n[1 of 1] Compiling TypeApplicationsErrorMessage ( TypeApplicationsErrorMessage.hs, TypeApplicationsErrorMessage.o )\r\n\r\nTypeApplicationsErrorMessage.hs:6:5: error:\r\n • Cannot apply expression of type ‘a0 > a0 > a0’\r\n to a visible type argument ‘Integer’\r\n • In the expression: f @Integer\r\n In an equation for ‘g’: g = f @Integer\r\n \r\n6  g = f @Integer\r\n  ^^^^^^^^^^\r\n}}}\r\n\r\nThis error is easily fixed by supplying an explicit type signature to `f`. So, perhaps the error message could just say so?\r\n\r\nI am observing this with `The Glorious Glasgow Haskell Compilation System, version 8.6.0.20180810`.","type_of_failure":"OtherFailure","blocking":[]} >9.2.1https://gitlab.haskell.org/ghc/ghc//issues/15557Reduce type families in equations' RHS when testing equation compatibility20190707T18:04:08ZmniipReduce type families in equations' RHS when testing equation compatibilityThe reference I found for closed type families with compatible equations is: https://www.microsoft.com/enus/research/wpcontent/uploads/2016/07/popl137eisenberg.pdf
There in Definition 8 in section 3.4 it states:
Definition 8 (Compatibility implementation). The test for compatibility, written compat(p, q), checks that unify(lhsp, lhsq) = Ω implies Ω(rhsp) = Ω(rhsq). If unify(lhsp, lhsq) fails, compat(p, q) holds vacuously.
Examine the following families:
```hs
type family If (a :: Bool) (b :: k) (c :: k) :: k where
If False a b = b
If True a b = a
type family Eql (a :: k) (b :: k) :: Bool where
Eql a a = True
Eql _ _ = False
type family Test (a :: Maybe k) (b :: Maybe k) :: Maybe k where
Test (Just x) (Just y) = If (Eql x y) (Just x) Nothing
Test a a = a
Test Nothing _ = Nothing
Test _ Nothing = Nothing
```
Applying the check to the equations 1 and 2 of `Test` we get:
unify(\<`Just x`, `Just y`\>, \<`a`, `a`\>) = Ω = \[`a` \> `Just x`, `y` \> `x`\]
Ω(`a`) = `Just x` = `If (Eql x x) (Just x) Nothing` = Ω(`If (Eql x y) (Just x) Nothing`)
Therefore the equations must be compatible, and when tidying `forall a. p a > p (Test a a)` the application should reduce to `forall a. p a > p a`
That doesn't happen:
```hs
> :t undefined :: p a > p (Test a a)
p a > p (Test a a)
```
Examining the IfaceAxBranches (cf #15546) we see:
```hs
axiom D:R:Test::
Test a ('Just x) ('Just y) = If (Eql x y) ('Just x) 'Nothing
Test k a a = a
(incompatible indices: [0])
Test k 'Nothing _ = 'Nothing
Test k _ 'Nothing = 'Nothing
```
GHC did not consider the two equations compatible.
Digging into why, I came across this ticket: #8423, in which a potentially unbounded (and indefinite) number of type family reductions was necessary to evidence Ω(rhsp) = Ω(rhsq). I don't claim to fully understand goldfire's [ticket:8423\#comment:80951](https://gitlab.haskell.org//ghc/ghc/issues/8423#note_80951), but the issue is clear: reducing type families while doing a compartibility check might depend on other compatibility checks already being done, including a check depending on itself in which case we are interested in the biggest fixed point (why?).
The family here doesn't require any of that special consideration because `Eql x x` reduces right away without any compatibility checks, and `If` is essentially open (indeed making `If` open doesn't help anything).
This brings the question: is something like goldfire's described algorithm (or a simplification thereof) something we would like to have in GHC or is that too complex? What is the status on the implementation of that algorithm?
P.S: An interesting workaround is adding an `If t c c = c` equation (compatible), and then writing `Test` as:
```hs
type family Test (a :: Maybe k) (b :: Maybe k) :: Maybe k where
Test (Just x) (Just y) = If (Eql (Just x) (Just y)) (Just x) Nothing
Test a a = If (Eql a a) a Nothing
Test Nothing a = If (Eql Nothing a) Nothing Nothing
Test a Nothing = If (Eql a Nothing) Nothing Nothing
```
This lets GHC discover the necessary equalities without reducing type families, yet erase the workaround'ed type family applications immediately.
P.P.S: In [ticket:15546\#comment:158797](https://gitlab.haskell.org//ghc/ghc/issues/15546#note_158797) I mixed up left and right, it's the RHS that should be/are not reduced. This probably confused SPJ a lot.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.3 
 Type  FeatureRequest 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  goldfire, simonpj 
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Reduce type families in equations' RHS when testing equation compatibility","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["TypeFamilies"],"differentials":[],"test_case":"","architecture":"","cc":["goldfire","simonpj"],"type":"FeatureRequest","description":"The reference I found for closed type families with compatible equations is: https://www.microsoft.com/enus/research/wpcontent/uploads/2016/07/popl137eisenberg.pdf\r\n\r\nThere in Definition 8 in section 3.4 it states:\r\n\r\nDefinition 8 (Compatibility implementation). The test for compatibility, written compat(p, q), checks that unify(lhsp, lhsq) = Ω implies Ω(rhsp) = Ω(rhsq). If unify(lhsp, lhsq) fails, compat(p, q) holds vacuously.\r\n\r\nExamine the following families:\r\n\r\n{{{#!hs\r\ntype family If (a :: Bool) (b :: k) (c :: k) :: k where\r\n If False a b = b\r\n If True a b = a\r\n\r\ntype family Eql (a :: k) (b :: k) :: Bool where\r\n Eql a a = True\r\n Eql _ _ = False\r\n\r\ntype family Test (a :: Maybe k) (b :: Maybe k) :: Maybe k where\r\n Test (Just x) (Just y) = If (Eql x y) (Just x) Nothing\r\n Test a a = a\r\n Test Nothing _ = Nothing\r\n Test _ Nothing = Nothing\r\n}}}\r\n\r\nApplying the check to the equations 1 and 2 of `Test` we get:\r\n\r\nunify(<`Just x`, `Just y`>, <`a`, `a`>) = Ω = [`a` > `Just x`, `y` > `x`]\r\n\r\nΩ(`a`) = `Just x` = `If (Eql x x) (Just x) Nothing` = Ω(`If (Eql x y) (Just x) Nothing`)\r\n\r\nTherefore the equations must be compatible, and when tidying `forall a. p a > p (Test a a)` the application should reduce to `forall a. p a > p a`\r\n\r\nThat doesn't happen:\r\n{{{#!hs\r\n> :t undefined :: p a > p (Test a a)\r\np a > p (Test a a)\r\n}}}\r\n\r\nExamining the IfaceAxBranches (cf #15546) we see:\r\n{{{#!hs\r\n axiom D:R:Test::\r\n Test a ('Just x) ('Just y) = If (Eql x y) ('Just x) 'Nothing\r\n Test k a a = a\r\n (incompatible indices: [0])\r\n Test k 'Nothing _ = 'Nothing\r\n Test k _ 'Nothing = 'Nothing\r\n}}}\r\n\r\nGHC did not consider the two equations compatible.\r\n\r\nDigging into why, I came across this ticket: #8423, in which a potentially unbounded (and indefinite) number of type family reductions was necessary to evidence Ω(rhsp) = Ω(rhsq). I don't claim to fully understand goldfire's ticket:8423#comment:10, but the issue is clear: reducing type families while doing a compartibility check might depend on other compatibility checks already being done, including a check depending on itself in which case we are interested in the biggest fixed point (why?).\r\n\r\nThe family here doesn't require any of that special consideration because `Eql x x` reduces right away without any compatibility checks, and `If` is essentially open (indeed making `If` open doesn't help anything).\r\n\r\nThis brings the question: is something like goldfire's described algorithm (or a simplification thereof) something we would like to have in GHC or is that too complex? What is the status on the implementation of that algorithm?\r\n\r\nP.S: An interesting workaround is adding an `If t c c = c` equation (compatible), and then writing `Test` as:\r\n{{{#!hs\r\ntype family Test (a :: Maybe k) (b :: Maybe k) :: Maybe k where\r\n Test (Just x) (Just y) = If (Eql (Just x) (Just y)) (Just x) Nothing\r\n Test a a = If (Eql a a) a Nothing\r\n Test Nothing a = If (Eql Nothing a) Nothing Nothing\r\n Test a Nothing = If (Eql a Nothing) Nothing Nothing\r\n}}}\r\n\r\nThis lets GHC discover the necessary equalities without reducing type families, yet erase the workaround'ed type family applications immediately.\r\n\r\nP.P.S: In ticket:15546#comment:4 I mixed up left and right, it's the RHS that should be/are not reduced. This probably confused SPJ a lot.","type_of_failure":"OtherFailure","blocking":[]} >The reference I found for closed type families with compatible equations is: https://www.microsoft.com/enus/research/wpcontent/uploads/2016/07/popl137eisenberg.pdf
There in Definition 8 in section 3.4 it states:
Definition 8 (Compatibility implementation). The test for compatibility, written compat(p, q), checks that unify(lhsp, lhsq) = Ω implies Ω(rhsp) = Ω(rhsq). If unify(lhsp, lhsq) fails, compat(p, q) holds vacuously.
Examine the following families:
```hs
type family If (a :: Bool) (b :: k) (c :: k) :: k where
If False a b = b
If True a b = a
type family Eql (a :: k) (b :: k) :: Bool where
Eql a a = True
Eql _ _ = False
type family Test (a :: Maybe k) (b :: Maybe k) :: Maybe k where
Test (Just x) (Just y) = If (Eql x y) (Just x) Nothing
Test a a = a
Test Nothing _ = Nothing
Test _ Nothing = Nothing
```
Applying the check to the equations 1 and 2 of `Test` we get:
unify(\<`Just x`, `Just y`\>, \<`a`, `a`\>) = Ω = \[`a` \> `Just x`, `y` \> `x`\]
Ω(`a`) = `Just x` = `If (Eql x x) (Just x) Nothing` = Ω(`If (Eql x y) (Just x) Nothing`)
Therefore the equations must be compatible, and when tidying `forall a. p a > p (Test a a)` the application should reduce to `forall a. p a > p a`
That doesn't happen:
```hs
> :t undefined :: p a > p (Test a a)
p a > p (Test a a)
```
Examining the IfaceAxBranches (cf #15546) we see:
```hs
axiom D:R:Test::
Test a ('Just x) ('Just y) = If (Eql x y) ('Just x) 'Nothing
Test k a a = a
(incompatible indices: [0])
Test k 'Nothing _ = 'Nothing
Test k _ 'Nothing = 'Nothing
```
GHC did not consider the two equations compatible.
Digging into why, I came across this ticket: #8423, in which a potentially unbounded (and indefinite) number of type family reductions was necessary to evidence Ω(rhsp) = Ω(rhsq). I don't claim to fully understand goldfire's [ticket:8423\#comment:80951](https://gitlab.haskell.org//ghc/ghc/issues/8423#note_80951), but the issue is clear: reducing type families while doing a compartibility check might depend on other compatibility checks already being done, including a check depending on itself in which case we are interested in the biggest fixed point (why?).
The family here doesn't require any of that special consideration because `Eql x x` reduces right away without any compatibility checks, and `If` is essentially open (indeed making `If` open doesn't help anything).
This brings the question: is something like goldfire's described algorithm (or a simplification thereof) something we would like to have in GHC or is that too complex? What is the status on the implementation of that algorithm?
P.S: An interesting workaround is adding an `If t c c = c` equation (compatible), and then writing `Test` as:
```hs
type family Test (a :: Maybe k) (b :: Maybe k) :: Maybe k where
Test (Just x) (Just y) = If (Eql (Just x) (Just y)) (Just x) Nothing
Test a a = If (Eql a a) a Nothing
Test Nothing a = If (Eql Nothing a) Nothing Nothing
Test a Nothing = If (Eql a Nothing) Nothing Nothing
```
This lets GHC discover the necessary equalities without reducing type families, yet erase the workaround'ed type family applications immediately.
P.P.S: In [ticket:15546\#comment:158797](https://gitlab.haskell.org//ghc/ghc/issues/15546#note_158797) I mixed up left and right, it's the RHS that should be/are not reduced. This probably confused SPJ a lot.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.3 
 Type  FeatureRequest 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  goldfire, simonpj 
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Reduce type families in equations' RHS when testing equation compatibility","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["TypeFamilies"],"differentials":[],"test_case":"","architecture":"","cc":["goldfire","simonpj"],"type":"FeatureRequest","description":"The reference I found for closed type families with compatible equations is: https://www.microsoft.com/enus/research/wpcontent/uploads/2016/07/popl137eisenberg.pdf\r\n\r\nThere in Definition 8 in section 3.4 it states:\r\n\r\nDefinition 8 (Compatibility implementation). The test for compatibility, written compat(p, q), checks that unify(lhsp, lhsq) = Ω implies Ω(rhsp) = Ω(rhsq). If unify(lhsp, lhsq) fails, compat(p, q) holds vacuously.\r\n\r\nExamine the following families:\r\n\r\n{{{#!hs\r\ntype family If (a :: Bool) (b :: k) (c :: k) :: k where\r\n If False a b = b\r\n If True a b = a\r\n\r\ntype family Eql (a :: k) (b :: k) :: Bool where\r\n Eql a a = True\r\n Eql _ _ = False\r\n\r\ntype family Test (a :: Maybe k) (b :: Maybe k) :: Maybe k where\r\n Test (Just x) (Just y) = If (Eql x y) (Just x) Nothing\r\n Test a a = a\r\n Test Nothing _ = Nothing\r\n Test _ Nothing = Nothing\r\n}}}\r\n\r\nApplying the check to the equations 1 and 2 of `Test` we get:\r\n\r\nunify(<`Just x`, `Just y`>, <`a`, `a`>) = Ω = [`a` > `Just x`, `y` > `x`]\r\n\r\nΩ(`a`) = `Just x` = `If (Eql x x) (Just x) Nothing` = Ω(`If (Eql x y) (Just x) Nothing`)\r\n\r\nTherefore the equations must be compatible, and when tidying `forall a. p a > p (Test a a)` the application should reduce to `forall a. p a > p a`\r\n\r\nThat doesn't happen:\r\n{{{#!hs\r\n> :t undefined :: p a > p (Test a a)\r\np a > p (Test a a)\r\n}}}\r\n\r\nExamining the IfaceAxBranches (cf #15546) we see:\r\n{{{#!hs\r\n axiom D:R:Test::\r\n Test a ('Just x) ('Just y) = If (Eql x y) ('Just x) 'Nothing\r\n Test k a a = a\r\n (incompatible indices: [0])\r\n Test k 'Nothing _ = 'Nothing\r\n Test k _ 'Nothing = 'Nothing\r\n}}}\r\n\r\nGHC did not consider the two equations compatible.\r\n\r\nDigging into why, I came across this ticket: #8423, in which a potentially unbounded (and indefinite) number of type family reductions was necessary to evidence Ω(rhsp) = Ω(rhsq). I don't claim to fully understand goldfire's ticket:8423#comment:10, but the issue is clear: reducing type families while doing a compartibility check might depend on other compatibility checks already being done, including a check depending on itself in which case we are interested in the biggest fixed point (why?).\r\n\r\nThe family here doesn't require any of that special consideration because `Eql x x` reduces right away without any compatibility checks, and `If` is essentially open (indeed making `If` open doesn't help anything).\r\n\r\nThis brings the question: is something like goldfire's described algorithm (or a simplification thereof) something we would like to have in GHC or is that too complex? What is the status on the implementation of that algorithm?\r\n\r\nP.S: An interesting workaround is adding an `If t c c = c` equation (compatible), and then writing `Test` as:\r\n{{{#!hs\r\ntype family Test (a :: Maybe k) (b :: Maybe k) :: Maybe k where\r\n Test (Just x) (Just y) = If (Eql (Just x) (Just y)) (Just x) Nothing\r\n Test a a = If (Eql a a) a Nothing\r\n Test Nothing a = If (Eql Nothing a) Nothing Nothing\r\n Test a Nothing = If (Eql a Nothing) Nothing Nothing\r\n}}}\r\n\r\nThis lets GHC discover the necessary equalities without reducing type families, yet erase the workaround'ed type family applications immediately.\r\n\r\nP.P.S: In ticket:15546#comment:4 I mixed up left and right, it's the RHS that should be/are not reduced. This probably confused SPJ a lot.","type_of_failure":"OtherFailure","blocking":[]} >8.6.1https://gitlab.haskell.org/ghc/ghc//issues/15416Higher rank types in pattern synonyms20210123T01:13:41ZmniipHigher rank types in pattern synonyms```hs
{# LANGUAGE RankNTypes, PatternSynonyms, ViewPatterns #}
```
Consider the following two pattern synonyms:
```hs
pattern N :: () => () => forall r. r > (a > r) > r
pattern N < ((\f > f Nothing Just) > Nothing) where N = \n j > n
pattern J :: a > forall r. r > (a > r) > r
pattern J x < ((\f > f Nothing Just) > Just x) where J x = \n j > j x
```
The pattern synonym type declaration syntax is very fragile and awkward wrt quantifiers but that's a story for another ticket.
Now consider four ways to write the same function: using pattern synonyms we've defined above vs. using the exact view patterns they were defiend with; and using a series of equations vs. an explicit `case of`:
```hs
fooVPEqns, fooVPCase, fooPSEqns, fooPSCase :: (forall r. r > (a > r) > r) > Maybe a
fooVPEqns ((\f > f Nothing Just) > Nothing) = Nothing
fooVPEqns ((\f > f Nothing Just) > Just x) = Just x
fooVPCase v = case v of
((\f > f Nothing Just) > Nothing) > Nothing
((\f > f Nothing Just) > Just x) > Just x
fooPSEqns N = Nothing
fooPSEqns (J x) = Just x
fooPSCase v = case v of
N > Nothing
J x > Just x
```
Three of these compile and work fine, the fourth breaks:
```hs
QuantPatSyn.hs:22:9: error:
• Couldn't match expected type ‘r0 > (a > r0) > r0’
with actual type ‘forall r. r > (a0 > r) > r’
• In the pattern: N
In a case alternative: N > Nothing
In the expression:
case v of
N > Nothing
J x > Just x
• Relevant bindings include
v :: forall r. r > (a > r) > r (bound at QuantPatSyn.hs:21:11)
fooPSCase :: (forall r. r > (a > r) > r) > Maybe a
(bound at QuantPatSyn.hs:21:1)

22  N > Nothing
 ^
QuantPatSyn.hs:23:9: error:
• Couldn't match expected type ‘r0 > (a > r0) > r0’
with actual type ‘forall r. r > (a > r) > r’
• In the pattern: J x
In a case alternative: J x > Just x
In the expression:
case v of
N > Nothing
J x > Just x
• Relevant bindings include
v :: forall r. r > (a > r) > r (bound at QuantPatSyn.hs:21:11)
fooPSCase :: (forall r. r > (a > r) > r) > Maybe a
(bound at QuantPatSyn.hs:21:1)

23  J x > Just x
 ^^^
```
The exact wording of the error message (the appearance of `forall` in the "actual type") makes me think this is an error on the typechecker's side: the part of the typechecker that handles pattern synonyms doesn't handle higher rank types correctly.
Another symptom can be observed with the following:
```hs
pattern V :: Void > (forall r. r)
pattern V x < ((\f > f) > x) where V x = absurd x
barVPEqns, barVPCase, barPSEqns, barPSCase :: (forall r. r) > Void
barVPEqns ((\f > f) > x) = x
barVPCase v = case v of
((\f > f) > x) > x
barPSEqns (V x) = x
barPSCase v = case v of
V x > x
```
```hs
QuantPatSyn.hs:43:9: error:
• Cannot instantiate unification variable ‘r0’
with a type involving foralls: forall r. r
GHC doesn't yet support impredicative polymorphism
• In the pattern: V x
In a case alternative: V x > x
In the expression: case v of { V x > x }

43  V x > x
 ^^^
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Higher rank types in pattern synonyms","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["PatternSynonyms"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{# LANGUAGE RankNTypes, PatternSynonyms, ViewPatterns #}\r\n}}}\r\nConsider the following two pattern synonyms:\r\n\r\n{{{#!hs\r\npattern N :: () => () => forall r. r > (a > r) > r\r\npattern N < ((\\f > f Nothing Just) > Nothing) where N = \\n j > n\r\n\r\npattern J :: a > forall r. r > (a > r) > r\r\npattern J x < ((\\f > f Nothing Just) > Just x) where J x = \\n j > j x\r\n}}}\r\n\r\nThe pattern synonym type declaration syntax is very fragile and awkward wrt quantifiers but that's a story for another ticket.\r\n\r\nNow consider four ways to write the same function: using pattern synonyms we've defined above vs. using the exact view patterns they were defiend with; and using a series of equations vs. an explicit `case of`:\r\n\r\n{{{#!hs\r\nfooVPEqns, fooVPCase, fooPSEqns, fooPSCase :: (forall r. r > (a > r) > r) > Maybe a\r\n\r\nfooVPEqns ((\\f > f Nothing Just) > Nothing) = Nothing\r\nfooVPEqns ((\\f > f Nothing Just) > Just x) = Just x\r\n\r\nfooVPCase v = case v of\r\n\t((\\f > f Nothing Just) > Nothing) > Nothing\r\n\t((\\f > f Nothing Just) > Just x) > Just x\r\n\r\nfooPSEqns N = Nothing\r\nfooPSEqns (J x) = Just x\r\n\r\nfooPSCase v = case v of\r\n\tN > Nothing\r\n\tJ x > Just x\r\n}}}\r\n\r\nThree of these compile and work fine, the fourth breaks:\r\n{{{#!hs\r\nQuantPatSyn.hs:22:9: error:\r\n • Couldn't match expected type ‘r0 > (a > r0) > r0’\r\n with actual type ‘forall r. r > (a0 > r) > r’\r\n • In the pattern: N\r\n In a case alternative: N > Nothing\r\n In the expression:\r\n case v of\r\n N > Nothing\r\n J x > Just x\r\n • Relevant bindings include\r\n v :: forall r. r > (a > r) > r (bound at QuantPatSyn.hs:21:11)\r\n fooPSCase :: (forall r. r > (a > r) > r) > Maybe a\r\n (bound at QuantPatSyn.hs:21:1)\r\n \r\n22  N > Nothing\r\n  ^\r\n\r\nQuantPatSyn.hs:23:9: error:\r\n • Couldn't match expected type ‘r0 > (a > r0) > r0’\r\n with actual type ‘forall r. r > (a > r) > r’\r\n • In the pattern: J x\r\n In a case alternative: J x > Just x\r\n In the expression:\r\n case v of\r\n N > Nothing\r\n J x > Just x\r\n • Relevant bindings include\r\n v :: forall r. r > (a > r) > r (bound at QuantPatSyn.hs:21:11)\r\n fooPSCase :: (forall r. r > (a > r) > r) > Maybe a\r\n (bound at QuantPatSyn.hs:21:1)\r\n \r\n23  J x > Just x\r\n  ^^^\r\n}}}\r\n\r\nThe exact wording of the error message (the appearance of `forall` in the \"actual type\") makes me think this is an error on the typechecker's side: the part of the typechecker that handles pattern synonyms doesn't handle higher rank types correctly.\r\n\r\nAnother symptom can be observed with the following:\r\n\r\n{{{#!hs\r\npattern V :: Void > (forall r. r)\r\npattern V x < ((\\f > f) > x) where V x = absurd x\r\n\r\nbarVPEqns, barVPCase, barPSEqns, barPSCase :: (forall r. r) > Void\r\n\r\nbarVPEqns ((\\f > f) > x) = x\r\n\r\nbarVPCase v = case v of\r\n\t((\\f > f) > x) > x\r\n\r\nbarPSEqns (V x) = x\r\n\r\nbarPSCase v = case v of\r\n\tV x > x\r\n}}}\r\n{{{#!hs\r\nQuantPatSyn.hs:43:9: error:\r\n • Cannot instantiate unification variable ‘r0’\r\n with a type involving foralls: forall r. r\r\n GHC doesn't yet support impredicative polymorphism\r\n • In the pattern: V x\r\n In a case alternative: V x > x\r\n In the expression: case v of { V x > x }\r\n \r\n43  V x > x\r\n  ^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >```hs
{# LANGUAGE RankNTypes, PatternSynonyms, ViewPatterns #}
```
Consider the following two pattern synonyms:
```hs
pattern N :: () => () => forall r. r > (a > r) > r
pattern N < ((\f > f Nothing Just) > Nothing) where N = \n j > n
pattern J :: a > forall r. r > (a > r) > r
pattern J x < ((\f > f Nothing Just) > Just x) where J x = \n j > j x
```
The pattern synonym type declaration syntax is very fragile and awkward wrt quantifiers but that's a story for another ticket.
Now consider four ways to write the same function: using pattern synonyms we've defined above vs. using the exact view patterns they were defiend with; and using a series of equations vs. an explicit `case of`:
```hs
fooVPEqns, fooVPCase, fooPSEqns, fooPSCase :: (forall r. r > (a > r) > r) > Maybe a
fooVPEqns ((\f > f Nothing Just) > Nothing) = Nothing
fooVPEqns ((\f > f Nothing Just) > Just x) = Just x
fooVPCase v = case v of
((\f > f Nothing Just) > Nothing) > Nothing
((\f > f Nothing Just) > Just x) > Just x
fooPSEqns N = Nothing
fooPSEqns (J x) = Just x
fooPSCase v = case v of
N > Nothing
J x > Just x
```
Three of these compile and work fine, the fourth breaks:
```hs
QuantPatSyn.hs:22:9: error:
• Couldn't match expected type ‘r0 > (a > r0) > r0’
with actual type ‘forall r. r > (a0 > r) > r’
• In the pattern: N
In a case alternative: N > Nothing
In the expression:
case v of
N > Nothing
J x > Just x
• Relevant bindings include
v :: forall r. r > (a > r) > r (bound at QuantPatSyn.hs:21:11)
fooPSCase :: (forall r. r > (a > r) > r) > Maybe a
(bound at QuantPatSyn.hs:21:1)

22  N > Nothing
 ^
QuantPatSyn.hs:23:9: error:
• Couldn't match expected type ‘r0 > (a > r0) > r0’
with actual type ‘forall r. r > (a > r) > r’
• In the pattern: J x
In a case alternative: J x > Just x
In the expression:
case v of
N > Nothing
J x > Just x
• Relevant bindings include
v :: forall r. r > (a > r) > r (bound at QuantPatSyn.hs:21:11)
fooPSCase :: (forall r. r > (a > r) > r) > Maybe a
(bound at QuantPatSyn.hs:21:1)

23  J x > Just x
 ^^^
```
The exact wording of the error message (the appearance of `forall` in the "actual type") makes me think this is an error on the typechecker's side: the part of the typechecker that handles pattern synonyms doesn't handle higher rank types correctly.
Another symptom can be observed with the following:
```hs
pattern V :: Void > (forall r. r)
pattern V x < ((\f > f) > x) where V x = absurd x
barVPEqns, barVPCase, barPSEqns, barPSCase :: (forall r. r) > Void
barVPEqns ((\f > f) > x) = x
barVPCase v = case v of
((\f > f) > x) > x
barPSEqns (V x) = x
barPSCase v = case v of
V x > x
```
```hs
QuantPatSyn.hs:43:9: error:
• Cannot instantiate unification variable ‘r0’
with a type involving foralls: forall r. r
GHC doesn't yet support impredicative polymorphism
• In the pattern: V x
In a case alternative: V x > x
In the expression: case v of { V x > x }

43  V x > x
 ^^^
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Higher rank types in pattern synonyms","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["PatternSynonyms"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{# LANGUAGE RankNTypes, PatternSynonyms, ViewPatterns #}\r\n}}}\r\nConsider the following two pattern synonyms:\r\n\r\n{{{#!hs\r\npattern N :: () => () => forall r. r > (a > r) > r\r\npattern N < ((\\f > f Nothing Just) > Nothing) where N = \\n j > n\r\n\r\npattern J :: a > forall r. r > (a > r) > r\r\npattern J x < ((\\f > f Nothing Just) > Just x) where J x = \\n j > j x\r\n}}}\r\n\r\nThe pattern synonym type declaration syntax is very fragile and awkward wrt quantifiers but that's a story for another ticket.\r\n\r\nNow consider four ways to write the same function: using pattern synonyms we've defined above vs. using the exact view patterns they were defiend with; and using a series of equations vs. an explicit `case of`:\r\n\r\n{{{#!hs\r\nfooVPEqns, fooVPCase, fooPSEqns, fooPSCase :: (forall r. r > (a > r) > r) > Maybe a\r\n\r\nfooVPEqns ((\\f > f Nothing Just) > Nothing) = Nothing\r\nfooVPEqns ((\\f > f Nothing Just) > Just x) = Just x\r\n\r\nfooVPCase v = case v of\r\n\t((\\f > f Nothing Just) > Nothing) > Nothing\r\n\t((\\f > f Nothing Just) > Just x) > Just x\r\n\r\nfooPSEqns N = Nothing\r\nfooPSEqns (J x) = Just x\r\n\r\nfooPSCase v = case v of\r\n\tN > Nothing\r\n\tJ x > Just x\r\n}}}\r\n\r\nThree of these compile and work fine, the fourth breaks:\r\n{{{#!hs\r\nQuantPatSyn.hs:22:9: error:\r\n • Couldn't match expected type ‘r0 > (a > r0) > r0’\r\n with actual type ‘forall r. r > (a0 > r) > r’\r\n • In the pattern: N\r\n In a case alternative: N > Nothing\r\n In the expression:\r\n case v of\r\n N > Nothing\r\n J x > Just x\r\n • Relevant bindings include\r\n v :: forall r. r > (a > r) > r (bound at QuantPatSyn.hs:21:11)\r\n fooPSCase :: (forall r. r > (a > r) > r) > Maybe a\r\n (bound at QuantPatSyn.hs:21:1)\r\n \r\n22  N > Nothing\r\n  ^\r\n\r\nQuantPatSyn.hs:23:9: error:\r\n • Couldn't match expected type ‘r0 > (a > r0) > r0’\r\n with actual type ‘forall r. r > (a > r) > r’\r\n • In the pattern: J x\r\n In a case alternative: J x > Just x\r\n In the expression:\r\n case v of\r\n N > Nothing\r\n J x > Just x\r\n • Relevant bindings include\r\n v :: forall r. r > (a > r) > r (bound at QuantPatSyn.hs:21:11)\r\n fooPSCase :: (forall r. r > (a > r) > r) > Maybe a\r\n (bound at QuantPatSyn.hs:21:1)\r\n \r\n23  J x > Just x\r\n  ^^^\r\n}}}\r\n\r\nThe exact wording of the error message (the appearance of `forall` in the \"actual type\") makes me think this is an error on the typechecker's side: the part of the typechecker that handles pattern synonyms doesn't handle higher rank types correctly.\r\n\r\nAnother symptom can be observed with the following:\r\n\r\n{{{#!hs\r\npattern V :: Void > (forall r. r)\r\npattern V x < ((\\f > f) > x) where V x = absurd x\r\n\r\nbarVPEqns, barVPCase, barPSEqns, barPSCase :: (forall r. r) > Void\r\n\r\nbarVPEqns ((\\f > f) > x) = x\r\n\r\nbarVPCase v = case v of\r\n\t((\\f > f) > x) > x\r\n\r\nbarPSEqns (V x) = x\r\n\r\nbarPSCase v = case v of\r\n\tV x > x\r\n}}}\r\n{{{#!hs\r\nQuantPatSyn.hs:43:9: error:\r\n • Cannot instantiate unification variable ‘r0’\r\n with a type involving foralls: forall r. r\r\n GHC doesn't yet support impredicative polymorphism\r\n • In the pattern: V x\r\n In a case alternative: V x > x\r\n In the expression: case v of { V x > x }\r\n \r\n43  V x > x\r\n  ^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >9.2.1https://gitlab.haskell.org/ghc/ghc//issues/15351QuantifiedConstraints ignore FunctionalDependencies20201203T08:24:56ZaaronvargoQuantifiedConstraints ignore FunctionalDependenciesThe following code fails to compile:
```hs
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE FunctionalDependencies #}
class C a b  a > b where
foo :: a > b
bar :: (forall a. C (f a) Int) => f a > String
bar = show . foo
```
```
• Could not deduce (Show a0) arising from a use of ‘show’
...
The type variable ‘a0’ is ambiguous
• Could not deduce (C (f a) a0) arising from a use of ‘foo’
...
The type variable ‘a0’ is ambiguous
```
Yet it ought to work, since this is perfectly fine with toplevel instances:
```hs
instance C [a] Int where ...
baz :: [a] > String
baz = show . foo
```The following code fails to compile:
```hs
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE FunctionalDependencies #}
class C a b  a > b where
foo :: a > b
bar :: (forall a. C (f a) Int) => f a > String
bar = show . foo
```
```
• Could not deduce (Show a0) arising from a use of ‘show’
...
The type variable ‘a0’ is ambiguous
• Could not deduce (C (f a) a0) arising from a use of ‘foo’
...
The type variable ‘a0’ is ambiguous
```
Yet it ought to work, since this is perfectly fine with toplevel instances:
```hs
instance C [a] Int where ...
baz :: [a] > String
baz = show . foo
```https://gitlab.haskell.org/ghc/ghc//issues/15347QuantifiedConstraints: Implication constraints with type families don't work20190918T06:46:06ZaaronvargoQuantifiedConstraints: Implication constraints with type families don't workThis may be related to #14860, but I think it's different.
The following code fails to compile:
```hs
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE AllowAmbiguousTypes #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE GADTs #}
{# LANGUAGE ConstraintKinds #}
import Prelude()
import Data.Kind
data Dict c = c => Dict
type family F a :: Constraint
foo :: forall a b. (a => F b, a) => Dict (F b)
foo = Dict
```
```
• Could not deduce: F b arising from a use of ‘Dict’
from the context: (a => F b, a)
```
Yet the following all do compile:
```hs
bar :: forall a. F a => Dict (F a)
bar = Dict
baz :: forall a b. (a => b, a) => Dict b
baz = Dict
qux :: forall a b c. (a => c, a, c ~ F b) => Dict (F b)
qux = Dict
```
It seems that a wanted `F b` can be solved with a given `F b`, but not with a given `a => F b`, which is bizarre. The fact that `qux` still works is also strange, as it means that you get a different result if you first simplify by substituting `c = F b`.
As a more practical example, the following similarly fails to compile, due to the `Cod f` type family:
```hs
 in addition to the above extensions
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE FunctionalDependencies #}
class Ob p a
class (forall a. Ob (Dom f) a => Ob (Cod f) (f a)) => Functor f where
type Dom f
type Cod f
liftOb :: forall f a. (Functor f, Ob (Dom f) a) => Dict (Ob (Cod f) (f a))
liftOb = Dict
```
While a version which uses fundeps instead does compile:
```hs
class (forall a. Ob dom a => Ob cod (f a)) => Functor dom cod f  f > dom cod
liftOb :: forall f a dom cod. (Functor dom cod f, Ob dom a) => Dict (Ob cod (f a))
liftOb = Dict
```This may be related to #14860, but I think it's different.
The following code fails to compile:
```hs
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE AllowAmbiguousTypes #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE GADTs #}
{# LANGUAGE ConstraintKinds #}
import Prelude()
import Data.Kind
data Dict c = c => Dict
type family F a :: Constraint
foo :: forall a b. (a => F b, a) => Dict (F b)
foo = Dict
```
```
• Could not deduce: F b arising from a use of ‘Dict’
from the context: (a => F b, a)
```
Yet the following all do compile:
```hs
bar :: forall a. F a => Dict (F a)
bar = Dict
baz :: forall a b. (a => b, a) => Dict b
baz = Dict
qux :: forall a b c. (a => c, a, c ~ F b) => Dict (F b)
qux = Dict
```
It seems that a wanted `F b` can be solved with a given `F b`, but not with a given `a => F b`, which is bizarre. The fact that `qux` still works is also strange, as it means that you get a different result if you first simplify by substituting `c = F b`.
As a more practical example, the following similarly fails to compile, due to the `Cod f` type family:
```hs
 in addition to the above extensions
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE FunctionalDependencies #}
class Ob p a
class (forall a. Ob (Dom f) a => Ob (Cod f) (f a)) => Functor f where
type Dom f
type Cod f
liftOb :: forall f a. (Functor f, Ob (Dom f) a) => Dict (Ob (Cod f) (f a))
liftOb = Dict
```
While a version which uses fundeps instead does compile:
```hs
class (forall a. Ob dom a => Ob cod (f a)) => Functor dom cod f  f > dom cod
liftOb :: forall f a dom cod. (Functor dom cod f, Ob dom a) => Dict (Ob cod (f a))
liftOb = Dict
```https://gitlab.haskell.org/ghc/ghc//issues/15043A more aggressive version of fprintexpandedsynonyms that prints all type s...20200123T19:20:59ZDomen KožarA more aggressive version of fprintexpandedsynonyms that prints all type synonymsUsing GHC 8.2.2 and `stack build ghcoptions=fprintexpandedsynonyms` I have the following type synonym for servant:
```hs
type Get302 (cts :: [*]) (hs :: [*]) = Verb 'GET 302 cts
(Headers (Header "Location" String ': hs) NoContent)
```
and get the following error message when `String` is mismatched for `Text`:
```
• Couldn't match type ‘Text’ with ‘[Char]’
Expected type: AsServerT App
: ("login"
:> ("callback"
:> (QueryParam "code" Text
:> (QueryParam "state" Text
:> MyApp.Types.Servant.Get302
'[PlainText]
'[Header "SetCookie" SetCookie,
Header "SetCookie" SetCookie]))))
Actual type: Maybe Code
> Maybe Text
> App
(Headers
'[Header "Location" Text, Header "SetCookie" SetCookie,
Header "SetCookie" SetCookie]
NoContent)
```
The error is confusing as type synonym is not expanded and offending `Header` is missing from the output in the expected type.Using GHC 8.2.2 and `stack build ghcoptions=fprintexpandedsynonyms` I have the following type synonym for servant:
```hs
type Get302 (cts :: [*]) (hs :: [*]) = Verb 'GET 302 cts
(Headers (Header "Location" String ': hs) NoContent)
```
and get the following error message when `String` is mismatched for `Text`:
```
• Couldn't match type ‘Text’ with ‘[Char]’
Expected type: AsServerT App
: ("login"
:> ("callback"
:> (QueryParam "code" Text
:> (QueryParam "state" Text
:> MyApp.Types.Servant.Get302
'[PlainText]
'[Header "SetCookie" SetCookie,
Header "SetCookie" SetCookie]))))
Actual type: Maybe Code
> Maybe Text
> App
(Headers
'[Header "Location" Text, Header "SetCookie" SetCookie,
Header "SetCookie" SetCookie]
NoContent)
```
The error is confusing as type synonym is not expanded and offending `Header` is missing from the output in the expected type.