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

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

26  (fromDynamic dyn :: Maybe (IOA (Live t)))
 ^^^^^^^^^^^^^^^
```
Potentially related to #16627https://gitlab.haskell.org/ghc/ghc//issues/17562`Any` appearing in a quantified constraint20210111T13:07:45ZRichard Eisenbergrae@richarde.dev`Any` appearing in a quantified constraintIf I say
```hs
{# LANGUAGE QuantifiedConstraints, MultiParamTypeClasses #}
module Bug where
class (forall a. a b ~ a c) => C b c
```
I get
```
Bug.hs:5:1: error:
• Illegal type synonym family application ‘GHC.Types.Any
@*’ in instance:
(a b :: GHC.Types.Any @*) ~ (a c :: GHC.Types.Any @*)
• In the quantified constraint ‘forall (a :: k > GHC.Types.Any).
a b ~ a c’
In the context: forall (a :: k > GHC.Types.Any). a b ~ a c
While checking the superclasses of class ‘C’
In the class declaration for ‘C’

5  class (forall a. a b ~ a c) => C b c
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
This is a specific case of #17567. Despite superficial similarity, this is unrelated to #16775.If I say
```hs
{# LANGUAGE QuantifiedConstraints, MultiParamTypeClasses #}
module Bug where
class (forall a. a b ~ a c) => C b c
```
I get
```
Bug.hs:5:1: error:
• Illegal type synonym family application ‘GHC.Types.Any
@*’ in instance:
(a b :: GHC.Types.Any @*) ~ (a c :: GHC.Types.Any @*)
• In the quantified constraint ‘forall (a :: k > GHC.Types.Any).
a b ~ a c’
In the context: forall (a :: k > GHC.Types.Any). a b ~ a c
While checking the superclasses of class ‘C’
In the class declaration for ‘C’

5  class (forall a. a b ~ a c) => C b c
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
This is a specific case of #17567. Despite superficial similarity, this is unrelated to #16775.9.0.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/17567Never `Any`ify during kind inference20210111T13:09:30ZRichard Eisenbergrae@richarde.devNever `Any`ify during kind inference#14198 concludes with a new plan: never `Any`ify during kind inference. This ticket tracks this particular problem, separate from #14198.
Here are some examples of `Any`ification during kind inference:
#17301:
```hs
data B a
data TySing ty where
SB :: TySing (B a)
data ATySing where
MkATySing :: TySing ty > ATySing
type family Forget ty :: ATySing where
Forget (B a) = MkATySing SB
```
The RHS of that type family equation is really `MkATySing @alpha (SB @alpha)`, and the `alpha` gets zonked to `Any`.
#14198:
```hs
type T = forall a. Proxy a
```
The RHS of the type synonym is really `forall (a :: kappa). Proxy @kappa a`, and the `kappa` gets zonked to `Any`.
#17562:
```hs
class (forall a. a b ~ a c) => C b c
```
The superclass constraint is really `forall (a :: Type > kappa). (~) @kappa (a b) (a c))`, and the `kappa` gets zonked to `Any`.
We want to stop zonking to `Any`, preferring to error instead. But how should we implement?
* Option A: Use a new variant of `ZonkFlexi`, a choice carried around in a `ZonkEnv` that says what to do with empty metavariables. The new choice would cause an error. This new form of `ZonkFlexi` would be used in the final zonks in e.g. TcTyClsDecls. Open question: how to get a decent error message? I think we'd have to pass around the original, toplevel type in order to report it. By the time we have just the unbound metavariable, we have no context to report.
* Option B: Similar to (A), but don't report an error in the zonker. Instead, the new variant of `ZonkFlexi` would insert some magical error type. Then, the validity checker could do an early pass, looking for the error type; it can then report a nice error message.
* Option C: Look for all cases where `Any`ification might happen, and detect each one separately. This can produce lovely error messages. The solution for #17562 in !2313 does this. Perhaps we can pair this choice with a new `ZonkFlexi` that panics. That way, we'll know if we've missed a case.
* Simon below proposes Option D: Zap to `Type` instead of `Any`. I (Richard) view D as an addon to any of the above plans. Because `Type` is not always wellkinded, we can only zap to `Type` sometimes, and we still need to decide what we do at other times. Personally, I prefer not to treat `Type` specially with XPolyKinds` enabled, and so I'd prefer that we don't do this.
* EDIT: Also, we can consider Option E: Report poor error messages, saying something about an unconstrained kind variable. Users would be helped only via the context (the "In the data declaration for `Wurble`" bits). This would mean building up useful contexts in the zonker.
* Option F: The new constructor for `ZonkFlexi` could carry the toplevel type we are trying to zonk. If we encounter an unconstrained metavariable, we just look at this bit of context to produce the error message. Perhaps this could be combined with the contextbuilding in Option E for good effect. This is the first solution I'm actually happy with.
Thoughts?#14198 concludes with a new plan: never `Any`ify during kind inference. This ticket tracks this particular problem, separate from #14198.
Here are some examples of `Any`ification during kind inference:
#17301:
```hs
data B a
data TySing ty where
SB :: TySing (B a)
data ATySing where
MkATySing :: TySing ty > ATySing
type family Forget ty :: ATySing where
Forget (B a) = MkATySing SB
```
The RHS of that type family equation is really `MkATySing @alpha (SB @alpha)`, and the `alpha` gets zonked to `Any`.
#14198:
```hs
type T = forall a. Proxy a
```
The RHS of the type synonym is really `forall (a :: kappa). Proxy @kappa a`, and the `kappa` gets zonked to `Any`.
#17562:
```hs
class (forall a. a b ~ a c) => C b c
```
The superclass constraint is really `forall (a :: Type > kappa). (~) @kappa (a b) (a c))`, and the `kappa` gets zonked to `Any`.
We want to stop zonking to `Any`, preferring to error instead. But how should we implement?
* Option A: Use a new variant of `ZonkFlexi`, a choice carried around in a `ZonkEnv` that says what to do with empty metavariables. The new choice would cause an error. This new form of `ZonkFlexi` would be used in the final zonks in e.g. TcTyClsDecls. Open question: how to get a decent error message? I think we'd have to pass around the original, toplevel type in order to report it. By the time we have just the unbound metavariable, we have no context to report.
* Option B: Similar to (A), but don't report an error in the zonker. Instead, the new variant of `ZonkFlexi` would insert some magical error type. Then, the validity checker could do an early pass, looking for the error type; it can then report a nice error message.
* Option C: Look for all cases where `Any`ification might happen, and detect each one separately. This can produce lovely error messages. The solution for #17562 in !2313 does this. Perhaps we can pair this choice with a new `ZonkFlexi` that panics. That way, we'll know if we've missed a case.
* Simon below proposes Option D: Zap to `Type` instead of `Any`. I (Richard) view D as an addon to any of the above plans. Because `Type` is not always wellkinded, we can only zap to `Type` sometimes, and we still need to decide what we do at other times. Personally, I prefer not to treat `Type` specially with XPolyKinds` enabled, and so I'd prefer that we don't do this.
* EDIT: Also, we can consider Option E: Report poor error messages, saying something about an unconstrained kind variable. Users would be helped only via the context (the "In the data declaration for `Wurble`" bits). This would mean building up useful contexts in the zonker.
* Option F: The new constructor for `ZonkFlexi` could carry the toplevel type we are trying to zonk. If we encounter an unconstrained metavariable, we just look at this bit of context to produce the error message. Perhaps this could be combined with the contextbuilding in Option E for good effect. This is the first solution I'm actually happy with.
Thoughts?https://gitlab.haskell.org/ghc/ghc//issues/17301GHC.TypeLits.TypeError can print 'GHC.Types.Any' when existentials are involved20210111T13:10:21ZsheafGHC.TypeLits.TypeError can print 'GHC.Types.Any' when existentials are involvedI've run into a situation where GHC seems to forget some information.
Specifically: when wrapping typelevel information into a promoted existential datatype, and then unwrapping it, `Any` can appear.
I've boiled it down to the following simple example:
```haskell
{# LANGUAGE DataKinds #}
{# LANGUAGE GADTs #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE UndecidableInstances #}
module AnyTypeError where
import GHC.TypeLits
( TypeError, ErrorMessage(..) )
data A = MkA
data B (a :: A)
data TySing ty where
SB :: TySing (B a)
data ATySing where
MkATySing :: TySing ty > ATySing
type family Forget ty :: ATySing where
Forget (B a) = MkATySing SB
type family Message ty where
Message (MkATySing (_ :: TySing ty)) =
TypeError ( ShowType ty )
type KnownType = B MkA
foo :: Message (Forget KnownType) => ()
foo = ()
bar :: ()
bar = foo
```
```
AnyTypeError.hs:36:7: error:
* B GHC.Types.Any
* In the expression: foo
In an equation for `bar': bar = foo

36  bar = foo
 ^^^
Failed, no modules loaded.
```
I think the error message should instead be:
```
AnyTypeError.hs:36:7: error:
* B 'MkA
...
```
<p>
<details>
<summary> Show/hide background information (i.e. why this matters to me).</summary>
I ran into this code when working on giving helpful custom type errors. In a library I'm working on, the user can layout vertex data passed to the GPU by specifing interface slots (see e.g. [the OpenGL wiki](https://www.khronos.org/opengl/wiki/Layout_Qualifier_(GLSL)#Interface_components) for reference). For instance the following would be an invalid layout:
```haskell
type InvalidLayout = '[ Slot 0 0 ':> V 3 Double, Slot 1 0 ':> V 4 Float ]
```
After some lengthy typelevel computations with type families (involving existential types similar to those described above), I need to throw an error: the `V 4 Double` spills into the second slot (`Slot 1`) so overlaps with the `V 4 Float`. However the error message I end up throwing, because of the bug described here, comes out looking like this:
```
* Overlap at location 1, component 0:
 V GHC.Types.Any Double based at location 0, component 0,
 V GHC.Types.Any Float based at location 1, component 0.
```
The size of the vectors are lost, so the error message becomes confusingly vague.
</details>
</p>
I've tested this on GHC 8.6.5, 8.8.1 and HEAD (8.9.0.20190930), all giving identical results.I've run into a situation where GHC seems to forget some information.
Specifically: when wrapping typelevel information into a promoted existential datatype, and then unwrapping it, `Any` can appear.
I've boiled it down to the following simple example:
```haskell
{# LANGUAGE DataKinds #}
{# LANGUAGE GADTs #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE UndecidableInstances #}
module AnyTypeError where
import GHC.TypeLits
( TypeError, ErrorMessage(..) )
data A = MkA
data B (a :: A)
data TySing ty where
SB :: TySing (B a)
data ATySing where
MkATySing :: TySing ty > ATySing
type family Forget ty :: ATySing where
Forget (B a) = MkATySing SB
type family Message ty where
Message (MkATySing (_ :: TySing ty)) =
TypeError ( ShowType ty )
type KnownType = B MkA
foo :: Message (Forget KnownType) => ()
foo = ()
bar :: ()
bar = foo
```
```
AnyTypeError.hs:36:7: error:
* B GHC.Types.Any
* In the expression: foo
In an equation for `bar': bar = foo

36  bar = foo
 ^^^
Failed, no modules loaded.
```
I think the error message should instead be:
```
AnyTypeError.hs:36:7: error:
* B 'MkA
...
```
<p>
<details>
<summary> Show/hide background information (i.e. why this matters to me).</summary>
I ran into this code when working on giving helpful custom type errors. In a library I'm working on, the user can layout vertex data passed to the GPU by specifing interface slots (see e.g. [the OpenGL wiki](https://www.khronos.org/opengl/wiki/Layout_Qualifier_(GLSL)#Interface_components) for reference). For instance the following would be an invalid layout:
```haskell
type InvalidLayout = '[ Slot 0 0 ':> V 3 Double, Slot 1 0 ':> V 4 Float ]
```
After some lengthy typelevel computations with type families (involving existential types similar to those described above), I need to throw an error: the `V 4 Double` spills into the second slot (`Slot 1`) so overlaps with the `V 4 Float`. However the error message I end up throwing, because of the bug described here, comes out looking like this:
```
* Overlap at location 1, component 0:
 V GHC.Types.Any Double based at location 0, component 0,
 V GHC.Types.Any Float based at location 1, component 0.
```
The size of the vectors are lost, so the error message becomes confusingly vague.
</details>
</p>
I've tested this on GHC 8.6.5, 8.8.1 and HEAD (8.9.0.20190930), all giving identical results.https://gitlab.haskell.org/ghc/ghc//issues/18151Etaexpansion of a leftsection20210112T23:04:49ZRichard Eisenbergrae@richarde.devEtaexpansion of a leftsectionIf I say
```hs
x = seq (True `undefined`) ()
```
what should I get when evaluating `x`?
According to my understanding of the Haskell Report, I should get `()`. And according to my understanding of GHC's source code (in `GHC.Tc.Gen.Expr`), I should get `()`. But I get an exception.
Why?
NB: `XPostfixOperators` is off. If it were on, the exception would be expected.
Spun off from https://github.com/ghcproposals/ghcproposals/pull/275#issuecomment624282022If I say
```hs
x = seq (True `undefined`) ()
```
what should I get when evaluating `x`?
According to my understanding of the Haskell Report, I should get `()`. And according to my understanding of GHC's source code (in `GHC.Tc.Gen.Expr`), I should get `()`. But I get an exception.
Why?
NB: `XPostfixOperators` is off. If it were on, the exception would be expected.
Spun off from https://github.com/ghcproposals/ghcproposals/pull/275#issuecomment6242820229.0.1Vladislav ZavialovVladislav Zavialovhttps://gitlab.haskell.org/ghc/ghc//issues/19197‘:kind () :: '()’ doesn't give any output20210118T17:11:59ZIcelandjack‘:kind () :: '()’ doesn't give any output```
$ ./ghc/_build/stage1/bin/ghc ignoredotghci interactive
GHCi, version 9.1.0.20201202: https://www.haskell.org/ghc/ :? for help
ghci> :set XKindSignatures XDataKinds
ghci> :k () :: '()
ghci>
ghci> :set XPartialTypeSignatures Wnopartialtypesignatures
ghci> :k (_, _) :: '(_, _)
ghci>
ghci> import Data.Functor.Identity
ghci> :k Identity _ :: 'Identity _
ghci>
```
It should give an error```
$ ./ghc/_build/stage1/bin/ghc ignoredotghci interactive
GHCi, version 9.1.0.20201202: https://www.haskell.org/ghc/ :? for help
ghci> :set XKindSignatures XDataKinds
ghci> :k () :: '()
ghci>
ghci> :set XPartialTypeSignatures Wnopartialtypesignatures
ghci> :k (_, _) :: '(_, _)
ghci>
ghci> import Data.Functor.Identity
ghci> :k Identity _ :: 'Identity _
ghci>
```
It should give an errorhttps://gitlab.haskell.org/ghc/ghc//issues/19142panic lookup_final_id with fdefertypeerrors and kind error in instance def...20210122T21:09:33ZJakob Brünkerpanic lookup_final_id with fdefertypeerrors and kind error in instance definition## Summary
This file
```haskell
{# OPTIONS_GHC fdefertypeerrors #}
{# LANGUAGE ExplicitForAll
, TypeApplications
, KindSignatures
, FlexibleInstances
#}
foo :: forall (f :: * > *) . String
foo = ""
instance Show a where
show _ = foo @Int
```
produces the following error:
```
Bug.hs:12:17: warning: [Wdeferredtypeerrors]
• Expected kind ‘* > *’, but ‘Int’ has kind ‘*’
• In the type ‘Int’
In the expression: foo @Int
In an equation for ‘show’: show _ = foo @Int

12  show _ = foo @Int
 ^^^
ghc: panic! (the 'impossible' happened)
(GHC version 9.0.0.20201227:
lookup_final_id
$fShowa
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/GHC/Utils/Outputable.hs:1230:37 in ghc:GHC.Utils.Outputable
pprPanic, called at compiler/GHC/Iface/Tidy.hs:200:12 in ghc:GHC.Iface.Tidy
```
Without `fdefertypeerrors`, only the kind error would be shown, not the panic.
## Expected behavior
GHC shouldn't panic
## Environment
* GHC version used: 9.0.0.20201227 as well as 8.10.2
Optional:
* Operating System: Ubuntu inside WSL2 inside Windows 10
* System Architecture: x86_64## Summary
This file
```haskell
{# OPTIONS_GHC fdefertypeerrors #}
{# LANGUAGE ExplicitForAll
, TypeApplications
, KindSignatures
, FlexibleInstances
#}
foo :: forall (f :: * > *) . String
foo = ""
instance Show a where
show _ = foo @Int
```
produces the following error:
```
Bug.hs:12:17: warning: [Wdeferredtypeerrors]
• Expected kind ‘* > *’, but ‘Int’ has kind ‘*’
• In the type ‘Int’
In the expression: foo @Int
In an equation for ‘show’: show _ = foo @Int

12  show _ = foo @Int
 ^^^
ghc: panic! (the 'impossible' happened)
(GHC version 9.0.0.20201227:
lookup_final_id
$fShowa
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/GHC/Utils/Outputable.hs:1230:37 in ghc:GHC.Utils.Outputable
pprPanic, called at compiler/GHC/Iface/Tidy.hs:200:12 in ghc:GHC.Iface.Tidy
```
Without `fdefertypeerrors`, only the kind error would be shown, not the panic.
## Expected behavior
GHC shouldn't panic
## Environment
* GHC version used: 9.0.0.20201227 as well as 8.10.2
Optional:
* Operating System: Ubuntu inside WSL2 inside Windows 10
* System Architecture: x86_64https://gitlab.haskell.org/ghc/ghc//issues/16947Refactor Ct and friends20210122T23:50:33ZRichard Eisenbergrae@richarde.devRefactor Ct and friendsRight now, the `Ct` type contains many constructors. This ticket tracks breaking up this type into smaller ones. Candidates:
* All constraints are born as noncanonical. So the bag of constraints in the `TcM` monad are all noncanonical. This should be its own type.
* Equality constraints are dealt with separately from others. (See details on the description of the inert set.) These should be their own types, too.
* A work list has both canonical and noncanonical constraints. But this might be the only place we need the full sum.Right now, the `Ct` type contains many constructors. This ticket tracks breaking up this type into smaller ones. Candidates:
* All constraints are born as noncanonical. So the bag of constraints in the `TcM` monad are all noncanonical. This should be its own type.
* Equality constraints are dealt with separately from others. (See details on the description of the inert set.) These should be their own types, too.
* A work list has both canonical and noncanonical constraints. But this might be the only place we need the full sum.9.2.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://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/17955mkNewTyConRhs panic when trying to constrain newtype with Coercible20210123T06:44:33ZmatzemathicsmkNewTyConRhs panic when trying to constrain newtype with Coercible## Summary
The following code panics in ghc 8.8.3:
```haskell
{# LANGUAGE FlexibleContexts #}
import Data.Coerce
newtype T = Coercible () T => T ()
```
Error message:
```
[1 of 1] Compiling Main ( abug.hs, abug.o )
ghc: panic! (the 'impossible' happened)
(GHC version 8.8.3 for x86_64unknownlinux):
mkNewTyConRhs
T [Coercible () T, ()]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1159:37 in ghc:Outputable
pprPanic, called at compiler/iface/BuildTyCl.hs:65:27 in ghc:BuildTyCl
```
This seems to come from whatever is done to infer Coercible's instances.
Any other Constraint (weather or not using a multi parameter class) gives an error message:
```haskell
{# LANGUAGE FlexibleContexts #}
newtype T = Show T => T ()
```
results in:
```
[1 of 1] Compiling Main ( abug.hs, abug.o )
abug.hs:3:13: error:
* A newtype constructor cannot have a context in its type
T :: Show T => () > T
* In the definition of data constructor `T'
In the newtype declaration for `T'

3  newtype T = Show T => T ()
 ^^^^^^^^^^^^^^
```
## Expected behavior
Should most likely print an error message as in the second example.
## Environment
* GHC version used: 8.8.3## Summary
The following code panics in ghc 8.8.3:
```haskell
{# LANGUAGE FlexibleContexts #}
import Data.Coerce
newtype T = Coercible () T => T ()
```
Error message:
```
[1 of 1] Compiling Main ( abug.hs, abug.o )
ghc: panic! (the 'impossible' happened)
(GHC version 8.8.3 for x86_64unknownlinux):
mkNewTyConRhs
T [Coercible () T, ()]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1159:37 in ghc:Outputable
pprPanic, called at compiler/iface/BuildTyCl.hs:65:27 in ghc:BuildTyCl
```
This seems to come from whatever is done to infer Coercible's instances.
Any other Constraint (weather or not using a multi parameter class) gives an error message:
```haskell
{# LANGUAGE FlexibleContexts #}
newtype T = Show T => T ()
```
results in:
```
[1 of 1] Compiling Main ( abug.hs, abug.o )
abug.hs:3:13: error:
* A newtype constructor cannot have a context in its type
T :: Show T => () > T
* In the definition of data constructor `T'
In the newtype declaration for `T'

3  newtype T = Show T => T ()
 ^^^^^^^^^^^^^^
```
## Expected behavior
Should most likely print an error message as in the second example.
## Environment
* GHC version used: 8.8.39.0.1https://gitlab.haskell.org/ghc/ghc//issues/14873The wellkinded type invariant (in TcType)20210123T17:55:45ZRyan ScottThe wellkinded type invariant (in TcType)(Originally noticed [here](https://travisci.org/goldfirere/singletons/jobs/347945148#L1179).)
The following program typechecks on GHC 8.2.2 on GHC 8.4.1, but panics on GHC HEAD:
```hs
{# LANGUAGE RankNTypes #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeApplications #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
module Bug where
import Data.Kind (Type)
data family Sing (a :: k)
newtype instance Sing (f :: k1 ~> k2) =
SLambda { applySing :: forall t. Sing t > Sing (Apply f t) }
data TyFun :: Type > Type > Type
type a ~> b = TyFun a b > Type
infixr 0 ~>
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
class SingI (a :: k) where
sing :: Sing a
data ColSym1 :: f a > a ~> Bool
type instance Apply (ColSym1 x) y = Col x y
class PColumn (f :: Type > Type) where
type Col (x :: f a) (y :: a) :: Bool
class SColumn (f :: Type > Type) where
sCol :: forall (x :: f a) (y :: a).
Sing x > Sing y > Sing (Col x y :: Bool)
instance (SColumn f, SingI x) => SingI (ColSym1 (x :: f a) :: a ~> Bool) where
sing = SLambda (sCol (sing @_ @x))
```
```
$ /opt/ghc/head/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
ghc: panic! (the 'impossible' happened)
(GHC version 8.5.20180201 for x86_64unknownlinux):
piResultTy
k_aZU[tau:1]
(a_aW8[sk:1] > <*>_N)
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1150:37 in ghc:Outputable
pprPanic, called at compiler/types/Type.hs:947:35 in ghc:Type
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  highest 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"GHC HEAD regression (piResultTy)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"(Originally noticed [https://travisci.org/goldfirere/singletons/jobs/347945148#L1179 here].)\r\n\r\nThe following program typechecks on GHC 8.2.2 on GHC 8.4.1, but panics on GHC HEAD:\r\n\r\n{{{#!hs\r\n{# LANGUAGE RankNTypes #}\r\n{# LANGUAGE ScopedTypeVariables #}\r\n{# LANGUAGE TypeApplications #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeInType #}\r\n{# LANGUAGE TypeOperators #}\r\nmodule Bug where\r\n\r\nimport Data.Kind (Type)\r\n\r\ndata family Sing (a :: k)\r\n\r\nnewtype instance Sing (f :: k1 ~> k2) =\r\n SLambda { applySing :: forall t. Sing t > Sing (Apply f t) }\r\n\r\ndata TyFun :: Type > Type > Type\r\ntype a ~> b = TyFun a b > Type\r\ninfixr 0 ~>\r\ntype family Apply (f :: k1 ~> k2) (x :: k1) :: k2\r\n\r\nclass SingI (a :: k) where\r\n sing :: Sing a\r\n\r\ndata ColSym1 :: f a > a ~> Bool\r\ntype instance Apply (ColSym1 x) y = Col x y\r\n\r\nclass PColumn (f :: Type > Type) where\r\n type Col (x :: f a) (y :: a) :: Bool\r\n\r\nclass SColumn (f :: Type > Type) where\r\n sCol :: forall (x :: f a) (y :: a).\r\n Sing x > Sing y > Sing (Col x y :: Bool)\r\n\r\ninstance (SColumn f, SingI x) => SingI (ColSym1 (x :: f a) :: a ~> Bool) where\r\n sing = SLambda (sCol (sing @_ @x))\r\n}}}\r\n\r\n{{{\r\n$ /opt/ghc/head/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\nghc: panic! (the 'impossible' happened)\r\n (GHC version 8.5.20180201 for x86_64unknownlinux):\r\n piResultTy\r\n k_aZU[tau:1]\r\n (a_aW8[sk:1] > <*>_N)\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1150:37 in ghc:Outputable\r\n pprPanic, called at compiler/types/Type.hs:947:35 in ghc:Type\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >(Originally noticed [here](https://travisci.org/goldfirere/singletons/jobs/347945148#L1179).)
The following program typechecks on GHC 8.2.2 on GHC 8.4.1, but panics on GHC HEAD:
```hs
{# LANGUAGE RankNTypes #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeApplications #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
module Bug where
import Data.Kind (Type)
data family Sing (a :: k)
newtype instance Sing (f :: k1 ~> k2) =
SLambda { applySing :: forall t. Sing t > Sing (Apply f t) }
data TyFun :: Type > Type > Type
type a ~> b = TyFun a b > Type
infixr 0 ~>
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
class SingI (a :: k) where
sing :: Sing a
data ColSym1 :: f a > a ~> Bool
type instance Apply (ColSym1 x) y = Col x y
class PColumn (f :: Type > Type) where
type Col (x :: f a) (y :: a) :: Bool
class SColumn (f :: Type > Type) where
sCol :: forall (x :: f a) (y :: a).
Sing x > Sing y > Sing (Col x y :: Bool)
instance (SColumn f, SingI x) => SingI (ColSym1 (x :: f a) :: a ~> Bool) where
sing = SLambda (sCol (sing @_ @x))
```
```
$ /opt/ghc/head/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
ghc: panic! (the 'impossible' happened)
(GHC version 8.5.20180201 for x86_64unknownlinux):
piResultTy
k_aZU[tau:1]
(a_aW8[sk:1] > <*>_N)
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1150:37 in ghc:Outputable
pprPanic, called at compiler/types/Type.hs:947:35 in ghc:Type
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  highest 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"GHC HEAD regression (piResultTy)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"(Originally noticed [https://travisci.org/goldfirere/singletons/jobs/347945148#L1179 here].)\r\n\r\nThe following program typechecks on GHC 8.2.2 on GHC 8.4.1, but panics on GHC HEAD:\r\n\r\n{{{#!hs\r\n{# LANGUAGE RankNTypes #}\r\n{# LANGUAGE ScopedTypeVariables #}\r\n{# LANGUAGE TypeApplications #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeInType #}\r\n{# LANGUAGE TypeOperators #}\r\nmodule Bug where\r\n\r\nimport Data.Kind (Type)\r\n\r\ndata family Sing (a :: k)\r\n\r\nnewtype instance Sing (f :: k1 ~> k2) =\r\n SLambda { applySing :: forall t. Sing t > Sing (Apply f t) }\r\n\r\ndata TyFun :: Type > Type > Type\r\ntype a ~> b = TyFun a b > Type\r\ninfixr 0 ~>\r\ntype family Apply (f :: k1 ~> k2) (x :: k1) :: k2\r\n\r\nclass SingI (a :: k) where\r\n sing :: Sing a\r\n\r\ndata ColSym1 :: f a > a ~> Bool\r\ntype instance Apply (ColSym1 x) y = Col x y\r\n\r\nclass PColumn (f :: Type > Type) where\r\n type Col (x :: f a) (y :: a) :: Bool\r\n\r\nclass SColumn (f :: Type > Type) where\r\n sCol :: forall (x :: f a) (y :: a).\r\n Sing x > Sing y > Sing (Col x y :: Bool)\r\n\r\ninstance (SColumn f, SingI x) => SingI (ColSym1 (x :: f a) :: a ~> Bool) where\r\n sing = SLambda (sCol (sing @_ @x))\r\n}}}\r\n\r\n{{{\r\n$ /opt/ghc/head/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\nghc: panic! (the 'impossible' happened)\r\n (GHC version 8.5.20180201 for x86_64unknownlinux):\r\n piResultTy\r\n k_aZU[tau:1]\r\n (a_aW8[sk:1] > <*>_N)\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1150:37 in ghc:Outputable\r\n pprPanic, called at compiler/types/Type.hs:947:35 in ghc:Type\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >9.2.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://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/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/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/19106Partial type signature variable confuses instance solving20210125T22:40:41ZRichard Eisenbergrae@richarde.devPartial type signature variable confuses instance solvingWhen I say
```hs
{# LANGUAGE TypeFamilies, GADTs #}
module Bug where
f :: (a ~ [b]) => T a > _ > String
f (MkT x) _ = show x
data T a where
MkT :: G a => a > T a
type family G a where
G [b] = Show b
```
I get
```
Bug.hs:6:1: error:
• Could not deduce (Show b)
from the context: a ~ [b]
bound by the inferred type for ‘f’:
forall a b {w}. (a ~ [b]) => T a > w > String
at Bug.hs:6:120
• When checking that the inferred type
f :: forall {a} {b} {w}. (a ~ [b], Show [b]) => T a > w > String
is as general as its (partial) signature
f :: forall a b {w}. (a ~ [b]) => T a > w > String
```
We end up with
```
[G] Show b[tyv:1]
[W] Show [b[tyv:1]]
```
The check in `matchableGivens` considers `b` a metavariable. This isn't entirely wrong, but `b` is a `TyVarTv`, and should not be considered unifiable in `matchableGivens`. The solution is very easy: just change `matchableGivens` to treat `TyVarTv`s like skolems.When I say
```hs
{# LANGUAGE TypeFamilies, GADTs #}
module Bug where
f :: (a ~ [b]) => T a > _ > String
f (MkT x) _ = show x
data T a where
MkT :: G a => a > T a
type family G a where
G [b] = Show b
```
I get
```
Bug.hs:6:1: error:
• Could not deduce (Show b)
from the context: a ~ [b]
bound by the inferred type for ‘f’:
forall a b {w}. (a ~ [b]) => T a > w > String
at Bug.hs:6:120
• When checking that the inferred type
f :: forall {a} {b} {w}. (a ~ [b], Show [b]) => T a > w > String
is as general as its (partial) signature
f :: forall a b {w}. (a ~ [b]) => T a > w > String
```
We end up with
```
[G] Show b[tyv:1]
[W] Show [b[tyv:1]]
```
The check in `matchableGivens` considers `b` a metavariable. This isn't entirely wrong, but `b` is a `TyVarTv`, and should not be considered unifiable in `matchableGivens`. The solution is very easy: just change `matchableGivens` to treat `TyVarTv`s like skolems.Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/19107GADT pattern match defeats instance solving20210125T22:41:18ZRichard Eisenbergrae@richarde.devGADT pattern match defeats instance solvingWhen I say
```hs
{# LANGUAGE GADTs #}
 NB: NO FlexibleContexts
module Bug where
data T a where
MkT :: Show a => [a] > T a
f (MkT x) = show x
```
GHC says
```
Bug.hs:8:1: error:
• Non typevariable argument in the constraint: Show [a]
(Use FlexibleContexts to permit this)
• When checking the inferred type
f :: forall {a}. Show [a] => T a > String
```
The problem is that GHC wants to infer `f :: Show [a] => T a > String`. Yet the correct type is `f :: Show a => T a > String`, with the simplified `Show a` constraint.
The reason this happens is that the solver ends up in this scenario:
```
at level 2
[G] Show alpha[tau:1]
[W] Show [alpha[tau:1]]
```
Before committing to the toplevel `Show a => Show [a]` instance, GHC checks whether any Givens might fire later. It worries `Show alpha` might apply later. But this would be impossible unless `alpha` becomes an infinitely nested list. There is already logic in `lookupInstEnv'` to usefully ignore such absurdities in instance lookup (see `Note [Infinitary substitution in lookup]` in GHC.Core.InstEnv), and we should extend this logic to `matchableGivens`.When I say
```hs
{# LANGUAGE GADTs #}
 NB: NO FlexibleContexts
module Bug where
data T a where
MkT :: Show a => [a] > T a
f (MkT x) = show x
```
GHC says
```
Bug.hs:8:1: error:
• Non typevariable argument in the constraint: Show [a]
(Use FlexibleContexts to permit this)
• When checking the inferred type
f :: forall {a}. Show [a] => T a > String
```
The problem is that GHC wants to infer `f :: Show [a] => T a > String`. Yet the correct type is `f :: Show a => T a > String`, with the simplified `Show a` constraint.
The reason this happens is that the solver ends up in this scenario:
```
at level 2
[G] Show alpha[tau:1]
[W] Show [alpha[tau:1]]
```
Before committing to the toplevel `Show a => Show [a]` instance, GHC checks whether any Givens might fire later. It worries `Show alpha` might apply later. But this would be impossible unless `alpha` becomes an infinitely nested list. There is already logic in `lookupInstEnv'` to usefully ignore such absurdities in instance lookup (see `Note [Infinitary substitution in lookup]` in GHC.Core.InstEnv), and we should extend this logic to `matchableGivens`.Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/19315GHC 9.0 regression: plots0.1.1.2 fails to build due to ambiguous type variable20210210T21:11:55ZRyan ScottGHC 9.0 regression: plots0.1.1.2 fails to build due to ambiguous type variable_Originally observed in a `head.hackage` CI build [here](https://gitlab.haskell.org/ghc/head.hackage//jobs/568397#L5617)_.
The `plots0.1.1.2` library fails to compile using commit 0789f7a18a78920f50647e2b4aa8082a14ca9e90 of the `ghc9.0` branch. Here is a selfcontained example with no external dependencies:
```hs
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE FunctionalDependencies #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE RecordWildCards #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeOperators #}
module Bug where
import Control.Monad.Reader
import Data.Functor.Const
import Data.Functor.Identity
import Data.Monoid (Any(..))
import Data.Typeable
type TypeableFloat n = (Typeable n, RealFloat n)
type Lens' s a = Lens s s a a
type Lens s t a b = forall f. Functor f => (a > f b) > s > f t
type LensLike' f s a = LensLike f s s a a
type LensLike f s t a b = (a > f b) > s > f t
type Getting r s a = (a > Const r a) > s > Const r s
type ASetter s t a b = (a > Identity b) > s > Identity t
data V2 a = V2 !a !a
flipX_Y :: Num n => V2 n > V2 n
flipX_Y (V2 x y) = V2 (y) (x)
class R1 t where
_x :: Lens' (t a) a
class R1 t => R2 t where
_y :: Lens' (t a) a
instance R1 V2 where
_x f (V2 a b) = (`V2` b) <$> f a
instance R2 V2 where
_y f (V2 a b) = V2 a <$> f b
infixl 8 #
(#) :: a > (a > b) > b
(#) = flip ($)
infixr 4 %~
(%~) :: ASetter s t a b > (a > b) > s > t
(%~) = over
(^.) :: s > Getting a s a > a
s ^. l = getConst (l Const s)
over :: ASetter s t a b > (a > b) > s > t
over l f = runIdentity . l (Identity . f)
view :: MonadReader s m => Getting a s a > m a
view l = asks (getConst . l Const)
lens :: (s > a) > (s > b > t) > Lens s t a b
lens sa sbt afb s = sbt s <$> afb (sa s)
type family V a :: * > *
type family N a :: *
type Vn a = V a (N a)
data Style (v :: * > *) n = Style
class HasStyle a where
applyStyle :: Style (V a) (N a) > a > a
type TextFunction b v n = TextAlignment n > String > QDiagram b v n Any
data TickLabels b (v :: * > *) n = TickLabels
{ tlFun :: [n] > (n,n) > [(n, String)]
, tlTextFun :: TextFunction b v n
, tlStyle :: Style v n
, tlGap :: n
}
type instance V (TickLabels b v n) = v
type instance N (TickLabels b v n) = n
class HasTickLabels f a b  a > b where
tickLabel :: LensLike' f a (TickLabels b (V a) (N a))
tickLabelTextFunction :: Functor f => LensLike' f a (TextFunction b (V a) (N a))
tickLabelTextFunction = tickLabel . lens tlTextFun (\tl f > tl {tlTextFun = f})
tickLabelFunction :: Functor f => LensLike' f a ([N a] > (N a, N a) > [(N a, String)])
tickLabelFunction = tickLabel . lens tlFun (\tl f > tl {tlFun = f})
tickLabelStyle :: Functor f => LensLike' f a (Style (V a) (N a))
tickLabelStyle = tickLabel . lens tlStyle (\tl sty > tl {tlStyle = sty})
tickLabelGap :: Functor f => LensLike' f a (N a)
tickLabelGap = tickLabel . lens tlGap (\tl n > tl {tlGap = n})
instance HasTickLabels f (TickLabels b v n) b where
tickLabel = id
data ColourBar b n = ColourBar
{ cbTickLabels :: TickLabels b V2 n
, cbTicks :: MajorTicks V2 n
, cbWidth :: n
}
type instance V (ColourBar b n) = V2
type instance N (ColourBar b n) = n
data MajorTicks (v :: * > *) n = MajorTicks
{ matFunction :: (n,n) > [n]
}
type instance V (MajorTicks v n) = v
type instance N (MajorTicks v n) = n
class HasMajorTicks f a where
majorTicks :: LensLike' f a (MajorTicks (V a) (N a))
majorTicksFunction :: Functor f => LensLike' f a ((N a, N a) > [N a])
majorTicksFunction = majorTicks . lens matFunction (\mat a > mat {matFunction = a})
instance HasMajorTicks f (MajorTicks v n) where
majorTicks = id
data Path (v :: * > *) n = Path
data (::) u v = (u > v) :: (v > u)
infixr 7 ::
instance Semigroup (a :: a) where
(f :: f') <> (g :: g') = f . g :: g' . f'
instance Monoid (v :: v) where
mempty = id :: id
data Transformation v n = Transformation (v n :: v n) (v n :: v n) (v n)
class Transformable t where
transform :: Transformation (V t) (N t) > t > t
translation :: v n > Transformation v n
translation = Transformation mempty mempty
translate :: (Transformable t) => Vn t > t > t
translate = transform . translation
class Transformable t => Renderable t b where
orient :: HasOrientation o => o > a > a > a
orient o h v =
case view orientation o of
Horizontal > h
Vertical > v
data Orientation = Horizontal  Vertical
class HasOrientation a where
orientation :: Lens' a Orientation
instance HasPlacement (ColourBar b n) where
placement = undefined
instance HasOrientation (ColourBar b n) where
orientation = undefined
instance Functor f => HasMajorTicks f (ColourBar b n) where
majorTicks = lens cbTicks (\c a > c {cbTicks = a})
data ColourMap = ColourMap
data QDiagram b (v :: * > *) n m = QD
instance Semigroup m  (Metric v, OrderedField n, Semigroup m)
=> HasStyle (QDiagram b v n m) where
applyStyle = undefined
instance Semigroup m  (Metric v, OrderedField n, Semigroup m)
=> Monoid (QDiagram b v n m) where
mempty = undefined
instance Semigroup m  (Metric v, OrderedField n, Semigroup m)
=> Semigroup (QDiagram b v n m) where
(<>) = undefined
instance Semigroup m  (OrderedField n, Metric v, Semigroup m)
=> Transformable (QDiagram b v n m) where
transform = undefined
type instance V (QDiagram b v n m) = v
type instance N (QDiagram b v n m) = n
data TextAlignment n = BaselineText  BoxAlignedText n n
data Placement = Placement
{ pAt :: V2 Rational
}
class HasPlacement a where
placement :: Lens' a Placement
placementAt :: Lens' a (V2 Rational)
placementAt = placement . lens pAt (\p a > p {pAt = a})
renderColourBar
:: forall n b. (TypeableFloat n, Renderable (Path V2 n) b)
=> ColourBar b n
> ColourMap
> (n,n)
> n
> QDiagram b V2 n Any
renderColourBar cb@ColourBar {..} _cm bnds@(lb,ub) l
= tLbs
where
o, xy :: a > a > a
o = orient cb
xy a b = if let V2 x y = cb^.placementAt in x > y
then a else b
w = cbWidth
f x = (x  (ub + lb)/2) / (ub  lb) * l
inRange x = x >= lb && x <= ub
tickXs = view majorTicksFunction cbTicks bnds
tickXs' :: [n]
tickXs' = filter inRange tickXs
tickLabelXs :: [(n, String)]
tickLabelXs = view tickLabelFunction cbTickLabels tickXs' bnds
tLbs :: QDiagram b V2 n Any
tLbs = foldMap drawTickLabel tickLabelXs
drawTickLabel :: (n, String) > QDiagram b (V (TickLabels b V2 n)) (N (TickLabels b V2 n)) Any
drawTickLabel (x,label) =
view tickLabelTextFunction cbTickLabels tAlign label
# translate v
# applyStyle (cbTickLabels ^. tickLabelStyle)
where v = V2 (f x) ( w/2  view tickLabelGap cbTickLabels)
# xy id (_y %~ negate)
# o id ((_y %~ negate) . flipX_Y)
tAlign = o (xy (BoxAlignedText 0.5 1) (BoxAlignedText 0.5 0))
(xy (BoxAlignedText 0 0.5) (BoxAlignedText 1 0.5))
```
This compiles with GHC 8.10.3 and earlier, but fails to compile with `ghc9.0`:
```
$ ~/Software/ghc9.0.0.20210130/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:229:22: error:
• Could not deduce (HasTickLabels
(Const ([n] > (n, n) > [(n, String)])) (TickLabels b V2 n) b0)
arising from a use of ‘tickLabelFunction’
from the context: (TypeableFloat n, Renderable (Path V2 n) b)
bound by the type signature for:
renderColourBar :: forall n b.
(TypeableFloat n, Renderable (Path V2 n) b) =>
ColourBar b n
> ColourMap > (n, n) > n > QDiagram b V2 n Any
at Bug.hs:(204,1)(210,24)
The type variable ‘b0’ is ambiguous
Relevant bindings include
tickLabelXs :: [(n, String)] (bound at Bug.hs:229:3)
tickXs' :: [n] (bound at Bug.hs:226:3)
inRange :: n > Bool (bound at Bug.hs:222:3)
tickXs :: [n] (bound at Bug.hs:224:3)
l :: n (bound at Bug.hs:211:52)
ub :: n (bound at Bug.hs:211:48)
cbTickLabels :: TickLabels b V2 n (bound at Bug.hs:211:31)
(Some bindings suppressed; use fmaxrelevantbinds=N or fnomaxrelevantbinds)
These potential instance exist:
instance HasTickLabels f (TickLabels b v n) b
 Defined at Bug.hs:100:10
• In the first argument of ‘view’, namely ‘tickLabelFunction’
In the expression: view tickLabelFunction cbTickLabels tickXs' bnds
In an equation for ‘tickLabelXs’:
tickLabelXs = view tickLabelFunction cbTickLabels tickXs' bnds

229  tickLabelXs = view tickLabelFunction cbTickLabels tickXs' bnds
 ^^^^^^^^^^^^^^^^^
```
Moreover, this compiles with GHC 9.0.1rc1. This regression was introduced at some point between the following commits:
* 9183f5a537df159e37c26d9d385cf497bcfaae30 (`gitlabci: Don't run LLVM tests on Debian 9`). This commit has an artifact associated with it, and I can confirm that the bug is not present here.
* 0789f7a18a78920f50647e2b4aa8082a14ca9e90 (`Hadrian: show default ghcbignum backend (fix #18912)`)_Originally observed in a `head.hackage` CI build [here](https://gitlab.haskell.org/ghc/head.hackage//jobs/568397#L5617)_.
The `plots0.1.1.2` library fails to compile using commit 0789f7a18a78920f50647e2b4aa8082a14ca9e90 of the `ghc9.0` branch. Here is a selfcontained example with no external dependencies:
```hs
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE FunctionalDependencies #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE RecordWildCards #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeOperators #}
module Bug where
import Control.Monad.Reader
import Data.Functor.Const
import Data.Functor.Identity
import Data.Monoid (Any(..))
import Data.Typeable
type TypeableFloat n = (Typeable n, RealFloat n)
type Lens' s a = Lens s s a a
type Lens s t a b = forall f. Functor f => (a > f b) > s > f t
type LensLike' f s a = LensLike f s s a a
type LensLike f s t a b = (a > f b) > s > f t
type Getting r s a = (a > Const r a) > s > Const r s
type ASetter s t a b = (a > Identity b) > s > Identity t
data V2 a = V2 !a !a
flipX_Y :: Num n => V2 n > V2 n
flipX_Y (V2 x y) = V2 (y) (x)
class R1 t where
_x :: Lens' (t a) a
class R1 t => R2 t where
_y :: Lens' (t a) a
instance R1 V2 where
_x f (V2 a b) = (`V2` b) <$> f a
instance R2 V2 where
_y f (V2 a b) = V2 a <$> f b
infixl 8 #
(#) :: a > (a > b) > b
(#) = flip ($)
infixr 4 %~
(%~) :: ASetter s t a b > (a > b) > s > t
(%~) = over
(^.) :: s > Getting a s a > a
s ^. l = getConst (l Const s)
over :: ASetter s t a b > (a > b) > s > t
over l f = runIdentity . l (Identity . f)
view :: MonadReader s m => Getting a s a > m a
view l = asks (getConst . l Const)
lens :: (s > a) > (s > b > t) > Lens s t a b
lens sa sbt afb s = sbt s <$> afb (sa s)
type family V a :: * > *
type family N a :: *
type Vn a = V a (N a)
data Style (v :: * > *) n = Style
class HasStyle a where
applyStyle :: Style (V a) (N a) > a > a
type TextFunction b v n = TextAlignment n > String > QDiagram b v n Any
data TickLabels b (v :: * > *) n = TickLabels
{ tlFun :: [n] > (n,n) > [(n, String)]
, tlTextFun :: TextFunction b v n
, tlStyle :: Style v n
, tlGap :: n
}
type instance V (TickLabels b v n) = v
type instance N (TickLabels b v n) = n
class HasTickLabels f a b  a > b where
tickLabel :: LensLike' f a (TickLabels b (V a) (N a))
tickLabelTextFunction :: Functor f => LensLike' f a (TextFunction b (V a) (N a))
tickLabelTextFunction = tickLabel . lens tlTextFun (\tl f > tl {tlTextFun = f})
tickLabelFunction :: Functor f => LensLike' f a ([N a] > (N a, N a) > [(N a, String)])
tickLabelFunction = tickLabel . lens tlFun (\tl f > tl {tlFun = f})
tickLabelStyle :: Functor f => LensLike' f a (Style (V a) (N a))
tickLabelStyle = tickLabel . lens tlStyle (\tl sty > tl {tlStyle = sty})
tickLabelGap :: Functor f => LensLike' f a (N a)
tickLabelGap = tickLabel . lens tlGap (\tl n > tl {tlGap = n})
instance HasTickLabels f (TickLabels b v n) b where
tickLabel = id
data ColourBar b n = ColourBar
{ cbTickLabels :: TickLabels b V2 n
, cbTicks :: MajorTicks V2 n
, cbWidth :: n
}
type instance V (ColourBar b n) = V2
type instance N (ColourBar b n) = n
data MajorTicks (v :: * > *) n = MajorTicks
{ matFunction :: (n,n) > [n]
}
type instance V (MajorTicks v n) = v
type instance N (MajorTicks v n) = n
class HasMajorTicks f a where
majorTicks :: LensLike' f a (MajorTicks (V a) (N a))
majorTicksFunction :: Functor f => LensLike' f a ((N a, N a) > [N a])
majorTicksFunction = majorTicks . lens matFunction (\mat a > mat {matFunction = a})
instance HasMajorTicks f (MajorTicks v n) where
majorTicks = id
data Path (v :: * > *) n = Path
data (::) u v = (u > v) :: (v > u)
infixr 7 ::
instance Semigroup (a :: a) where
(f :: f') <> (g :: g') = f . g :: g' . f'
instance Monoid (v :: v) where
mempty = id :: id
data Transformation v n = Transformation (v n :: v n) (v n :: v n) (v n)
class Transformable t where
transform :: Transformation (V t) (N t) > t > t
translation :: v n > Transformation v n
translation = Transformation mempty mempty
translate :: (Transformable t) => Vn t > t > t
translate = transform . translation
class Transformable t => Renderable t b where
orient :: HasOrientation o => o > a > a > a
orient o h v =
case view orientation o of
Horizontal > h
Vertical > v
data Orientation = Horizontal  Vertical
class HasOrientation a where
orientation :: Lens' a Orientation
instance HasPlacement (ColourBar b n) where
placement = undefined
instance HasOrientation (ColourBar b n) where
orientation = undefined
instance Functor f => HasMajorTicks f (ColourBar b n) where
majorTicks = lens cbTicks (\c a > c {cbTicks = a})
data ColourMap = ColourMap
data QDiagram b (v :: * > *) n m = QD
instance Semigroup m  (Metric v, OrderedField n, Semigroup m)
=> HasStyle (QDiagram b v n m) where
applyStyle = undefined
instance Semigroup m  (Metric v, OrderedField n, Semigroup m)
=> Monoid (QDiagram b v n m) where
mempty = undefined
instance Semigroup m  (Metric v, OrderedField n, Semigroup m)
=> Semigroup (QDiagram b v n m) where
(<>) = undefined
instance Semigroup m  (OrderedField n, Metric v, Semigroup m)
=> Transformable (QDiagram b v n m) where
transform = undefined
type instance V (QDiagram b v n m) = v
type instance N (QDiagram b v n m) = n
data TextAlignment n = BaselineText  BoxAlignedText n n
data Placement = Placement
{ pAt :: V2 Rational
}
class HasPlacement a where
placement :: Lens' a Placement
placementAt :: Lens' a (V2 Rational)
placementAt = placement . lens pAt (\p a > p {pAt = a})
renderColourBar
:: forall n b. (TypeableFloat n, Renderable (Path V2 n) b)
=> ColourBar b n
> ColourMap
> (n,n)
> n
> QDiagram b V2 n Any
renderColourBar cb@ColourBar {..} _cm bnds@(lb,ub) l
= tLbs
where
o, xy :: a > a > a
o = orient cb
xy a b = if let V2 x y = cb^.placementAt in x > y
then a else b
w = cbWidth
f x = (x  (ub + lb)/2) / (ub  lb) * l
inRange x = x >= lb && x <= ub
tickXs = view majorTicksFunction cbTicks bnds
tickXs' :: [n]
tickXs' = filter inRange tickXs
tickLabelXs :: [(n, String)]
tickLabelXs = view tickLabelFunction cbTickLabels tickXs' bnds
tLbs :: QDiagram b V2 n Any
tLbs = foldMap drawTickLabel tickLabelXs
drawTickLabel :: (n, String) > QDiagram b (V (TickLabels b V2 n)) (N (TickLabels b V2 n)) Any
drawTickLabel (x,label) =
view tickLabelTextFunction cbTickLabels tAlign label
# translate v
# applyStyle (cbTickLabels ^. tickLabelStyle)
where v = V2 (f x) ( w/2  view tickLabelGap cbTickLabels)
# xy id (_y %~ negate)
# o id ((_y %~ negate) . flipX_Y)
tAlign = o (xy (BoxAlignedText 0.5 1) (BoxAlignedText 0.5 0))
(xy (BoxAlignedText 0 0.5) (BoxAlignedText 1 0.5))
```
This compiles with GHC 8.10.3 and earlier, but fails to compile with `ghc9.0`:
```
$ ~/Software/ghc9.0.0.20210130/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:229:22: error:
• Could not deduce (HasTickLabels
(Const ([n] > (n, n) > [(n, String)])) (TickLabels b V2 n) b0)
arising from a use of ‘tickLabelFunction’
from the context: (TypeableFloat n, Renderable (Path V2 n) b)
bound by the type signature for:
renderColourBar :: forall n b.
(TypeableFloat n, Renderable (Path V2 n) b) =>
ColourBar b n
> ColourMap > (n, n) > n > QDiagram b V2 n Any
at Bug.hs:(204,1)(210,24)
The type variable ‘b0’ is ambiguous
Relevant bindings include
tickLabelXs :: [(n, String)] (bound at Bug.hs:229:3)
tickXs' :: [n] (bound at Bug.hs:226:3)
inRange :: n > Bool (bound at Bug.hs:222:3)
tickXs :: [n] (bound at Bug.hs:224:3)
l :: n (bound at Bug.hs:211:52)
ub :: n (bound at Bug.hs:211:48)
cbTickLabels :: TickLabels b V2 n (bound at Bug.hs:211:31)
(Some bindings suppressed; use fmaxrelevantbinds=N or fnomaxrelevantbinds)
These potential instance exist:
instance HasTickLabels f (TickLabels b v n) b
 Defined at Bug.hs:100:10
• In the first argument of ‘view’, namely ‘tickLabelFunction’
In the expression: view tickLabelFunction cbTickLabels tickXs' bnds
In an equation for ‘tickLabelXs’:
tickLabelXs = view tickLabelFunction cbTickLabels tickXs' bnds

229  tickLabelXs = view tickLabelFunction cbTickLabels tickXs' bnds
 ^^^^^^^^^^^^^^^^^
```
Moreover, this compiles with GHC 9.0.1rc1. This regression was introduced at some point between the following commits:
* 9183f5a537df159e37c26d9d385cf497bcfaae30 (`gitlabci: Don't run LLVM tests on Debian 9`). This commit has an artifact associated with it, and I can confirm that the bug is not present here.
* 0789f7a18a78920f50647e2b4aa8082a14ca9e90 (`Hadrian: show default ghcbignum backend (fix #18912)`)9.0.2https://gitlab.haskell.org/ghc/ghc//issues/13655Spurious untouchable type variable in connection with rank2 type and constra...20210215T03:51:51ZWolfgang JeltschSpurious untouchable type variable in connection with rank2 type and constraint familyThe following code cannot be compiled:
```hs
{# LANGUAGE ConstraintKinds, Rank2Types, TypeFamilies #}
import GHC.Exts (Constraint)
type family F a b :: Constraint
data T b c = T
f :: (forall b . F a b => T b c) > a
f _ = undefined
```
GHC outputs the following error message:
```
Untouchable.hs:9:6: error:
• Couldn't match type ‘c0’ with ‘c’
‘c0’ is untouchable
inside the constraints: F a b
bound by the type signature for:
f :: F a b => T b c0
at Untouchable.hs:9:637
‘c’ is a rigid type variable bound by
the type signature for:
f :: forall a c. (forall b. F a b => T b c) > a
at Untouchable.hs:9:6
Expected type: T b c0
Actual type: T b c
• In the ambiguity check for ‘f’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature:
f :: (forall b. F a b => T b c) > a
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1rc2 
 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":"Spurious untouchable type variable in connection with rank2 type and constraint family","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1rc2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following code cannot be compiled:\r\n{{{#!hs\r\n{# LANGUAGE ConstraintKinds, Rank2Types, TypeFamilies #}\r\n\r\nimport GHC.Exts (Constraint)\r\n\r\ntype family F a b :: Constraint\r\n\r\ndata T b c = T\r\n\r\nf :: (forall b . F a b => T b c) > a\r\nf _ = undefined\r\n}}}\r\nGHC outputs the following error message:\r\n{{{\r\nUntouchable.hs:9:6: error:\r\n • Couldn't match type ‘c0’ with ‘c’\r\n ‘c0’ is untouchable\r\n inside the constraints: F a b\r\n bound by the type signature for:\r\n f :: F a b => T b c0\r\n at Untouchable.hs:9:637\r\n ‘c’ is a rigid type variable bound by\r\n the type signature for:\r\n f :: forall a c. (forall b. F a b => T b c) > a\r\n at Untouchable.hs:9:6\r\n Expected type: T b c0\r\n Actual type: T b c\r\n • In the ambiguity check for ‘f’\r\n To defer the ambiguity check to use sites, enable AllowAmbiguousTypes\r\n In the type signature:\r\n f :: (forall b. F a b => T b c) > a\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >The following code cannot be compiled:
```hs
{# LANGUAGE ConstraintKinds, Rank2Types, TypeFamilies #}
import GHC.Exts (Constraint)
type family F a b :: Constraint
data T b c = T
f :: (forall b . F a b => T b c) > a
f _ = undefined
```
GHC outputs the following error message:
```
Untouchable.hs:9:6: error:
• Couldn't match type ‘c0’ with ‘c’
‘c0’ is untouchable
inside the constraints: F a b
bound by the type signature for:
f :: F a b => T b c0
at Untouchable.hs:9:637
‘c’ is a rigid type variable bound by
the type signature for:
f :: forall a c. (forall b. F a b => T b c) > a
at Untouchable.hs:9:6
Expected type: T b c0
Actual type: T b c
• In the ambiguity check for ‘f’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature:
f :: (forall b. F a b => T b c) > a
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1rc2 
 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":"Spurious untouchable type variable in connection with rank2 type and constraint family","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1rc2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following code cannot be compiled:\r\n{{{#!hs\r\n{# LANGUAGE ConstraintKinds, Rank2Types, TypeFamilies #}\r\n\r\nimport GHC.Exts (Constraint)\r\n\r\ntype family F a b :: Constraint\r\n\r\ndata T b c = T\r\n\r\nf :: (forall b . F a b => T b c) > a\r\nf _ = undefined\r\n}}}\r\nGHC outputs the following error message:\r\n{{{\r\nUntouchable.hs:9:6: error:\r\n • Couldn't match type ‘c0’ with ‘c’\r\n ‘c0’ is untouchable\r\n inside the constraints: F a b\r\n bound by the type signature for:\r\n f :: F a b => T b c0\r\n at Untouchable.hs:9:637\r\n ‘c’ is a rigid type variable bound by\r\n the type signature for:\r\n f :: forall a c. (forall b. F a b => T b c) > a\r\n at Untouchable.hs:9:6\r\n Expected type: T b c0\r\n Actual type: T b c\r\n • In the ambiguity check for ‘f’\r\n To defer the ambiguity check to use sites, enable AllowAmbiguousTypes\r\n In the type signature:\r\n f :: (forall b. F a b => T b c) > a\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/17333Coercible solver does not look through "class newtypes"20210216T21:35:31ZRyan ScottCoercible solver does not look through "class newtypes"The code below makes use of the "class newtype" design pattern:
```hs
class Show a => MyShow a
instance Show a => MyShow a
```
`MyShow` is a newtype around `Show` in the sense that when compiled to Core, a `MyShow` dictionary is literally a newtype around `Show`. Unfortunately, this newtype treatment does not extend to the `Coercible` solver, as the following example demonstrates:
```hs
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE MonoLocalBinds #}
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE UndecidableInstances #}
{# LANGUAGE UndecidableSuperClasses #}
module Bug where
import Data.Coerce
class Show a => MyShow a
instance Show a => MyShow a
newtype T1 a = MkT1 ( Show a => a > a > String)
newtype T2 a = MkT2 (MyShow a => a > a > String)
f :: T1 a > T2 a
f = coerce
```
```
$ /opt/ghc/8.8.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:20:5: error:
• Couldn't match representation of type ‘MyShow a’
with that of ‘Show a’
arising from a use of ‘coerce’
The data constructor ‘Bug.C:MyShow’
of newtype ‘MyShow’ is not in scope
• In the expression: coerce
In an equation for ‘f’: f = coerce
• Relevant bindings include
f :: T1 a > T2 a (bound at Bug.hs:20:1)

20  f = coerce
 ^^^^^^
```
Somewhat surprisingly, this does not work. Even the error message indicates that `MyShow` is a newtype (which is a bit odd, but whatever), but since the internal `C:MyShow` constructor is not exposed, the `Coercible` solver doesn't have enough information to proceed.
If the following change is applied to GHC, then it typechecks:
```diff
diff git a/compiler/typecheck/FamInst.hs b/compiler/typecheck/FamInst.hs
index a339dd7b57..8640b3e3e0 100644
 a/compiler/typecheck/FamInst.hs
+++ b/compiler/typecheck/FamInst.hs
@@ 41,7 +41,7 @@ import Name
import Pair
import Panic
import VarSet
import Bag( Bag, unionBags, unitBag )
+import Bag( Bag, emptyBag, unionBags, unitBag )
import Control.Monad
#include "HsVersions.h"
@@ 577,6 +577,10 @@ tcTopNormaliseNewTypeTF_maybe faminsts rdr_env ty
= mapStepResult (\co > (unitBag gre, co)) $
unwrapNewTypeStepper rec_nts tc tys
+  isClassTyCon tc && isNewTyCon tc
+ = mapStepResult (\co > (emptyBag, co)) $
+ unwrapNewTypeStepper rec_nts tc tys
+
 otherwise
= NS_Done
```
The simplified example above is somewhat contrived, although I have legitimate need of this feature in more complicated scenarios like this one (inspired by [Generic Programming of All Kinds](https://victorcmiraldo.github.io/data/hask2018_draft.pdf)):
```hs
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE DataKinds #}
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE GADTs #}
{# LANGUAGE ImpredicativeTypes #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE TypeApplications #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeOperators #}
{# LANGUAGE UndecidableInstances #}
{# LANGUAGE UndecidableSuperClasses #}
module GOAK where
import Data.Coerce
import Data.Kind
newtype T = MkT ((forall a. Show a) => Int)
type TRep = Field (ForAllQ (Kon Show :@: Var VZ) :=>>: Kon Int) LoT0
f :: T > TRep
f (MkT x) = Field (coerce @((forall a. Show a) => Int)
@(Interpret (ForAllQ (Kon Show :@: Var VZ) :=>>: Kon Int) LoT0)
x)

infixr 5 :&&:
data LoT :: Type > Type where
LoT0 :: LoT Type
(:&&:) :: k > LoT ks > LoT (k > ks)
type family HeadLoT (tys :: LoT (k > k')) :: k where
HeadLoT (a :&&: _) = a
type family TailLoT (tys :: LoT (k > k')) :: LoT k' where
TailLoT (_ :&&: as) = as
data TyVar :: Type > Type > Type where
VZ :: TyVar (x > xs) x
VS :: TyVar xs k > TyVar (x > xs) k
data Atom :: Type > Type > Type where
Var :: TyVar d k > Atom d k
Kon :: k > Atom d k
(:@:) :: Atom d (k1 > k2) > Atom d k1 > Atom d k2
(:=>>:) :: Atom d Constraint > Atom d Type > Atom d Type
ForAllQ :: Atom (d1 > d) Constraint > Atom d Constraint
type family InterpretVar (t :: TyVar d k) (tys :: LoT d) :: k where
InterpretVar 'VZ tys = HeadLoT tys
InterpretVar ('VS v) tys = InterpretVar v (TailLoT tys)
type family Interpret (t :: Atom d k) (tys :: LoT d) :: k where
Interpret ('Var v) tys = InterpretVar v tys
Interpret ('Kon t) tys = t
Interpret (f ':@: x) tys = (Interpret f tys) (Interpret x tys)
Interpret (c ':=>>: f) tys = SuchThatI c f tys
Interpret (ForAllQ f) tys = ForAllQI f tys
newtype SuchThatI :: Atom d Constraint > Atom d Type > LoT d > Type where
SuchThatI :: (Interpret c tys => Interpret f tys) > SuchThatI c f tys
class (forall t. WrappedQI f (t ':&&: tys)) => ForAllQI (f :: Atom (d1 > d) Constraint) (tys :: LoT d)
instance (forall t. WrappedQI f (t ':&&: tys)) => ForAllQI (f :: Atom (d1 > d) Constraint) (tys :: LoT d)
class Interpret f tys => WrappedQI (f :: Atom d Constraint) (tys :: LoT d)
instance Interpret f tys => WrappedQI (f :: Atom d Constraint) (tys :: LoT d)
newtype Field :: Atom d Type > LoT d > Type where
Field :: { unField :: Interpret t x } > Field t x
```
`f` will not typecheck without the ability to coerce from `ForAllQI f tys` to `forall t. WrappedQI f (t ':&&: tys)`. Moreover, it would be extremely difficult to write `f` _without_ `coerce`.The code below makes use of the "class newtype" design pattern:
```hs
class Show a => MyShow a
instance Show a => MyShow a
```
`MyShow` is a newtype around `Show` in the sense that when compiled to Core, a `MyShow` dictionary is literally a newtype around `Show`. Unfortunately, this newtype treatment does not extend to the `Coercible` solver, as the following example demonstrates:
```hs
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE MonoLocalBinds #}
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE UndecidableInstances #}
{# LANGUAGE UndecidableSuperClasses #}
module Bug where
import Data.Coerce
class Show a => MyShow a
instance Show a => MyShow a
newtype T1 a = MkT1 ( Show a => a > a > String)
newtype T2 a = MkT2 (MyShow a => a > a > String)
f :: T1 a > T2 a
f = coerce
```
```
$ /opt/ghc/8.8.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:20:5: error:
• Couldn't match representation of type ‘MyShow a’
with that of ‘Show a’
arising from a use of ‘coerce’
The data constructor ‘Bug.C:MyShow’
of newtype ‘MyShow’ is not in scope
• In the expression: coerce
In an equation for ‘f’: f = coerce
• Relevant bindings include
f :: T1 a > T2 a (bound at Bug.hs:20:1)

20  f = coerce
 ^^^^^^
```
Somewhat surprisingly, this does not work. Even the error message indicates that `MyShow` is a newtype (which is a bit odd, but whatever), but since the internal `C:MyShow` constructor is not exposed, the `Coercible` solver doesn't have enough information to proceed.
If the following change is applied to GHC, then it typechecks:
```diff
diff git a/compiler/typecheck/FamInst.hs b/compiler/typecheck/FamInst.hs
index a339dd7b57..8640b3e3e0 100644
 a/compiler/typecheck/FamInst.hs
+++ b/compiler/typecheck/FamInst.hs
@@ 41,7 +41,7 @@ import Name
import Pair
import Panic
import VarSet
import Bag( Bag, unionBags, unitBag )
+import Bag( Bag, emptyBag, unionBags, unitBag )
import Control.Monad
#include "HsVersions.h"
@@ 577,6 +577,10 @@ tcTopNormaliseNewTypeTF_maybe faminsts rdr_env ty
= mapStepResult (\co > (unitBag gre, co)) $
unwrapNewTypeStepper rec_nts tc tys
+  isClassTyCon tc && isNewTyCon tc
+ = mapStepResult (\co > (emptyBag, co)) $
+ unwrapNewTypeStepper rec_nts tc tys
+
 otherwise
= NS_Done
```
The simplified example above is somewhat contrived, although I have legitimate need of this feature in more complicated scenarios like this one (inspired by [Generic Programming of All Kinds](https://victorcmiraldo.github.io/data/hask2018_draft.pdf)):
```hs
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE DataKinds #}
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE GADTs #}
{# LANGUAGE ImpredicativeTypes #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE TypeApplications #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeOperators #}
{# LANGUAGE UndecidableInstances #}
{# LANGUAGE UndecidableSuperClasses #}
module GOAK where
import Data.Coerce
import Data.Kind
newtype T = MkT ((forall a. Show a) => Int)
type TRep = Field (ForAllQ (Kon Show :@: Var VZ) :=>>: Kon Int) LoT0
f :: T > TRep
f (MkT x) = Field (coerce @((forall a. Show a) => Int)
@(Interpret (ForAllQ (Kon Show :@: Var VZ) :=>>: Kon Int) LoT0)
x)

infixr 5 :&&:
data LoT :: Type > Type where
LoT0 :: LoT Type
(:&&:) :: k > LoT ks > LoT (k > ks)
type family HeadLoT (tys :: LoT (k > k')) :: k where
HeadLoT (a :&&: _) = a
type family TailLoT (tys :: LoT (k > k')) :: LoT k' where
TailLoT (_ :&&: as) = as
data TyVar :: Type > Type > Type where
VZ :: TyVar (x > xs) x
VS :: TyVar xs k > TyVar (x > xs) k
data Atom :: Type > Type > Type where
Var :: TyVar d k > Atom d k
Kon :: k > Atom d k
(:@:) :: Atom d (k1 > k2) > Atom d k1 > Atom d k2
(:=>>:) :: Atom d Constraint > Atom d Type > Atom d Type
ForAllQ :: Atom (d1 > d) Constraint > Atom d Constraint
type family InterpretVar (t :: TyVar d k) (tys :: LoT d) :: k where
InterpretVar 'VZ tys = HeadLoT tys
InterpretVar ('VS v) tys = InterpretVar v (TailLoT tys)
type family Interpret (t :: Atom d k) (tys :: LoT d) :: k where
Interpret ('Var v) tys = InterpretVar v tys
Interpret ('Kon t) tys = t
Interpret (f ':@: x) tys = (Interpret f tys) (Interpret x tys)
Interpret (c ':=>>: f) tys = SuchThatI c f tys
Interpret (ForAllQ f) tys = ForAllQI f tys
newtype SuchThatI :: Atom d Constraint > Atom d Type > LoT d > Type where
SuchThatI :: (Interpret c tys => Interpret f tys) > SuchThatI c f tys
class (forall t. WrappedQI f (t ':&&: tys)) => ForAllQI (f :: Atom (d1 > d) Constraint) (tys :: LoT d)
instance (forall t. WrappedQI f (t ':&&: tys)) => ForAllQI (f :: Atom (d1 > d) Constraint) (tys :: LoT d)
class Interpret f tys => WrappedQI (f :: Atom d Constraint) (tys :: LoT d)
instance Interpret f tys => WrappedQI (f :: Atom d Constraint) (tys :: LoT d)
newtype Field :: Atom d Type > LoT d > Type where
Field :: { unField :: Interpret t x } > Field t x
```
`f` will not typecheck without the ability to coerce from `ForAllQI f tys` to `forall t. WrappedQI f (t ':&&: tys)`. Moreover, it would be extremely difficult to write `f` _without_ `coerce`.https://gitlab.haskell.org/ghc/ghc//issues/19131Does the subtype check in Note [Impedance matching] ever fail?20210217T13:00:27ZRichard Eisenbergrae@richarde.devDoes the subtype check in Note [Impedance matching] ever fail?`GHC.Tc.Gen.Bind` tells us
```
Note [Impedance matching]
~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
f 0 x = x
f n x = g [] (not x)
g [] y = f 10 y
g _ y = f 9 y
After typechecking we'll get
f_mono_ty :: a > Bool > Bool
g_mono_ty :: [b] > Bool > Bool
with constraints
(Eq a, Num a)
Note that f is polymorphic in 'a' and g in 'b'; and these are not linked.
The types we really want for f and g are
f :: forall a. (Eq a, Num a) => a > Bool > Bool
g :: forall b. [b] > Bool > Bool
We can get these by "impedance matching":
tuple :: forall a b. (Eq a, Num a) => (a > Bool > Bool, [b] > Bool > Bool)
tuple a b d1 d1 = let ...bind f_mono, g_mono in (f_mono, g_mono)
f a d1 d2 = case tuple a Any d1 d2 of (f, g) > f
g b = case tuple Integer b dEqInteger dNumInteger of (f,g) > g
Suppose the shared quantified tyvars are qtvs and constraints theta.
Then we want to check that
forall qtvs. theta => f_mono_ty is more polymorphic than f's polytype
and the proof is the impedance matcher.
Notice that the impedance matcher may do defaulting. See #7173.
It also cleverly does an ambiguity check; for example, rejecting
f :: F a > F a
where F is a noninjective type function.
```
This describes a subtype check. That subtype check is performed with the context returned from this function:
```hs
mk_impedance_match_msg :: MonoBindInfo
> TcType > TcType
> TidyEnv > TcM (TidyEnv, SDoc)
 This is a rare but rather awkward error messages
mk_impedance_match_msg (MBI { mbi_poly_name = name, mbi_sig = mb_sig })
inf_ty sig_ty tidy_env
= do { (tidy_env1, inf_ty) < zonkTidyTcType tidy_env inf_ty
; (tidy_env2, sig_ty) < zonkTidyTcType tidy_env1 sig_ty
; let msg = vcat [ text "When checking that the inferred type"
, nest 2 $ ppr name <+> dcolon <+> ppr inf_ty
, text "is as general as its" <+> what <+> text "signature"
, nest 2 $ ppr name <+> dcolon <+> ppr sig_ty ]
; return (tidy_env2, msg) }
where
what = case mb_sig of
Nothing > text "inferred"
Just sig  isPartialSig sig > text "(partial)"
 otherwise > empty
```
A search in the testsuite shows no occurrence of "When checking that the inferred type".
So: Does this subtype check ever fail? If so, we should have a test case in the testsuite for this message. If not, we should explain why failure is impossible and then remove the above function.`GHC.Tc.Gen.Bind` tells us
```
Note [Impedance matching]
~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
f 0 x = x
f n x = g [] (not x)
g [] y = f 10 y
g _ y = f 9 y
After typechecking we'll get
f_mono_ty :: a > Bool > Bool
g_mono_ty :: [b] > Bool > Bool
with constraints
(Eq a, Num a)
Note that f is polymorphic in 'a' and g in 'b'; and these are not linked.
The types we really want for f and g are
f :: forall a. (Eq a, Num a) => a > Bool > Bool
g :: forall b. [b] > Bool > Bool
We can get these by "impedance matching":
tuple :: forall a b. (Eq a, Num a) => (a > Bool > Bool, [b] > Bool > Bool)
tuple a b d1 d1 = let ...bind f_mono, g_mono in (f_mono, g_mono)
f a d1 d2 = case tuple a Any d1 d2 of (f, g) > f
g b = case tuple Integer b dEqInteger dNumInteger of (f,g) > g
Suppose the shared quantified tyvars are qtvs and constraints theta.
Then we want to check that
forall qtvs. theta => f_mono_ty is more polymorphic than f's polytype
and the proof is the impedance matcher.
Notice that the impedance matcher may do defaulting. See #7173.
It also cleverly does an ambiguity check; for example, rejecting
f :: F a > F a
where F is a noninjective type function.
```
This describes a subtype check. That subtype check is performed with the context returned from this function:
```hs
mk_impedance_match_msg :: MonoBindInfo
> TcType > TcType
> TidyEnv > TcM (TidyEnv, SDoc)
 This is a rare but rather awkward error messages
mk_impedance_match_msg (MBI { mbi_poly_name = name, mbi_sig = mb_sig })
inf_ty sig_ty tidy_env
= do { (tidy_env1, inf_ty) < zonkTidyTcType tidy_env inf_ty
; (tidy_env2, sig_ty) < zonkTidyTcType tidy_env1 sig_ty
; let msg = vcat [ text "When checking that the inferred type"
, nest 2 $ ppr name <+> dcolon <+> ppr inf_ty
, text "is as general as its" <+> what <+> text "signature"
, nest 2 $ ppr name <+> dcolon <+> ppr sig_ty ]
; return (tidy_env2, msg) }
where
what = case mb_sig of
Nothing > text "inferred"
Just sig  isPartialSig sig > text "(partial)"
 otherwise > empty
```
A search in the testsuite shows no occurrence of "When checking that the inferred type".
So: Does this subtype check ever fail? If so, we should have a test case in the testsuite for this message. If not, we should explain why failure is impossible and then remove the above function.