GHC issueshttps://gitlab.haskell.org/ghc/ghc//issues20201029T19:00:42Zhttps://gitlab.haskell.org/ghc/ghc//issues/18850Instance/given overlap trips up the ambiguity check20201029T19:00:42ZRichard Eisenbergrae@richarde.devInstance/given overlap trips up the ambiguity checkThursday is a good day to abuse GHC. So I said this:
```hs
{# LANGUAGE TypeFamilies, FlexibleInstances #}
module Bug where
class IsBool bool
instance bool ~ Bool => IsBool bool
class C a
instance C Bool
f :: (C bool, IsBool bool) => ()
f = ()
```
To me, `f`'s type is unambiguous: the `IsBool bool` constraint fixes the type variable `bool` to be `Bool`. But GHC says
```
/Users/rae/temp/Bug2.hs:11:6: error:
• Could not deduce (C bool0)
from the context: (C bool, IsBool bool)
bound by the type signature for:
f :: forall bool. (C bool, IsBool bool) => ()
at /Users/rae/temp/Bug2.hs:11:632
The type variable ‘bool0’ is ambiguous
• In the ambiguity check for ‘f’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature: f :: (C bool, IsBool bool) => ()

11  f :: (C bool, IsBool bool) => ()
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
But maybe I'm wrong. Is the type really ambiguous? No. When I say
```hs
{# LANGUAGE TypeFamilies, FlexibleInstances, AllowAmbiguousTypes #}
module Bug where
class IsBool bool
instance bool ~ Bool => IsBool bool
class C a
instance C Bool
f :: (C bool, IsBool bool) => ()
f = ()
g = f
```
my program is accepted. I've added `AllowAmbiguousTypes` and the binding `g = f`. That binding is accepted  no type applications or other funny business. This suggests that `f`'s type is not actually ambiguous.
What's going on is an overeager instance/given overlap; see `Note [Instance and Given overlap]` in `GHC.Tc.Solver.Interact`. That Note ends with
```
All of this is disgustingly delicate, so to discourage people from writing
simplifiable class givens, we warn about signatures that contain them;
see GHC.Tc.Validity Note [Simplifiable given constraints].
```
But I don't get the warning! Even in my second program, which is errorfree. Hunting further into `GHC.Tc.Validity`, I find this code:
```hs
checkSimplifiableClassConstraint env dflags ctxt cls tys
 not (wopt Opt_WarnSimplifiableClassConstraints dflags)
= return ()
 xopt LangExt.MonoLocalBinds dflags
= return ()
 ...
```
where the `...` includes generating a warning. Of course, I *do* have `XMonoLocalBinds`, as implied by `XTypeFamilies`. What happens when I disable this (with an explicit `XNoMonoLocalBinds`)?
```
/Users/rae/temp/Bug2.hs:11:6: warning: [Wsimplifiableclassconstraints]
• The constraint ‘IsBool bool’ matches
instance (bool ~ Bool) => IsBool bool
 Defined at /Users/rae/temp/Bug2.hs:6:10
This makes type inference for inner bindings fragile;
either use MonoLocalBinds, or simplify it using the instance
• In the type signature: f :: (C bool, IsBool bool) => ()

11  f :: (C bool, IsBool bool) => ()
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
Good. The warning fires.
My conclusions:
1. My first program really ought to be accepted. The type is not ambiguous. I'm willing to concede this point to "disgustingly delicate", though, if we don't see an easy way to fix.
2. It looks the warning should fire even when `XMonoLocalBinds` is in effect. My program has no local generalization involved. How would users disable the warnings? By not writing a simplifiable Given.Thursday is a good day to abuse GHC. So I said this:
```hs
{# LANGUAGE TypeFamilies, FlexibleInstances #}
module Bug where
class IsBool bool
instance bool ~ Bool => IsBool bool
class C a
instance C Bool
f :: (C bool, IsBool bool) => ()
f = ()
```
To me, `f`'s type is unambiguous: the `IsBool bool` constraint fixes the type variable `bool` to be `Bool`. But GHC says
```
/Users/rae/temp/Bug2.hs:11:6: error:
• Could not deduce (C bool0)
from the context: (C bool, IsBool bool)
bound by the type signature for:
f :: forall bool. (C bool, IsBool bool) => ()
at /Users/rae/temp/Bug2.hs:11:632
The type variable ‘bool0’ is ambiguous
• In the ambiguity check for ‘f’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature: f :: (C bool, IsBool bool) => ()

11  f :: (C bool, IsBool bool) => ()
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
But maybe I'm wrong. Is the type really ambiguous? No. When I say
```hs
{# LANGUAGE TypeFamilies, FlexibleInstances, AllowAmbiguousTypes #}
module Bug where
class IsBool bool
instance bool ~ Bool => IsBool bool
class C a
instance C Bool
f :: (C bool, IsBool bool) => ()
f = ()
g = f
```
my program is accepted. I've added `AllowAmbiguousTypes` and the binding `g = f`. That binding is accepted  no type applications or other funny business. This suggests that `f`'s type is not actually ambiguous.
What's going on is an overeager instance/given overlap; see `Note [Instance and Given overlap]` in `GHC.Tc.Solver.Interact`. That Note ends with
```
All of this is disgustingly delicate, so to discourage people from writing
simplifiable class givens, we warn about signatures that contain them;
see GHC.Tc.Validity Note [Simplifiable given constraints].
```
But I don't get the warning! Even in my second program, which is errorfree. Hunting further into `GHC.Tc.Validity`, I find this code:
```hs
checkSimplifiableClassConstraint env dflags ctxt cls tys
 not (wopt Opt_WarnSimplifiableClassConstraints dflags)
= return ()
 xopt LangExt.MonoLocalBinds dflags
= return ()
 ...
```
where the `...` includes generating a warning. Of course, I *do* have `XMonoLocalBinds`, as implied by `XTypeFamilies`. What happens when I disable this (with an explicit `XNoMonoLocalBinds`)?
```
/Users/rae/temp/Bug2.hs:11:6: warning: [Wsimplifiableclassconstraints]
• The constraint ‘IsBool bool’ matches
instance (bool ~ Bool) => IsBool bool
 Defined at /Users/rae/temp/Bug2.hs:6:10
This makes type inference for inner bindings fragile;
either use MonoLocalBinds, or simplify it using the instance
• In the type signature: f :: (C bool, IsBool bool) => ()

11  f :: (C bool, IsBool bool) => ()
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
Good. The warning fires.
My conclusions:
1. My first program really ought to be accepted. The type is not ambiguous. I'm willing to concede this point to "disgustingly delicate", though, if we don't see an easy way to fix.
2. It looks the warning should fire even when `XMonoLocalBinds` is in effect. My program has no local generalization involved. How would users disable the warnings? By not writing a simplifiable Given.https://gitlab.haskell.org/ghc/ghc//issues/18802Typecheck record update via desugaring20201005T20:51:46ZSimon Peyton JonesTypecheck record update via desugaringThere are quite a few tickets relating to inadequacies of record update, including
* #18311
* #10856
* #2595
* #10808
* #3632: updating existentials if you do all of them at once
* #16501
Record update is a place where our general plan of typechecking the source syntax seems particularly hard to do. It wold be much easier (and correct by construction) to desugar (but still in HsSyn) and typecheck that.
Fortunately we now have a way to do that: our [Reengineer rebindable syntax](https://gitlab.haskell.org/ghc/ghc//issues/17582) ticket, #17582. A lot of attention is paid there to maintaining good error messages, which is the main challenge of this approach.
So this ticket is to propose: let's use the work on #17582 to solve our recordupdate tickets.There are quite a few tickets relating to inadequacies of record update, including
* #18311
* #10856
* #2595
* #10808
* #3632: updating existentials if you do all of them at once
* #16501
Record update is a place where our general plan of typechecking the source syntax seems particularly hard to do. It wold be much easier (and correct by construction) to desugar (but still in HsSyn) and typecheck that.
Fortunately we now have a way to do that: our [Reengineer rebindable syntax](https://gitlab.haskell.org/ghc/ghc//issues/17582) ticket, #17582. A lot of attention is paid there to maintaining good error messages, which is the main challenge of this approach.
So this ticket is to propose: let's use the work on #17582 to solve our recordupdate tickets.https://gitlab.haskell.org/ghc/ghc//issues/18739Infer multiplicity of let expression20200928T12:06:59ZArnaud SpiwackInfer multiplicity of let expression## Motivation
In a let expression `let x = rhs in u`, `x` is always bound with multiplicity `Many` (and, correspondingly, `u` is consumed with multiplicity `Many`).
This also holds of where expression `u where x = rhs`.
The situation is similar to that of case expression as in #18738 .
In #18461 , we are adding a syntax to force polymorphism, but programmers expect let expressions to know their multiplicity on their own (in particular, they expect `let x = y in u` to be the same as `u[x\y]`, but if the latter consumes `y` linearly, the former never does in the current GHC).
## Proposal
Infer the multiplicity of `let` binders instead of choosing `Many` systematically. The multiplicity would be a variable.
A small detail to pay attention to is that, in `let pat = rhs in u`, the outermost pattern of `pat` is lazy. Lazy pattern are only permissible in unrestricted patterns (one way to think about it is that the desugaring of lazy pattern is not linear).
The typechecker doesn't make this property very apparent, so we will have to be careful about it. I suppose the same issue arises in #18461 .## Motivation
In a let expression `let x = rhs in u`, `x` is always bound with multiplicity `Many` (and, correspondingly, `u` is consumed with multiplicity `Many`).
This also holds of where expression `u where x = rhs`.
The situation is similar to that of case expression as in #18738 .
In #18461 , we are adding a syntax to force polymorphism, but programmers expect let expressions to know their multiplicity on their own (in particular, they expect `let x = y in u` to be the same as `u[x\y]`, but if the latter consumes `y` linearly, the former never does in the current GHC).
## Proposal
Infer the multiplicity of `let` binders instead of choosing `Many` systematically. The multiplicity would be a variable.
A small detail to pay attention to is that, in `let pat = rhs in u`, the outermost pattern of `pat` is lazy. Lazy pattern are only permissible in unrestricted patterns (one way to think about it is that the desugaring of lazy pattern is not linear).
The typechecker doesn't make this property very apparent, so we will have to be careful about it. I suppose the same issue arises in #18461 .https://gitlab.haskell.org/ghc/ghc//issues/18738Infer multiplicity of case expression20210301T22:31:04ZArnaud SpiwackInfer multiplicity of case expression## Motivation
As it stands, the following expression
```haskell
case u of {…}
```
is always understood by the typechecker as consuming `u` with multiplicity `Many`. This was done in the first iteration of patch in order to ensure being fully compatible with regular Haskell without having to delve too much into inference issue.
This applies to case expressions and to pattern guards creating a pattern:
```haskell
 pat < u, … = …
```
here u is also consumed with multiplicity `Many`.
(In a `\case` or a function definition by equations, the multiplicity is decided by the type that it is checked against, if any. So it may be any multiplicity.)
Core is already equipped to deal with arbitrary multiplicities here.
## Proposal
These expressions should infer the appropriate multiplicity. So typechecking such a case expression should emit a multiplicity variable instead of choosing `Many` systematically.
One somewhat subtle point to keep in mind is that some patterns require that the scrutinee be consumed unrestrictedly. That's the case, for instance, of wildcard patterns (`_`). I believe that the current implementation will handle a variable for the pattern's multiplicity smoothly (see `checkManyPattern` in `GHC.Tc.Gen.Pat` ([currently](https://gitlab.haskell.org/ghc/ghc//blob/d7385f7077c6258c2a76ae51b4ea80f6fa9c7015/compiler/GHC/Tc/Gen/Pat.hs#L348349)). But it's worth doublechecking.
For pattern guard the relevant code is the `BindStmt` case of `tcGuardStmt` in `GHC.Tc.Gen.Match`.
cc @monoidal## Motivation
As it stands, the following expression
```haskell
case u of {…}
```
is always understood by the typechecker as consuming `u` with multiplicity `Many`. This was done in the first iteration of patch in order to ensure being fully compatible with regular Haskell without having to delve too much into inference issue.
This applies to case expressions and to pattern guards creating a pattern:
```haskell
 pat < u, … = …
```
here u is also consumed with multiplicity `Many`.
(In a `\case` or a function definition by equations, the multiplicity is decided by the type that it is checked against, if any. So it may be any multiplicity.)
Core is already equipped to deal with arbitrary multiplicities here.
## Proposal
These expressions should infer the appropriate multiplicity. So typechecking such a case expression should emit a multiplicity variable instead of choosing `Many` systematically.
One somewhat subtle point to keep in mind is that some patterns require that the scrutinee be consumed unrestrictedly. That's the case, for instance, of wildcard patterns (`_`). I believe that the current implementation will handle a variable for the pattern's multiplicity smoothly (see `checkManyPattern` in `GHC.Tc.Gen.Pat` ([currently](https://gitlab.haskell.org/ghc/ghc//blob/d7385f7077c6258c2a76ae51b4ea80f6fa9c7015/compiler/GHC/Tc/Gen/Pat.hs#L348349)). But it's worth doublechecking.
For pattern guard the relevant code is the `BindStmt` case of `tcGuardStmt` in `GHC.Tc.Gen.Match`.
cc @monoidalhttps://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/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/18413Suboptimal constraint solving20210329T08:49:08ZSimon 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/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 significant20210331T15:14:45ZBjö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/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/18062A cast might get in the way of instantiation20200427T10:20:56ZSimon Peyton JonesA cast might get in the way of instantiationSuppose we have a type signature `f :: forall a. Eq a => blah`, and it somehow kindchecks to
```
forall a. ((Eq a => Blah) > co)
```
In principle this can happen:
```
tc_hs_type mode (HsQualTy { hst_ctxt = ctxt, hst_body = rn_ty }) exp_kind
= do { ctxt' < tc_hs_context mode ctxt
; ek < newOpenTypeKind  The body kind (result of the function) can
 be TYPE r, for any r, hence newOpenTypeKind
; ty' < tc_lhs_type mode rn_ty ek
; checkExpectedKind (unLoc rn_ty) (mkPhiTy ctxt' ty')
liftedTypeKind exp_kind }
```
That `checkExpectedKind` can add a cast.
If this happens, our instantiation mechanisms would fall over in a heap. We'd instantiate the `forall a`, but then fail to instantiate the `Eq a =>`; instead we'd unify `(Eq a => blah) > co` with the function body. Bad, bad.
This popped up when fixing #18008, when a missing zonk in `tcHsPartialSigType` was producing just such a forall (with a Refl coercion). But it seems plausible that it could happen for real.
EDIT: And it does:
```hs
{# LANGUAGE KindSignatures, TypeFamilies, DataKinds #}
module Bug where
import Data.Kind ( Type )
type family Star where
Star = Type
f :: ((Eq a => a > Bool) :: Star)
f x = x == x
```
produces
```
Bug.hs:11:1: error:
• Couldn't match kind ‘Constraint’ with ‘*’
When matching types
a0 :: *
Eq a :: Constraint
Expected type: Eq a => a > Bool
Actual type: a0 > Bool
• The equation(s) for ‘f’ have one argument,
but its type ‘Eq a => a > Bool’ has none
• Relevant bindings include
f :: Eq a => a > Bool (bound at Bug.hs:11:1)

11  f x = x == x
 ^^^^^^^^^^^^
```
Solution: teach instantiation to look through casts.Suppose we have a type signature `f :: forall a. Eq a => blah`, and it somehow kindchecks to
```
forall a. ((Eq a => Blah) > co)
```
In principle this can happen:
```
tc_hs_type mode (HsQualTy { hst_ctxt = ctxt, hst_body = rn_ty }) exp_kind
= do { ctxt' < tc_hs_context mode ctxt
; ek < newOpenTypeKind  The body kind (result of the function) can
 be TYPE r, for any r, hence newOpenTypeKind
; ty' < tc_lhs_type mode rn_ty ek
; checkExpectedKind (unLoc rn_ty) (mkPhiTy ctxt' ty')
liftedTypeKind exp_kind }
```
That `checkExpectedKind` can add a cast.
If this happens, our instantiation mechanisms would fall over in a heap. We'd instantiate the `forall a`, but then fail to instantiate the `Eq a =>`; instead we'd unify `(Eq a => blah) > co` with the function body. Bad, bad.
This popped up when fixing #18008, when a missing zonk in `tcHsPartialSigType` was producing just such a forall (with a Refl coercion). But it seems plausible that it could happen for real.
EDIT: And it does:
```hs
{# LANGUAGE KindSignatures, TypeFamilies, DataKinds #}
module Bug where
import Data.Kind ( Type )
type family Star where
Star = Type
f :: ((Eq a => a > Bool) :: Star)
f x = x == x
```
produces
```
Bug.hs:11:1: error:
• Couldn't match kind ‘Constraint’ with ‘*’
When matching types
a0 :: *
Eq a :: Constraint
Expected type: Eq a => a > Bool
Actual type: a0 > Bool
• The equation(s) for ‘f’ have one argument,
but its type ‘Eq a => a > Bool’ has none
• Relevant bindings include
f :: Eq a => a > Bool (bound at Bug.hs:11:1)

11  f x = x == x
 ^^^^^^^^^^^^
```
Solution: teach instantiation to look through casts.https://gitlab.haskell.org/ghc/ghc//issues/18007GHCi infers toogeneral type when patternmatching on existential GADT20200408T23:12:25Zinfinity0GHCi infers toogeneral type when patternmatching on existential GADTRun the following in ghci, I tested with version 8.8.3:
<summary>
`ghci ghciscript Test.hs`
<details>
```haskell
:set XGADTs
:set XScopedTypeVariables
 standard GADT with restricted type param
data X a where X :: X Int; XB :: X Bool
 =============================================================================
 standard ADT with full type params
data Pair0 a b t = Pair0 (a t) (b t)
Pair0 X x < pure (Pair0 X [])
:t x
 x :: [Int] as expected
x /= [10]
 True
 as expected, type inference matches x with [10]
 =============================================================================
 existential ADT, same as DSum from Data.Dependent.Sum
data Pair a b = forall t. Pair (a t) (b t)
 same results with this equivalent GADTsyntax definition:
 data Pair a b where Pair :: a t > b t > Pair a b
Pair X x < pure (Pair X [])
x /= [10]
 somehow, type inference fails to match x with [10]
 • Couldn't match expected type ‘x’ with actual type ‘Integer’
:t x
 x :: [t] but it should be
 x :: [Int] because of the Pair X

Pair X (x :: [Int]) < pure (Pair X [])
x /= [10]
 True
 giving an explicit type signature fixes inference

Pair X x < pure (Pair X [0])
x /= [10]
 True
 giving an explicit value [0] also fixes inference

:{
test :: IO ()
test = do
Pair X x < pure (Pair X [])
print (x /= [10])
:}
test
 True
 putting the code inside a function, also fixes inference??
:{
test1 :: IO (Pair X [])
test1 = pure (Pair X [])
test2 :: Pair X [] > IO ()
test2 (Pair X x) = print (x /= [10])
:}
test1 >>= test2
 True
 separating the functions also works, and we never hint x's type
```
</details>
</summary>
I think this is different from #2206 and #14065 since the error message here is a pretty generic "Couldn't match type" rather than the GADTspecific error messages in those tickets ("GADT pattern match with nonrigid result type", "untouchable inside the constraints"), and it only affects GHCi.
Run the following in ghci, I tested with version 8.8.3:
<summary>
`ghci ghciscript Test.hs`
<details>
```haskell
:set XGADTs
:set XScopedTypeVariables
 standard GADT with restricted type param
data X a where X :: X Int; XB :: X Bool
 =============================================================================
 standard ADT with full type params
data Pair0 a b t = Pair0 (a t) (b t)
Pair0 X x < pure (Pair0 X [])
:t x
 x :: [Int] as expected
x /= [10]
 True
 as expected, type inference matches x with [10]
 =============================================================================
 existential ADT, same as DSum from Data.Dependent.Sum
data Pair a b = forall t. Pair (a t) (b t)
 same results with this equivalent GADTsyntax definition:
 data Pair a b where Pair :: a t > b t > Pair a b
Pair X x < pure (Pair X [])
x /= [10]
 somehow, type inference fails to match x with [10]
 • Couldn't match expected type ‘x’ with actual type ‘Integer’
:t x
 x :: [t] but it should be
 x :: [Int] because of the Pair X

Pair X (x :: [Int]) < pure (Pair X [])
x /= [10]
 True
 giving an explicit type signature fixes inference

Pair X x < pure (Pair X [0])
x /= [10]
 True
 giving an explicit value [0] also fixes inference

:{
test :: IO ()
test = do
Pair X x < pure (Pair X [])
print (x /= [10])
:}
test
 True
 putting the code inside a function, also fixes inference??
:{
test1 :: IO (Pair X [])
test1 = pure (Pair X [])
test2 :: Pair X [] > IO ()
test2 (Pair X x) = print (x /= [10])
:}
test1 >>= test2
 True
 separating the functions also works, and we never hint x's type
```
</details>
</summary>
I think this is different from #2206 and #14065 since the error message here is a pretty generic "Couldn't match type" rather than the GADTspecific error messages in those tickets ("GADT pattern match with nonrigid result type", "untouchable inside the constraints"), and it only affects GHCi.
https://gitlab.haskell.org/ghc/ghc//issues/17934Consider using specificity to disambiguate quantified constraints20210221T15:37:18ZRichard Eisenbergrae@richarde.devConsider using specificity to disambiguate quantified constraints**Summary:** Currently, quantified constraints shadow global instances. This ticket proposes to use specificity (in the sense used by overlapping instances) instead of shadowing.
**Motivation**
This looks like a sensible way of having a datatype that can store something of a type that supports some class interface:
```haskell
data Some (c :: Type > Constraint) where
Some :: c a => a > Some c
```
But now I want to write a `Show` instance. I can do this only when the existential `a` supports `Show`. But I don't wish to require that `c ~ Show`  maybe `c a` implies `Show a`. So I write this:
```haskell
instance (forall x . c x => Show x) => Show (Some c) where
showsPrec n (Some a) = showsPrec n a
```
But now this fails. The problem is that the instance gets expanded to
```haskell
instance (forall x . c x => Show x) => Show (Some c) where
showsPrec n (Some a) = showsPrec n a
show = $dmshow
```
where `$dmshow :: Show a => a > String` is the default method implementation for `show`. When typechecking this method, GHC needs to satisfy `Show (Some c)`. The context includes two possibilities: the quantified constraint, and the toplevel instance declaration. Because local instances (= quantified constraints) shadow global ones, we use the first. So we reduce `[W] Show (Some c)` to `[W] c (Some c)`, which cannot be solved, leading to disaster.
This example first came to light in https://gitlab.haskell.org/ghc/ghc/issues/16502#note_253501, where it was copied from #17794.
Taking this new approach will likely fix #16502 and allow the original program in #17202 to be accepted. See also https://gitlab.haskell.org/ghc/ghc/issues/16502#note_253501 and https://gitlab.haskell.org/ghc/ghc/issues/16502#note_259055 for more test cases.
**Background**:
The current instance lookup (as documented [here](https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#instancelookup)) works as follows to solve a `[W] C T` constraint (for some class `C` and type `T`).
1. Look for local (nonquantified) assumptions for `[G] C T`.
2. Look for local quantified constraints whose conclusions match `C T`. If exactly one matches, select the constraint. Then, check whether any quantified constraints *unify* with `C T` (allowing any variables in `C T` to be bound). If any do, abort, complaining about potential incoherence. Otherwise, reduce `[W] C T` to the premise of the quantified constraint.
3. Same as (2), but using the global instance table.
**Proposal**:
Use specificity to disambiguate.
* Let `<=spec` denote a partial order on instance heads. `C T1 <=spec C T2` iff there exists a substitution `S` such that `S(T2) = T1`  just as is used with overlapping instances today.
* Let metavariable `I` denote givens. These can be nonquantified, quantified (local), or global.
* Define `locality(I)` be a number that denotes how local `I` is. The locality of a nonquantified given is 1, of a quantified local given is 2, and of a global is 3.
* Define partial order `<=` on instances as follows:
1. If `I1 <=spec I2` and `I2 <=spec I1`, then `I1 <= I2` is `locality(I1) <= locality(I2)`.
2. If neither `I1 <=spec I2` nor `I2 <=spec I1`, then `I1 <= I2` is `locality(I1) <= locality(I2)`.
3. Otherwise, `I1 <= I2` if `I1 <=spec I2`.
Here is the proposed instance lookup procedure:
1. Collect all givens `I` (of all localities) that match a target. Call this set `Is`. If `Is` is empty, fail.
2. Let `I0` be the minimum element of `Is` with respect to `<=`. (Consider `Is` to be setlike, discarding duplicates.) If `I0` is not defined, fail.
3. Let `Is'` be the set `Is` excluding `I0`. Case on the locality of `I0`:
* `locality(I0) = 1`: Succeed with `I0` (skipping last check, below).
* `locality(I0) = 2`: Go on to next step if `Is'` contains only global instances. If `Is'` contains local instances, fail.
* `locality(I0) = 3`: Fail if any element in `Is'` is a local quantified instance. Go on to next step if, for every `I'` in `Is'`, either `I0` is *overlapping* or `I'` is *overlappable*.
4. Collect all givens (of all localities) that *unify* with a target, excluding those in `Is`. If `IncoherentInstances` is off and this set contains at least one instances not labeled **incoherent**, fail.
5. Succeed with `I0`.
**Discussion**:
This new algorithm is meant to replicate current behavior, except in the scenario where a global instance is more specific than a local one, in which the global instance should be selected. I have tried to capture current behavior w.r.t. incoherent and overlapping instances. In any case, if my algorithm deviates from current behavior w.r.t. incoherent or overlapping instances, this deviation is unintentional.
Another possible approach is to put local and global instances on even footing (that is, set both to have locality 2) but to allow users to explicitly label local instances as overlapping. I prefer the tiered approach above, but there's something simpler about local overlapping instances, in that it's one mechanism to think about.**Summary:** Currently, quantified constraints shadow global instances. This ticket proposes to use specificity (in the sense used by overlapping instances) instead of shadowing.
**Motivation**
This looks like a sensible way of having a datatype that can store something of a type that supports some class interface:
```haskell
data Some (c :: Type > Constraint) where
Some :: c a => a > Some c
```
But now I want to write a `Show` instance. I can do this only when the existential `a` supports `Show`. But I don't wish to require that `c ~ Show`  maybe `c a` implies `Show a`. So I write this:
```haskell
instance (forall x . c x => Show x) => Show (Some c) where
showsPrec n (Some a) = showsPrec n a
```
But now this fails. The problem is that the instance gets expanded to
```haskell
instance (forall x . c x => Show x) => Show (Some c) where
showsPrec n (Some a) = showsPrec n a
show = $dmshow
```
where `$dmshow :: Show a => a > String` is the default method implementation for `show`. When typechecking this method, GHC needs to satisfy `Show (Some c)`. The context includes two possibilities: the quantified constraint, and the toplevel instance declaration. Because local instances (= quantified constraints) shadow global ones, we use the first. So we reduce `[W] Show (Some c)` to `[W] c (Some c)`, which cannot be solved, leading to disaster.
This example first came to light in https://gitlab.haskell.org/ghc/ghc/issues/16502#note_253501, where it was copied from #17794.
Taking this new approach will likely fix #16502 and allow the original program in #17202 to be accepted. See also https://gitlab.haskell.org/ghc/ghc/issues/16502#note_253501 and https://gitlab.haskell.org/ghc/ghc/issues/16502#note_259055 for more test cases.
**Background**:
The current instance lookup (as documented [here](https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#instancelookup)) works as follows to solve a `[W] C T` constraint (for some class `C` and type `T`).
1. Look for local (nonquantified) assumptions for `[G] C T`.
2. Look for local quantified constraints whose conclusions match `C T`. If exactly one matches, select the constraint. Then, check whether any quantified constraints *unify* with `C T` (allowing any variables in `C T` to be bound). If any do, abort, complaining about potential incoherence. Otherwise, reduce `[W] C T` to the premise of the quantified constraint.
3. Same as (2), but using the global instance table.
**Proposal**:
Use specificity to disambiguate.
* Let `<=spec` denote a partial order on instance heads. `C T1 <=spec C T2` iff there exists a substitution `S` such that `S(T2) = T1`  just as is used with overlapping instances today.
* Let metavariable `I` denote givens. These can be nonquantified, quantified (local), or global.
* Define `locality(I)` be a number that denotes how local `I` is. The locality of a nonquantified given is 1, of a quantified local given is 2, and of a global is 3.
* Define partial order `<=` on instances as follows:
1. If `I1 <=spec I2` and `I2 <=spec I1`, then `I1 <= I2` is `locality(I1) <= locality(I2)`.
2. If neither `I1 <=spec I2` nor `I2 <=spec I1`, then `I1 <= I2` is `locality(I1) <= locality(I2)`.
3. Otherwise, `I1 <= I2` if `I1 <=spec I2`.
Here is the proposed instance lookup procedure:
1. Collect all givens `I` (of all localities) that match a target. Call this set `Is`. If `Is` is empty, fail.
2. Let `I0` be the minimum element of `Is` with respect to `<=`. (Consider `Is` to be setlike, discarding duplicates.) If `I0` is not defined, fail.
3. Let `Is'` be the set `Is` excluding `I0`. Case on the locality of `I0`:
* `locality(I0) = 1`: Succeed with `I0` (skipping last check, below).
* `locality(I0) = 2`: Go on to next step if `Is'` contains only global instances. If `Is'` contains local instances, fail.
* `locality(I0) = 3`: Fail if any element in `Is'` is a local quantified instance. Go on to next step if, for every `I'` in `Is'`, either `I0` is *overlapping* or `I'` is *overlappable*.
4. Collect all givens (of all localities) that *unify* with a target, excluding those in `Is`. If `IncoherentInstances` is off and this set contains at least one instances not labeled **incoherent**, fail.
5. Succeed with `I0`.
**Discussion**:
This new algorithm is meant to replicate current behavior, except in the scenario where a global instance is more specific than a local one, in which the global instance should be selected. I have tried to capture current behavior w.r.t. incoherent and overlapping instances. In any case, if my algorithm deviates from current behavior w.r.t. incoherent or overlapping instances, this deviation is unintentional.
Another possible approach is to put local and global instances on even footing (that is, set both to have locality 2) but to allow users to explicitly label local instances as overlapping. I prefer the tiered approach above, but there's something simpler about local overlapping instances, in that it's one mechanism to think about.https://gitlab.haskell.org/ghc/ghc//issues/17790`case` needn't instantiate its scrutinee20200205T15:31:19ZRichard Eisenbergrae@richarde.dev`case` needn't instantiate its scrutineeConsider
```hs
foo = case id of id' > (id' 'x', id' True)
```
Should this be accepted or rejected? GHC currently rejects. But simply by changing [this line](https://gitlab.haskell.org/ghc/ghc/blob/4bada77d5882974514d85d4bd0fd4e1801dad755/compiler/typecheck/TcExpr.hs#L528) to use `tcInferSigma` instead of `tcInferRho`, the program is accepted. (That's really it! Try it at home!)
Should we make this change? It makes our language more expressive. It also gets us closer to the Platonic ideal of a HindleyMilner language design, in that users should never have to think about instantiation or generalization. And ML does it. If I write
```ml
let ex = match fun x > x with
 f > (f 'x', f true)
```
then `ocamlc` accepts without complaint. Actually, this ML example is even more interesting: not only does it *preserve* the polymorphism in the scrutinee, it actually *generalizes*. Really, if Damas and Milner had been examining a language with `case`, they would have said that we need generalization at `let` and at `case`.
Of course, we could use `tcInferSigma` (enabling the Haskell example) but not to generalization. That means that `foo` would be accepted, but this `bar` would be rejected:
```hs
bar = case \x > x of id' > (id' 'x', id' True)
```
That's a bit of a shame.
This ticket is to track this small design decision.Consider
```hs
foo = case id of id' > (id' 'x', id' True)
```
Should this be accepted or rejected? GHC currently rejects. But simply by changing [this line](https://gitlab.haskell.org/ghc/ghc/blob/4bada77d5882974514d85d4bd0fd4e1801dad755/compiler/typecheck/TcExpr.hs#L528) to use `tcInferSigma` instead of `tcInferRho`, the program is accepted. (That's really it! Try it at home!)
Should we make this change? It makes our language more expressive. It also gets us closer to the Platonic ideal of a HindleyMilner language design, in that users should never have to think about instantiation or generalization. And ML does it. If I write
```ml
let ex = match fun x > x with
 f > (f 'x', f true)
```
then `ocamlc` accepts without complaint. Actually, this ML example is even more interesting: not only does it *preserve* the polymorphism in the scrutinee, it actually *generalizes*. Really, if Damas and Milner had been examining a language with `case`, they would have said that we need generalization at `let` and at `case`.
Of course, we could use `tcInferSigma` (enabling the Haskell example) but not to generalization. That means that `foo` would be accepted, but this `bar` would be rejected:
```hs
bar = case \x > x of id' > (id' 'x', id' True)
```
That's a bit of a shame.
This ticket is to track this small design decision.https://gitlab.haskell.org/ghc/ghc//issues/17737Recursive superclass check is defeated by quantified constraints20200310T14:21:59ZRichard Eisenbergrae@richarde.devRecursive superclass check is defeated by quantified constraintsThis is accepted:
```hs
{# LANGUAGE QuantifiedConstraints, KindSignatures, ConstraintKinds #}
module Bug where
import Data.Kind
class ((() :: Constraint) => C a) => C a
```
The vacuous constraint `()` hides the recursive superclass `C a`. Note that I do not have `RecursiveSuperclasses` enabled.
The culprit is `TcTyDecls.checkClassCycles`.
This is not a "real" bug report, in that I found the problem only by reading the source code, not by observing the misbehavior. Still, it shouldn't be hard to fix. Should we just look through quantified constraints always?This is accepted:
```hs
{# LANGUAGE QuantifiedConstraints, KindSignatures, ConstraintKinds #}
module Bug where
import Data.Kind
class ((() :: Constraint) => C a) => C a
```
The vacuous constraint `()` hides the recursive superclass `C a`. Note that I do not have `RecursiveSuperclasses` enabled.
The culprit is `TcTyDecls.checkClassCycles`.
This is not a "real" bug report, in that I found the problem only by reading the source code, not by observing the misbehavior. Still, it shouldn't be hard to fix. Should we just look through quantified constraints always?Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.dev