GHC issueshttps://gitlab.haskell.org/ghc/ghc//issues20200930T21:23:04Zhttps://gitlab.haskell.org/ghc/ghc//issues/18704GHC could not deduce constraint from itself20200930T21:23:04ZrybochodonezzarGHC could not deduce constraint from itself## Summary
following code:
```haskell
{# LANGUAGE GADTs, DataKinds, PolyKinds, ConstraintKinds, TypeApplications, RankNTypes, TypeFamilies, TypeOperators, MultiParamTypeClasses, UndecidableSuperClasses, FlexibleInstances, PatternSynonyms, FlexibleContexts, AllowAmbiguousTypes, ScopedTypeVariables #}
module Lib where
import GHC.Exts
import GHC.TypeLits
import Data.Proxy
data a ::: b = a ::: b
class Pair f where
type Left f :: a
type Right f :: b
instance Pair (a '::: b) where
type Left (a '::: b) = a
type Right (a '::: b) = b
class NC (x :: k)
instance NC (x :: k)
data L1 c f xs where
LC :: c x => f x > L1 c f xs > L1 c f (x ': xs)
LN :: L1 c f '[]
class (c1 (Left f), c2 (Right f)) => PairC c1 c2 f
instance (c1 x, c2 y) => PairC c1 c2 (x '::: y)
data f1 :*: f2 :: (kx ::: ky) > * where
(:*:) :: f1 x > f2 y > (f1 :*: f2) (x '::: y)
pairC :: forall c1 c2 x y e . (c1 x, c2 y) => (PairC c1 c2 (x '::: y) => e) > e
pairC e = e
type Foo t = L1 (PairC KnownSymbol NC) (Proxy :*: t)
pattern Foo :: forall s a t xs . KnownSymbol s => KnownSymbol s => Proxy s > t a > Foo t xs > Foo t (s '::: a ': xs)
pattern Foo p t xs < LC (p :*: t) xs where
Foo p t xs = pairC @KnownSymbol @NC @s @a (LC (p :*: t) xs)
```
Results in this compile error:
```
/home/ryba/ghcbug/src/Lib.hs:38:46: error:
• Could not deduce (PairC KnownSymbol NC (s '::: a))
arising from a use of ‘LC’
from the context: KnownSymbol s
bound by the signature for pattern synonym ‘Foo’
at src/Lib.hs:(37,1)(38,61)
or from: PairC KnownSymbol NC (s '::: a)
bound by a type expected by the context:
PairC KnownSymbol NC (s '::: a) =>
L1 (PairC KnownSymbol NC) (Proxy :*: t) ((s '::: a) : xs)
at src/Lib.hs:38:4561
• In the fifth argument of ‘pairC’, namely ‘(LC (p :*: t) xs)’
In the expression: pairC @KnownSymbol @NC @s @a (LC (p :*: t) xs)
In an equation for ‘Foo’:
Foo p t xs = pairC @KnownSymbol @NC @s @a (LC (p :*: t) xs)

38  Foo p t xs = pairC @KnownSymbol @NC @s @a (LC (p :*: t) xs)
 ^^^^^^^^^^^^^^^
```
Which basically boils down to "could not deduce a from a"
## Environment
* GHC version used: 8.10.2
* stack resolver=nightly20200914
Optional:
* Operating System: Ubuntu
* System Architecture: x8664## Summary
following code:
```haskell
{# LANGUAGE GADTs, DataKinds, PolyKinds, ConstraintKinds, TypeApplications, RankNTypes, TypeFamilies, TypeOperators, MultiParamTypeClasses, UndecidableSuperClasses, FlexibleInstances, PatternSynonyms, FlexibleContexts, AllowAmbiguousTypes, ScopedTypeVariables #}
module Lib where
import GHC.Exts
import GHC.TypeLits
import Data.Proxy
data a ::: b = a ::: b
class Pair f where
type Left f :: a
type Right f :: b
instance Pair (a '::: b) where
type Left (a '::: b) = a
type Right (a '::: b) = b
class NC (x :: k)
instance NC (x :: k)
data L1 c f xs where
LC :: c x => f x > L1 c f xs > L1 c f (x ': xs)
LN :: L1 c f '[]
class (c1 (Left f), c2 (Right f)) => PairC c1 c2 f
instance (c1 x, c2 y) => PairC c1 c2 (x '::: y)
data f1 :*: f2 :: (kx ::: ky) > * where
(:*:) :: f1 x > f2 y > (f1 :*: f2) (x '::: y)
pairC :: forall c1 c2 x y e . (c1 x, c2 y) => (PairC c1 c2 (x '::: y) => e) > e
pairC e = e
type Foo t = L1 (PairC KnownSymbol NC) (Proxy :*: t)
pattern Foo :: forall s a t xs . KnownSymbol s => KnownSymbol s => Proxy s > t a > Foo t xs > Foo t (s '::: a ': xs)
pattern Foo p t xs < LC (p :*: t) xs where
Foo p t xs = pairC @KnownSymbol @NC @s @a (LC (p :*: t) xs)
```
Results in this compile error:
```
/home/ryba/ghcbug/src/Lib.hs:38:46: error:
• Could not deduce (PairC KnownSymbol NC (s '::: a))
arising from a use of ‘LC’
from the context: KnownSymbol s
bound by the signature for pattern synonym ‘Foo’
at src/Lib.hs:(37,1)(38,61)
or from: PairC KnownSymbol NC (s '::: a)
bound by a type expected by the context:
PairC KnownSymbol NC (s '::: a) =>
L1 (PairC KnownSymbol NC) (Proxy :*: t) ((s '::: a) : xs)
at src/Lib.hs:38:4561
• In the fifth argument of ‘pairC’, namely ‘(LC (p :*: t) xs)’
In the expression: pairC @KnownSymbol @NC @s @a (LC (p :*: t) xs)
In an equation for ‘Foo’:
Foo p t xs = pairC @KnownSymbol @NC @s @a (LC (p :*: t) xs)

38  Foo p t xs = pairC @KnownSymbol @NC @s @a (LC (p :*: t) xs)
 ^^^^^^^^^^^^^^^
```
Which basically boils down to "could not deduce a from a"
## Environment
* GHC version used: 8.10.2
* stack resolver=nightly20200914
Optional:
* Operating System: Ubuntu
* System Architecture: x8664https://gitlab.haskell.org/ghc/ghc//issues/18689Why check for fdefertypeerrors in metaTyVarUpdateOK?20201222T13:22:39ZRichard Eisenbergrae@richarde.devWhy check for fdefertypeerrors in metaTyVarUpdateOK?Function `checkTypeEq` changes its behavior depending on the presence of `fdefertypeerrors` in an obscure case around heterogeneous equalities; see the code in `go_co`. This is undocumented (in the code), and neither Simon nor I can figure out why it's done.
Task: figure this out, and either document or remove this behavior.Function `checkTypeEq` changes its behavior depending on the presence of `fdefertypeerrors` in an obscure case around heterogeneous equalities; see the code in `go_co`. This is undocumented (in the code), and neither Simon nor I can figure out why it's done.
Task: figure this out, and either document or remove this behavior.Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/18645Incremental `tcCheckSatisfiability` API20200914T13:16:06ZSebastian GrafIncremental `tcCheckSatisfiability` APIThe patternmatch checker makes use of the function `tcCheckSatisfiability :: Bag EvVar > TcM Bool` (henceforth `tcCS`) offered by the typechecker to solve type constraints. Over the course of a patternmatch checking session, such a `Bag EvVar` is accumulated and incrementally checked after each addition. As #17836 shows in a rather painful way, that scales quadratically, because the typechecker chews through the same type constraints over and over again.
But look at how the patternmatch checker uses `tcCS`:
```hs
  Add some extra type constraints to the 'TyState'; return 'Nothing' if we
 find a contradiction (e.g. @Int ~ Bool@).
tyOracle :: TyState > Bag PredType > DsM (Maybe TyState)
tyOracle (TySt inert) cts
= do { evs < traverse nameTyCt cts
; let new_inert = inert `unionBags` evs
; ... < initTcDsForSolver $ tcCheckSatisfiability new_inert
; ... }
```
The `inert` set is a `Bag EvVar` for which *we already know they are compatible with each other*, as they were checked by `tcCS` in a previous call. Only `cts :: Bag PredType` are unchecked. And as far as the patternmatch checker is concerned, the type of `inert` is completely opaque, so the API to `tcCS` could very well be
```hs
tcCheckSatisfiability :: TcInert > Bag EvVar > TcM (Maybe TcInert)
  Add some extra type constraints to the 'TyState'; return 'Nothing' if we
 find a contradiction (e.g. @Int ~ Bool@).
tyOracle :: TyState > Bag PredType > DsM (Maybe TyState)
tyOracle (TySt inert) cts
= do { evs < traverse nameTyCt cts
; ...mb_new_inert... < initTcDsForSolver $ tcCheckSatisfiability inert evs
; ... }
```
I'm sure there already is something like `TcInert` in the typechecker. Looking at the implementation of `tcCS`, that might be the unused `EvBindMap`, but I'm not sure. Or is it the `InertCans` in `getInertCans`/`setInertCans`? CC @rae, @RyanGlScott, @simonpj
This blocks #17836 and would probably lead to quite a few (possibly rather drastic) metric decreases in other cases.The patternmatch checker makes use of the function `tcCheckSatisfiability :: Bag EvVar > TcM Bool` (henceforth `tcCS`) offered by the typechecker to solve type constraints. Over the course of a patternmatch checking session, such a `Bag EvVar` is accumulated and incrementally checked after each addition. As #17836 shows in a rather painful way, that scales quadratically, because the typechecker chews through the same type constraints over and over again.
But look at how the patternmatch checker uses `tcCS`:
```hs
  Add some extra type constraints to the 'TyState'; return 'Nothing' if we
 find a contradiction (e.g. @Int ~ Bool@).
tyOracle :: TyState > Bag PredType > DsM (Maybe TyState)
tyOracle (TySt inert) cts
= do { evs < traverse nameTyCt cts
; let new_inert = inert `unionBags` evs
; ... < initTcDsForSolver $ tcCheckSatisfiability new_inert
; ... }
```
The `inert` set is a `Bag EvVar` for which *we already know they are compatible with each other*, as they were checked by `tcCS` in a previous call. Only `cts :: Bag PredType` are unchecked. And as far as the patternmatch checker is concerned, the type of `inert` is completely opaque, so the API to `tcCS` could very well be
```hs
tcCheckSatisfiability :: TcInert > Bag EvVar > TcM (Maybe TcInert)
  Add some extra type constraints to the 'TyState'; return 'Nothing' if we
 find a contradiction (e.g. @Int ~ Bool@).
tyOracle :: TyState > Bag PredType > DsM (Maybe TyState)
tyOracle (TySt inert) cts
= do { evs < traverse nameTyCt cts
; ...mb_new_inert... < initTcDsForSolver $ tcCheckSatisfiability inert evs
; ... }
```
I'm sure there already is something like `TcInert` in the typechecker. Looking at the implementation of `tcCS`, that might be the unused `EvBindMap`, but I'm not sure. Or is it the `InertCans` in `getInertCans`/`setInertCans`? CC @rae, @RyanGlScott, @simonpj
This blocks #17836 and would probably lead to quite a few (possibly rather drastic) metric decreases in other cases.https://gitlab.haskell.org/ghc/ghc//issues/18542Kind error when using partial type signatures20200806T21:34:14Zlennart@augustsson.netKind error when using partial type signatures## Summary
When using a partial type signature I get a kind error, which is surprising.
## Steps to reproduce
Compile the following module. The function bar type checks, whereas baz gets a kind error
```
{# LANGUAGE RankNTypes #}
module Bug where
foo :: (Functor g) =>
(forall aa . Num aa => f aa > g aa) >
f a > g (f a)
foo f x = undefined
bar :: (forall aa . Num aa => f aa > Int > aa) >
f a > Int > f a
bar f = foo f
baz :: (forall aa . Num aa => f aa > Int > aa) >
f a > _ > f a
baz f = foo f
```
## Environment
* GHC version used:
The Glorious Glasgow Haskell Compilation System, version 8.10.1## Summary
When using a partial type signature I get a kind error, which is surprising.
## Steps to reproduce
Compile the following module. The function bar type checks, whereas baz gets a kind error
```
{# LANGUAGE RankNTypes #}
module Bug where
foo :: (Functor g) =>
(forall aa . Num aa => f aa > g aa) >
f a > g (f a)
foo f x = undefined
bar :: (forall aa . Num aa => f aa > Int > aa) >
f a > Int > f a
bar f = foo f
baz :: (forall aa . Num aa => f aa > Int > aa) >
f a > _ > f a
baz f = foo f
```
## Environment
* GHC version used:
The Glorious Glasgow Haskell Compilation System, version 8.10.19.2.1https://gitlab.haskell.org/ghc/ghc//issues/18529GHC fails to infer type with FlexibleContexts20200930T21:32:01ZRichard Eisenbergrae@richarde.devGHC fails to infer type with FlexibleContextsIf I say
```hs
{# LANGUAGE MultiParamTypeClasses, FlexibleContexts #}
module Bug where
class C a b where
op :: a > b > ()
 foo :: (C a Integer) => a > ()
foo x = op x 3
```
then GHC complains that the variable `b0` in the type of `foo` is ambiguous, because it tries to produce `C a b => a > ()` as the type of `foo`. Instead, it shouldn't quantify `b`, letting it default to `Integer`.
The solution is to use `oclose` instead of `growThetaTyVars` in `decideQuantifiedTyVars`. This will respect functional dependencies, quantifying over `b` only when a fundep exists from `a` to `b`.
I will fix in ongoing work (in the `wip/derivedrefactor` branch).If I say
```hs
{# LANGUAGE MultiParamTypeClasses, FlexibleContexts #}
module Bug where
class C a b where
op :: a > b > ()
 foo :: (C a Integer) => a > ()
foo x = op x 3
```
then GHC complains that the variable `b0` in the type of `foo` is ambiguous, because it tries to produce `C a b => a > ()` as the type of `foo`. Instead, it shouldn't quantify `b`, letting it default to `Integer`.
The solution is to use `oclose` instead of `growThetaTyVars` in `decideQuantifiedTyVars`. This will respect functional dependencies, quantifying over `b` only when a fundep exists from `a` to `b`.
I will fix in ongoing work (in the `wip/derivedrefactor` branch).Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/18481Improve instantiation of datacons20200721T08:48:13ZKrzysztof GogolewskiImprove instantiation of dataconsThis ticket tracks a possible improvement to `return_data_con`.
When typechecking a datacon `T`, do we instantiate its arguments? We'd like to avoid instantiation, because it breaks VTA.
Currently, we instantiate levitypolymorphic constructors. Quoting Note [Linear fields generalization]:
```
A small hitch: if the constructor is levitypolymorphic (unboxed tuples, sums,
certain newtypes with XUnliftedNewtypes) then this strategy produces
\r1 r2 a b (x # p :: a) (y # q :: b) > (# a, b #)
Which has type
forall r1 r2 a b. a #p> b #q> (# a, b #)
Which violates the levitypolymorphism restriction see Note [Levity polymorphism
checking] in DsMonad.
So we really must instantiate r1 and r2 rather than quantify over them. For
simplicity, we just instantiate the entire type, as described in Note
[Instantiating stupid theta]. It breaks visible type application with unboxed
tuples, sums and levitypolymorphic newtypes, but this doesn't appear to be used
anywhere.
A better plan: let's force all representation variable to be *inferred*, so that
they are not subject to visible type applications. Then we can instantiate
inferred argument eagerly.
```
The goal of this ticket is to implement the last paragraph.This ticket tracks a possible improvement to `return_data_con`.
When typechecking a datacon `T`, do we instantiate its arguments? We'd like to avoid instantiation, because it breaks VTA.
Currently, we instantiate levitypolymorphic constructors. Quoting Note [Linear fields generalization]:
```
A small hitch: if the constructor is levitypolymorphic (unboxed tuples, sums,
certain newtypes with XUnliftedNewtypes) then this strategy produces
\r1 r2 a b (x # p :: a) (y # q :: b) > (# a, b #)
Which has type
forall r1 r2 a b. a #p> b #q> (# a, b #)
Which violates the levitypolymorphism restriction see Note [Levity polymorphism
checking] in DsMonad.
So we really must instantiate r1 and r2 rather than quantify over them. For
simplicity, we just instantiate the entire type, as described in Note
[Instantiating stupid theta]. It breaks visible type application with unboxed
tuples, sums and levitypolymorphic newtypes, but this doesn't appear to be used
anywhere.
A better plan: let's force all representation variable to be *inferred*, so that
they are not subject to visible type applications. Then we can instantiate
inferred argument eagerly.
```
The goal of this ticket is to implement the last paragraph.https://gitlab.haskell.org/ghc/ghc//issues/18456"equirecursive" type family leads to stack overflow in ghci20200717T13:59:54ZXia Liyao"equirecursive" type family leads to stack overflow in ghci## Summary
Trying to typecheck a term using a (silly) type family such that `T ~ Maybe T` leads to a stack overflow (instead of a proper type error from reaching the max reduction depth, if this is to be an error at all).
## Steps to reproduce
```
> :set XTypeFamilies XUndecidableInstances
> type family T where T = Maybe T
> :t Nothing @T
Nothing @T*** Exception: stack overflow
```
(where the exception takes a few seconds to appear)
Compare that output to this variant that immediately produces a proper type error:
```
> :t Nothing @T :: T
<interactive>:5:1 error:
...
```
## Expected behavior
Either a success (`Nothing @T` has type `Maybe T` without requiring any type conversion), or a type error instead of an internal exception.
## Environment
* GHC version used: 8.10.1## Summary
Trying to typecheck a term using a (silly) type family such that `T ~ Maybe T` leads to a stack overflow (instead of a proper type error from reaching the max reduction depth, if this is to be an error at all).
## Steps to reproduce
```
> :set XTypeFamilies XUndecidableInstances
> type family T where T = Maybe T
> :t Nothing @T
Nothing @T*** Exception: stack overflow
```
(where the exception takes a few seconds to appear)
Compare that output to this variant that immediately produces a proper type error:
```
> :t Nothing @T :: T
<interactive>:5:1 error:
...
```
## Expected behavior
Either a success (`Nothing @T` has type `Maybe T` without requiring any type conversion), or a type error instead of an internal exception.
## Environment
* GHC version used: 8.10.1https://gitlab.haskell.org/ghc/ghc//issues/18451Infinite loop during kind inference20200727T08:10:18ZSimon Peyton JonesInfinite loop during kind inferenceThis program
```
{# LANGUAGE RankNTypes #}
{# LANGUAGE TypeInType #}
module Bug where
import Data.Kind
type Const a b = a
data SameKind :: k > k > Type
type T (k :: Const Type a) = forall (b :: k). SameKind a b
```
goes into an infinite loop during kind checking. (Extracted from #16245.)
We have
```
a_agk :: k_au5
k_atM :: Const Type a_agk
k_au5 := k_au7
```
and then we try to unify `k_au7 := k_atM`. That should be an occurscheck error, since `k_atM`'s kind mentions `a_agk`, whose kind mentions `k_au5`, which is equal to `k_au7`.
But `occCheckExpand` (called from `GHC.Tc.Utils.Unify.metaTyVarUpdateOK`) expands the `Const` synonym in `k_atM`'s kind so that it no longer mentions `a_agk`, which allows the update to go ahead.
Wrong! We can't do this `occCheckExpand` business inside kinds! Let's just not do that.This program
```
{# LANGUAGE RankNTypes #}
{# LANGUAGE TypeInType #}
module Bug where
import Data.Kind
type Const a b = a
data SameKind :: k > k > Type
type T (k :: Const Type a) = forall (b :: k). SameKind a b
```
goes into an infinite loop during kind checking. (Extracted from #16245.)
We have
```
a_agk :: k_au5
k_atM :: Const Type a_agk
k_au5 := k_au7
```
and then we try to unify `k_au7 := k_atM`. That should be an occurscheck error, since `k_atM`'s kind mentions `a_agk`, whose kind mentions `k_au5`, which is equal to `k_au7`.
But `occCheckExpand` (called from `GHC.Tc.Utils.Unify.metaTyVarUpdateOK`) expands the `Const` synonym in `k_atM`'s kind so that it no longer mentions `a_agk`, which allows the update to go ahead.
Wrong! We can't do this `occCheckExpand` business inside kinds! Let's just not do that.https://gitlab.haskell.org/ghc/ghc//issues/18439Pattern guards can break linearity20210108T16:49:06ZArnaud SpiwackPattern guards can break linearity## Summary
Patterns, in patternguards guards are not checked for linearity. Which let's us write incorrect program with respect to linearity. The linter rightfully rejects those.
## Steps to reproduce
This typechecks but should not:
```
{# LANGUAGE LinearTypes #}
unsafeConsume :: a #> ()
unsafeConsume x  _ < x = ()
```
## Environment
* GHC version used: master 3656dff8259199d0dab2d1a1f1b887c252a9c1a3
## Note
Originally reported by Roman Cheplyaka.## Summary
Patterns, in patternguards guards are not checked for linearity. Which let's us write incorrect program with respect to linearity. The linter rightfully rejects those.
## Steps to reproduce
This typechecks but should not:
```
{# LANGUAGE LinearTypes #}
unsafeConsume :: a #> ()
unsafeConsume x  _ < x = ()
```
## Environment
* GHC version used: master 3656dff8259199d0dab2d1a1f1b887c252a9c1a3
## Note
Originally reported by Roman Cheplyaka.Arnaud SpiwackArnaud Spiwackhttps://gitlab.haskell.org/ghc/ghc//issues/18413Suboptimal constraint solving20201109T16:27:10ZSimon Peyton JonesSuboptimal constraint solvingHere a summary of `ddumptctrace` for this program (part of test T12427a)
```
data T where
T1 :: a > ((forall b. [b]>[b]) > Int) > T
h11 y = case y of T1 _ v > v
```
I see this sequence
```
{co_awA} {0}:: ((forall b. [b] > [b]) > Int)
~# p_awz[tau:1] (CNonCanonical)
==> Hetero equality gives rise to kind equality
inert: {co_awG} :: p_awz[tau:1] ~# ((forall b. [b] > [b]) > Int > (TYPE {co_awF})_N)
work item: {co_awF} :: 'GHC.Types.LiftedRep ~# p_awy[tau:1]
co_awA := Sym ({co_awG} ; Sym (GRefl nominal ((forall b.[b] > [b]) > Int)
(TYPE {co_awF})_N))
==> Swap awF, kick out awG
work item: {co_awG} :: p_awz[tau:1] ~# ((forall b. [b] > [b]) > Int > (TYPE {co_awF})_N)
inert (because p_awy is untouchable):
{co_awH} :: p_awy[tau:1] ~# 'GHC.Types.LiftedRep
co_awF := Sym co_awH
==> flatten awG (strange double GRefl)
inert: {co_awH} :: p_awy[tau:1] ~# 'GHC.Types.LiftedRep
inert: {co_awI} :: p_awz[tau:1] ~# ((forall b. [b] > [b]) > Int > (TYPE (Sym {co_awH}))_N)
co_awG := {co_awI} ; (Sym (GRefl nominal ((forall b. [b] > [b]) > Int)
(TYPE (Sym {co_awH}))_N)
; GRefl nominal ((forall b. [b] > [b]) > Int)
(TYPE {co_awF})_N)
at this point we also make a derived shadow of awI, for some reason.
Solving stops here, but we float out awI, and awH, and then have another go
work: {co_awH} :: p_awy[tau:1] ~# 'GHC.Types.LiftedRep
work: {co_awI} :: p_awz[tau:1] ~# ((forall b. [b] > [b]) > Int > (TYPE (Sym {co_awH}))_N)
==> flatten awI (why?)
work: {co_awH} :: p_awy[tau:1] ~# 'GHC.Types.LiftedRep
inert: {co_awJ} :: p_awz[tau:1] ~# ((forall b. [b] > [b]) > Int > (TYPE (Sym {co_awH}))_N)
co_awI := {co_awJ} ; (Sym (GRefl nominal ((forall b. [b] > [b]) > Int)
(TYPE (Sym {co_awH}))_N) ; GRefl nominal ((forall b. [b] > [b])
> Int)
(TYPE (Sym {co_awH}))_N)
==> solve awH: p_awy := LiftedRep, kick out awJ
{co_awJ} :: p_awz[tau:1] ~# ((forall b. [b] > [b]) > Int > (TYPE (Sym {co_awH}))_N)
==> flatten awJ
co_awJ := {co_awK} ; GRefl nominal ((forall b. [b] > [b]) > Int)
(TYPE (Sym {co_awH}))_N
{co_awK} :: p_awz[tau:1] ~# ((forall b. [b] > [b]) > Int)
```
This seems like we are doing too much work, esp the double GRefls. Why did awI get flattened?
It's not a disaster, but pretty heavy handed.Here a summary of `ddumptctrace` for this program (part of test T12427a)
```
data T where
T1 :: a > ((forall b. [b]>[b]) > Int) > T
h11 y = case y of T1 _ v > v
```
I see this sequence
```
{co_awA} {0}:: ((forall b. [b] > [b]) > Int)
~# p_awz[tau:1] (CNonCanonical)
==> Hetero equality gives rise to kind equality
inert: {co_awG} :: p_awz[tau:1] ~# ((forall b. [b] > [b]) > Int > (TYPE {co_awF})_N)
work item: {co_awF} :: 'GHC.Types.LiftedRep ~# p_awy[tau:1]
co_awA := Sym ({co_awG} ; Sym (GRefl nominal ((forall b.[b] > [b]) > Int)
(TYPE {co_awF})_N))
==> Swap awF, kick out awG
work item: {co_awG} :: p_awz[tau:1] ~# ((forall b. [b] > [b]) > Int > (TYPE {co_awF})_N)
inert (because p_awy is untouchable):
{co_awH} :: p_awy[tau:1] ~# 'GHC.Types.LiftedRep
co_awF := Sym co_awH
==> flatten awG (strange double GRefl)
inert: {co_awH} :: p_awy[tau:1] ~# 'GHC.Types.LiftedRep
inert: {co_awI} :: p_awz[tau:1] ~# ((forall b. [b] > [b]) > Int > (TYPE (Sym {co_awH}))_N)
co_awG := {co_awI} ; (Sym (GRefl nominal ((forall b. [b] > [b]) > Int)
(TYPE (Sym {co_awH}))_N)
; GRefl nominal ((forall b. [b] > [b]) > Int)
(TYPE {co_awF})_N)
at this point we also make a derived shadow of awI, for some reason.
Solving stops here, but we float out awI, and awH, and then have another go
work: {co_awH} :: p_awy[tau:1] ~# 'GHC.Types.LiftedRep
work: {co_awI} :: p_awz[tau:1] ~# ((forall b. [b] > [b]) > Int > (TYPE (Sym {co_awH}))_N)
==> flatten awI (why?)
work: {co_awH} :: p_awy[tau:1] ~# 'GHC.Types.LiftedRep
inert: {co_awJ} :: p_awz[tau:1] ~# ((forall b. [b] > [b]) > Int > (TYPE (Sym {co_awH}))_N)
co_awI := {co_awJ} ; (Sym (GRefl nominal ((forall b. [b] > [b]) > Int)
(TYPE (Sym {co_awH}))_N) ; GRefl nominal ((forall b. [b] > [b])
> Int)
(TYPE (Sym {co_awH}))_N)
==> solve awH: p_awy := LiftedRep, kick out awJ
{co_awJ} :: p_awz[tau:1] ~# ((forall b. [b] > [b]) > Int > (TYPE (Sym {co_awH}))_N)
==> flatten awJ
co_awJ := {co_awK} ; GRefl nominal ((forall b. [b] > [b]) > Int)
(TYPE (Sym {co_awH}))_N
{co_awK} :: p_awz[tau:1] ~# ((forall b. [b] > [b]) > Int)
```
This seems like we are doing too much work, esp the double GRefls. Why did awI get flattened?
It's not a disaster, but pretty heavy handed.Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/18412Monotype check for case branches should not recur through arrows20200720T07:57:36ZRichard Eisenbergrae@richarde.devMonotype check for case branches should not recur through arrowsConsider this module:
```hs
{# LANGUAGE RankNTypes #}
module Bug where
hr :: (forall a. a > a) > ()
hr _ = ()
foo x = case x of () > hr
bar x = case x of True > hr
False > hr
```
On HEAD, `foo` is accepted while `bar` is rejected. (This is not a change from previous behavior.) The reason is that GHC requires `case` branches (when there are more than 1; and when the result of the `case` is being inferred, not checked) to have monotypes, lest it be left with the task of finding the most general supertype of a bunch of polytypes. However, now that we have simplified subsumption, it is draconian to propagate the monotype check past arrows. I thus claim that `bar` should be accepted.Consider this module:
```hs
{# LANGUAGE RankNTypes #}
module Bug where
hr :: (forall a. a > a) > ()
hr _ = ()
foo x = case x of () > hr
bar x = case x of True > hr
False > hr
```
On HEAD, `foo` is accepted while `bar` is rejected. (This is not a change from previous behavior.) The reason is that GHC requires `case` branches (when there are more than 1; and when the result of the `case` is being inferred, not checked) to have monotypes, lest it be left with the task of finding the most general supertype of a bunch of polytypes. However, now that we have simplified subsumption, it is draconian to propagate the monotype check past arrows. I thus claim that `bar` should be accepted.https://gitlab.haskell.org/ghc/ghc//issues/18406Functional dependency should constrain local inferred type, but does not20200720T13:58:34ZRichard Eisenbergrae@richarde.devFunctional dependency should constrain local inferred type, but does notIf I compile
```hs
{# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #}
module Bug where
class C a b  a > b where
op :: a > a
foo :: C a b => a > b > a
foo x y = blah x
where
blah z = [x,z] `seq` op z
```
with `ddumptc fprinttypecheckerelaboration fprintexplicitforalls`, I get
```
==================== Typechecker ====================
AbsBinds [a_apDT, b_apDU] [$dC_apDW]
{Exports: [foo <= foo_apDV
wrap: <>]
Exported types: foo :: forall a b. C a b => a > b > a
[LclId]
Binds: foo_apDV x_apD6 y_apD7
= blah_apD8 @ b_apDU $dC_apEm x_apD6
where
AbsBinds [b_apE7] [$dC_apEd]
{Exports: [blah_apD8 <= blah_apEb
wrap: <>]
Exported types: blah_apD8
:: forall {b}. C a_apDT b => a_apDT > a_apDT
[LclId]
Binds: blah_apD8 z_apD9
= [x_apD6, z_apD9] `seq` op @ a_apDT @ b_apE7 $dC_apE8 z_apD9
Evidence: [EvBinds{[W] $dC_apE8 = $dC_apEd}]}
Evidence: [EvBinds{[W] $dC_apEm = $dC_apDW}]}
```
Note that the local `blah` gets type `forall {b}. C a b => a > a`. Why quantify `b` locally? There is no reason to. There is no great harm either, but a patch I'm working on (https://gitlab.haskell.org/ghc/ghc//tree/wip/derivedrefactor) gets annoyed when this condition (which happens in the wild, in `Text.Parsec.Perm`) causes `[G] C a b1` and `[G] C a b2` to both be in scope with no relationship between `b1` and `b2`.
Will fix in ongoing work.If I compile
```hs
{# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #}
module Bug where
class C a b  a > b where
op :: a > a
foo :: C a b => a > b > a
foo x y = blah x
where
blah z = [x,z] `seq` op z
```
with `ddumptc fprinttypecheckerelaboration fprintexplicitforalls`, I get
```
==================== Typechecker ====================
AbsBinds [a_apDT, b_apDU] [$dC_apDW]
{Exports: [foo <= foo_apDV
wrap: <>]
Exported types: foo :: forall a b. C a b => a > b > a
[LclId]
Binds: foo_apDV x_apD6 y_apD7
= blah_apD8 @ b_apDU $dC_apEm x_apD6
where
AbsBinds [b_apE7] [$dC_apEd]
{Exports: [blah_apD8 <= blah_apEb
wrap: <>]
Exported types: blah_apD8
:: forall {b}. C a_apDT b => a_apDT > a_apDT
[LclId]
Binds: blah_apD8 z_apD9
= [x_apD6, z_apD9] `seq` op @ a_apDT @ b_apE7 $dC_apE8 z_apD9
Evidence: [EvBinds{[W] $dC_apE8 = $dC_apEd}]}
Evidence: [EvBinds{[W] $dC_apEm = $dC_apDW}]}
```
Note that the local `blah` gets type `forall {b}. C a b => a > a`. Why quantify `b` locally? There is no reason to. There is no great harm either, but a patch I'm working on (https://gitlab.haskell.org/ghc/ghc//tree/wip/derivedrefactor) gets annoyed when this condition (which happens in the wild, in `Text.Parsec.Perm`) causes `[G] C a b1` and `[G] C a b2` to both be in scope with no relationship between `b1` and `b2`.
Will fix in ongoing work.https://gitlab.haskell.org/ghc/ghc//issues/18311Record update is overrestrictive20201005T09:00:11ZSimon Peyton JonesRecord update is overrestrictiveConsider
```
type family F a
type instance F Int = Int
type instance F Bool = Int
data T a = MkT { x :: F a, y :: a }
foo1 :: T Int > T Bool
foo1 (MkT { x = x }) = MkT { x = x, y = True}
foo2 :: T Int > T Bool
foo2 t = t { y = True }
```
`foo1` typechecks fine, but `foo2` complains
```
Foo.hs:16:10: error:
• Couldn't match type ‘Int’ with ‘Bool’
Expected type: T Bool
Actual type: T Int
• In the expression: t {y = True}
In an equation for ‘foo2’: foo2 t = t {y = True}
```
This is bogus. `foo2` should be fine  precisely because `foo1` is.
The offending code is in the `RecordUpd` case of `GHc.Tc.Gen.Expr.tcExpr`. See this comment
```
 STEP 4 Note [Type of a record update]
 Figure out types for the scrutinee and result
 Both are of form (T a b c), with fresh type variables, but with
 common variables where the scrutinee and result must have the same type
 These are variables that appear in *any* arg of *any* of the
 relevant constructors *except* in the updated fields
```
With the advent of type families "appearing in" a type is not the same as being fixed by it.
Not hard to fix; might even lead to less code!Consider
```
type family F a
type instance F Int = Int
type instance F Bool = Int
data T a = MkT { x :: F a, y :: a }
foo1 :: T Int > T Bool
foo1 (MkT { x = x }) = MkT { x = x, y = True}
foo2 :: T Int > T Bool
foo2 t = t { y = True }
```
`foo1` typechecks fine, but `foo2` complains
```
Foo.hs:16:10: error:
• Couldn't match type ‘Int’ with ‘Bool’
Expected type: T Bool
Actual type: T Int
• In the expression: t {y = True}
In an equation for ‘foo2’: foo2 t = t {y = True}
```
This is bogus. `foo2` should be fine  precisely because `foo1` is.
The offending code is in the `RecordUpd` case of `GHc.Tc.Gen.Expr.tcExpr`. See this comment
```
 STEP 4 Note [Type of a record update]
 Figure out types for the scrutinee and result
 Both are of form (T a b c), with fresh type variables, but with
 common variables where the scrutinee and result must have the same type
 These are variables that appear in *any* arg of *any* of the
 relevant constructors *except* in the updated fields
```
With the advent of type families "appearing in" a type is not the same as being fixed by it.
Not hard to fix; might even lead to less code!https://gitlab.haskell.org/ghc/ghc//issues/18308Order of StandaloneKindSignatures and CUSKs extensions significant20200626T16:28:20ZBjörn HegerforsOrder of StandaloneKindSignatures and CUSKs extensions significant## Summary
I have some code that compiles without the `StandaloneKindSignatures` extension, does not compile with it, but does compile again if I also add the `CUSKs` extension _after_ `StandaloneKindSignatures`. However, if I place the `CUSKs` extension _before_ `StandaloneKindSignatures`, then the code doesn't compile.
I'm not sure if I can avoid a CUSK in this case either, because it revolves around an associated type family, which to my understanding standalone kind signatures cannot (yet) be written for.
I generally try to keep my extensions arranged alphabetically, which is unfortunate in this case. But that's not at all a big worry. For now I can put `CUSKs` after `StandaloneKindSignatures` as a workaround.
## Steps to reproduce
Boiling it down to a minimal demonstrative case, this compiles:
```haskell
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE StandaloneKindSignatures #}
{# LANGUAGE CUSKs #}
import Data.Kind (Type)
import Data.Proxy (Proxy)
class Cls where
type Fam (k :: Type) (a :: k) :: Type
mtd :: Proxy k > Proxy (a :: k) > Fam k a > Int
```
but this doesn't:
```haskell
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE CUSKs #}
{# LANGUAGE StandaloneKindSignatures #}
import Data.Kind (Type)
import Data.Proxy (Proxy)
class Cls where
type Fam (k :: Type) (a :: k) :: Type
mtd :: Proxy k > Proxy (a :: k) > Fam k a > Int
```
## Expected behavior
I would expect both of the above to compile.
I should also note that it's not very clear to me what it is about the type signature for `mtd` that makes it problematic. The part that is sensitive here is the `(a :: k)` kind annotation. Whether I instead put that annotation in a `forall` makes no difference. If I simply remove the kind annotation for `a`, and let it be inferred, the code compiles regardless of which of `StandaloneKindSignatures` and `CUSKs` are enabled (and in which order). I don't know if this part behaves as expected or not.
## Environment
* GHC version used: 8.10.1## Summary
I have some code that compiles without the `StandaloneKindSignatures` extension, does not compile with it, but does compile again if I also add the `CUSKs` extension _after_ `StandaloneKindSignatures`. However, if I place the `CUSKs` extension _before_ `StandaloneKindSignatures`, then the code doesn't compile.
I'm not sure if I can avoid a CUSK in this case either, because it revolves around an associated type family, which to my understanding standalone kind signatures cannot (yet) be written for.
I generally try to keep my extensions arranged alphabetically, which is unfortunate in this case. But that's not at all a big worry. For now I can put `CUSKs` after `StandaloneKindSignatures` as a workaround.
## Steps to reproduce
Boiling it down to a minimal demonstrative case, this compiles:
```haskell
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE StandaloneKindSignatures #}
{# LANGUAGE CUSKs #}
import Data.Kind (Type)
import Data.Proxy (Proxy)
class Cls where
type Fam (k :: Type) (a :: k) :: Type
mtd :: Proxy k > Proxy (a :: k) > Fam k a > Int
```
but this doesn't:
```haskell
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE CUSKs #}
{# LANGUAGE StandaloneKindSignatures #}
import Data.Kind (Type)
import Data.Proxy (Proxy)
class Cls where
type Fam (k :: Type) (a :: k) :: Type
mtd :: Proxy k > Proxy (a :: k) > Fam k a > Int
```
## Expected behavior
I would expect both of the above to compile.
I should also note that it's not very clear to me what it is about the type signature for `mtd` that makes it problematic. The part that is sensitive here is the `(a :: k)` kind annotation. Whether I instead put that annotation in a `forall` makes no difference. If I simply remove the kind annotation for `a`, and let it be inferred, the code compiles regardless of which of `StandaloneKindSignatures` and `CUSKs` are enabled (and in which order). I don't know if this part behaves as expected or not.
## Environment
* GHC version used: 8.10.1https://gitlab.haskell.org/ghc/ghc//issues/18300UnliftedNewtypesDifficultUnification broken due to simplified subsumption20200703T21:33:23ZBen GamariUnliftedNewtypesDifficultUnification broken due to simplified subsumption`UnliftedNewtypesDifficultUnification` fails due to simplified subsumption patch (!2600) in `DEBUG`enabled compiler.
```
Compile failed (exit code 1) errors were:
ghcstage2: panic! (the 'impossible' happened)
(GHC version 8.11.0.20200603:
ASSERT failed! file compiler/GHC/Core/FamInstEnv.hs, line 651
Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug
*** unexpected failure for UnliftedNewtypesDifficultUnification(normal)
```
I have marked this test as broken in the interest of getting !2600 merged.
As seen in Job [#356282](https://gitlab.haskell.org/ghc/ghc//jobs/356282).`UnliftedNewtypesDifficultUnification` fails due to simplified subsumption patch (!2600) in `DEBUG`enabled compiler.
```
Compile failed (exit code 1) errors were:
ghcstage2: panic! (the 'impossible' happened)
(GHC version 8.11.0.20200603:
ASSERT failed! file compiler/GHC/Core/FamInstEnv.hs, line 651
Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug
*** unexpected failure for UnliftedNewtypesDifficultUnification(normal)
```
I have marked this test as broken in the interest of getting !2600 merged.
As seen in Job [#356282](https://gitlab.haskell.org/ghc/ghc//jobs/356282).9.0.1Simon Peyton JonesSimon Peyton Joneshttps://gitlab.haskell.org/ghc/ghc//issues/18295Outdated commentary in solveNestedImplications?20200604T15:36:21ZRichard Eisenbergrae@richarde.devOutdated commentary in solveNestedImplications?`GHC.Tc.Solver.solveNestedImplications` looks like this:
```hs
solveNestedImplications :: Bag Implication
> TcS (Cts, Bag Implication)
 Precondition: the TcS inerts may contain unsolved simples which have
 to be converted to givens before we go inside a nested implication.
solveNestedImplications implics
 isEmptyBag implics
= return (emptyBag, emptyBag)
 otherwise
= do { traceTcS "solveNestedImplications starting {" empty
; (floated_eqs_s, unsolved_implics) < mapAndUnzipBagM solveImplication implics
; let floated_eqs = concatBag floated_eqs_s
 ... and we are back in the original TcS inerts
 Notice that the original includes the _insoluble_simples so it was safe to ignore
 them in the beginning of this function.
; traceTcS "solveNestedImplications end }" $
vcat [ text "all floated_eqs =" <+> ppr floated_eqs
, text "unsolved_implics =" <+> ppr unsolved_implics ]
; return (floated_eqs, catBagMaybes unsolved_implics) }
```
I believe that both the `Precondition:` and the `... and we are back` comments are out of date. If they are not, they should be clarified, as I have no idea what they mean.
Also:
```hs
solveImplication :: Implication  Wanted
> TcS (Cts,  All wanted or derived floated equalities: var = type
Maybe Implication)  Simplified implication (empty or singleton)
 Precondition: The TcS monad contains an empty worklist and givenonly inerts
 which after trying to solve this implication we must restore to their original value
```
The emptyworklist precondition seems reasonable, but the "givenonly inerts" bit is as mysterious as (and sounds quite related to) the previous problem.
@simonpj help?`GHC.Tc.Solver.solveNestedImplications` looks like this:
```hs
solveNestedImplications :: Bag Implication
> TcS (Cts, Bag Implication)
 Precondition: the TcS inerts may contain unsolved simples which have
 to be converted to givens before we go inside a nested implication.
solveNestedImplications implics
 isEmptyBag implics
= return (emptyBag, emptyBag)
 otherwise
= do { traceTcS "solveNestedImplications starting {" empty
; (floated_eqs_s, unsolved_implics) < mapAndUnzipBagM solveImplication implics
; let floated_eqs = concatBag floated_eqs_s
 ... and we are back in the original TcS inerts
 Notice that the original includes the _insoluble_simples so it was safe to ignore
 them in the beginning of this function.
; traceTcS "solveNestedImplications end }" $
vcat [ text "all floated_eqs =" <+> ppr floated_eqs
, text "unsolved_implics =" <+> ppr unsolved_implics ]
; return (floated_eqs, catBagMaybes unsolved_implics) }
```
I believe that both the `Precondition:` and the `... and we are back` comments are out of date. If they are not, they should be clarified, as I have no idea what they mean.
Also:
```hs
solveImplication :: Implication  Wanted
> TcS (Cts,  All wanted or derived floated equalities: var = type
Maybe Implication)  Simplified implication (empty or singleton)
 Precondition: The TcS monad contains an empty worklist and givenonly inerts
 which after trying to solve this implication we must restore to their original value
```
The emptyworklist precondition seems reasonable, but the "givenonly inerts" bit is as mysterious as (and sounds quite related to) the previous problem.
@simonpj help?https://gitlab.haskell.org/ghc/ghc//issues/18220Improve Coercible under foralls20200522T23:36:26ZSimon Peyton JonesImprove Coercible under forallsConsider
```
newtype Age = MkAge Int
h :: forall m. m Int > m Age
h x = coerce @(m Int) @(m Age) x
```
This fails, as it should, with
```
Couldn't match representation of type 'm Int'
with that of 'm Age'
arising from a use of 'coerce'
NB: We cannot know what roles the parameters to 'm' have;
we must assume that the role is nominal
```
And indeed, if we have
```
type family F a
data T a = MkT (F a)
```
Then `h @T` would indeed be bogus because `T Int` and `T Age` might have very different representations.
So far so good. Now consider
```
f :: forall m. (forall p q. Coercible p q => Coercible (m p) (m q))
=> m Int > m Age
f x = coerce @(m Int) @(m Age) x
g :: forall m. (forall p q. Coercible p q => Coercible (m p) (m q))
=> (forall a. a > m Int) > (forall a. a> m Age)
g x = coerce @(forall a. a > m Int) @(forall a. a > m Age) x
```
Here `f` succeeds. It needs `[W] Coercible (m Int) (m Age)` which it can prove from the quantified constraint.
But `g` is rejected with
```
Couldn't match representation of type 'm Int'
with that of 'm Age'
arising from a use of 'coerce'
NB: We cannot know what roles the parameters to 'm' have;
we must assume that the role is nominal
In the expression:
coerce @(forall a. a > m Int) @(forall a. a > m Age) x
```
That's odd! I can easily come up with a succesful elaboration of the program. Why? We start from
```
[W] Coercible (forall a. a > m Int) (forall a. a > m Age)
===>
[W] (forall a. a > m Int) ~R# (forall a. a > m Age)
===> {make an implication constraint}
[W] forall <noev> a. () => (a > m Int) ~R# (a > m Age)
```
The `<noev>` says that we don't have a place to put valuelevel evidence. Then we decompose:
```
===>
[W] forall <noev> a. () => (m Int) ~R# (m Age)
```
and now we are stuck because there is nowhere to put the evidence.
But the solution is simple! Just float the constraint out of the implication (it does not mention the skolem `a`). I have done this in !3319, and indeed it works.
However, it doesn't solve the full problem. What we wanted `m a Int ~R# m a Age`? Now the skolem `a` would prevent the constraint floating out, and we are back to square 1

That termlevel quantified constraint `(forall p q. Coercible p q => Coercible (m p) (m q))` is really a way of saying "m's first argument has representational role". Perhaps we should seek a way of saying that more directly, and in a way we can use in coercions. Something like `Rep# m`. Then the evidence for `Rep# m` justifies decomposing a wanted constraint `m t1 ~R# m t2`.
Another alternative would be to decorate the arrow in m's kind, as we proposed in the first roles paper.
Neither seems simple. So this ticket is just recording the issue, and pointing to the MR, for posterity.

All this arose in #18148 and #18213, but is only tangentially related in the end.Consider
```
newtype Age = MkAge Int
h :: forall m. m Int > m Age
h x = coerce @(m Int) @(m Age) x
```
This fails, as it should, with
```
Couldn't match representation of type 'm Int'
with that of 'm Age'
arising from a use of 'coerce'
NB: We cannot know what roles the parameters to 'm' have;
we must assume that the role is nominal
```
And indeed, if we have
```
type family F a
data T a = MkT (F a)
```
Then `h @T` would indeed be bogus because `T Int` and `T Age` might have very different representations.
So far so good. Now consider
```
f :: forall m. (forall p q. Coercible p q => Coercible (m p) (m q))
=> m Int > m Age
f x = coerce @(m Int) @(m Age) x
g :: forall m. (forall p q. Coercible p q => Coercible (m p) (m q))
=> (forall a. a > m Int) > (forall a. a> m Age)
g x = coerce @(forall a. a > m Int) @(forall a. a > m Age) x
```
Here `f` succeeds. It needs `[W] Coercible (m Int) (m Age)` which it can prove from the quantified constraint.
But `g` is rejected with
```
Couldn't match representation of type 'm Int'
with that of 'm Age'
arising from a use of 'coerce'
NB: We cannot know what roles the parameters to 'm' have;
we must assume that the role is nominal
In the expression:
coerce @(forall a. a > m Int) @(forall a. a > m Age) x
```
That's odd! I can easily come up with a succesful elaboration of the program. Why? We start from
```
[W] Coercible (forall a. a > m Int) (forall a. a > m Age)
===>
[W] (forall a. a > m Int) ~R# (forall a. a > m Age)
===> {make an implication constraint}
[W] forall <noev> a. () => (a > m Int) ~R# (a > m Age)
```
The `<noev>` says that we don't have a place to put valuelevel evidence. Then we decompose:
```
===>
[W] forall <noev> a. () => (m Int) ~R# (m Age)
```
and now we are stuck because there is nowhere to put the evidence.
But the solution is simple! Just float the constraint out of the implication (it does not mention the skolem `a`). I have done this in !3319, and indeed it works.
However, it doesn't solve the full problem. What we wanted `m a Int ~R# m a Age`? Now the skolem `a` would prevent the constraint floating out, and we are back to square 1

That termlevel quantified constraint `(forall p q. Coercible p q => Coercible (m p) (m q))` is really a way of saying "m's first argument has representational role". Perhaps we should seek a way of saying that more directly, and in a way we can use in coercions. Something like `Rep# m`. Then the evidence for `Rep# m` justifies decomposing a wanted constraint `m t1 ~R# m t2`.
Another alternative would be to decorate the arrow in m's kind, as we proposed in the first roles paper.
Neither seems simple. So this ticket is just recording the issue, and pointing to the MR, for posterity.

All this arose in #18148 and #18213, but is only tangentially related in the end.https://gitlab.haskell.org/ghc/ghc//issues/18196Type synonym lost with GADTs20200518T18:35:05ZIdentical SnowflakeType synonym lost with GADTsConsider the following:
```haskell
type Joules = Double
type Grams = Double
data Unit a where
Energy :: Unit Joules
Mass :: Unit Grams
test :: Unit a > a
test Energy = _
```
GHC reports the hole as `_ :: Double`, but I expected the synonym to remain intact, i.e., that the hole would be `_ :: Joules`.Consider the following:
```haskell
type Joules = Double
type Grams = Double
data Unit a where
Energy :: Unit Joules
Mass :: Unit Grams
test :: Unit a > a
test Energy = _
```
GHC reports the hole as `_ :: Double`, but I expected the synonym to remain intact, i.e., that the hole would be `_ :: Joules`.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/18073Outofdate commentary in Tc.Deriv.Infer20200423T03:49:06ZRichard Eisenbergrae@richarde.devOutofdate commentary in Tc.Deriv.InferCheck out https://gitlab.haskell.org/ghc/ghc//blob/15ab6cd548f284732a7f89d78c2b89b1bfc4ea1d/compiler/GHC/Tc/Deriv/Infer.hs#L805
* The commentary there talks about creating a variable `unsolved`, which does not seem to exist.
* In addition, the partition below creates `bad`, which is just ignored. Maybe this is right  I have not thought about it. But if it is right, it should be documented.
cc @RyanGlScottCheck out https://gitlab.haskell.org/ghc/ghc//blob/15ab6cd548f284732a7f89d78c2b89b1bfc4ea1d/compiler/GHC/Tc/Deriv/Infer.hs#L805
* The commentary there talks about creating a variable `unsolved`, which does not seem to exist.
* In addition, the partition below creates `bad`, which is just ignored. Maybe this is right  I have not thought about it. But if it is right, it should be documented.
cc @RyanGlScott