GHC issueshttps://gitlab.haskell.org/ghc/ghc//issues20201125T11:34:50Zhttps://gitlab.haskell.org/ghc/ghc//issues/18987Quick Look does not zonk return types20201125T11:34:50ZRichard Eisenbergrae@richarde.devQuick Look does not zonk return typesTest case `impredicative/T17332`:
```hs
data Dict c where
MkDict :: c => Dict c
aux :: Dict (forall a. a)
aux = MkDict
```
The constraint `c` ends up in the solver as an `IrredPred`, which reveals the polytype `forall a. a`. But zonking to reveal a polytype should never happen outside of Quick Look, as `Note [Quick Look]` in GHC.Tc.Gen.App tells us.
A quick look didn't reveal exactly where to put the zonk, and I don't want to add yet another wrinkle to !4149. But when this bug is fixed, the `ForAllPred` case in `canIrred` should never happen.Test case `impredicative/T17332`:
```hs
data Dict c where
MkDict :: c => Dict c
aux :: Dict (forall a. a)
aux = MkDict
```
The constraint `c` ends up in the solver as an `IrredPred`, which reveals the polytype `forall a. a`. But zonking to reveal a polytype should never happen outside of Quick Look, as `Note [Quick Look]` in GHC.Tc.Gen.App tells us.
A quick look didn't reveal exactly where to put the zonk, and I don't want to add yet another wrinkle to !4149. But when this bug is fixed, the `ForAllPred` case in `canIrred` should never happen.https://gitlab.haskell.org/ghc/ghc//issues/18929Investigate touchable metavariables in Givens20201126T17:53:30ZRichard Eisenbergrae@richarde.devInvestigate touchable metavariables in Givens@simonpj believes it would be disastrous to ever have a touchable metavariable in a Given. I'm not quite as sure what the disaster would be, but I admit such a situation is suspect. But we can concoct such a thing:
```hs
{# LANGUAGE PolyKinds, PartialTypeSignatures #}
module Bug where
import Data.Proxy
class C a where
meth :: Proxy a > ()
f :: C a => Proxy a > _
f p = meth p
```
The partial signature for `f` is not kindgeneralized (the fact that it is partial means that we might want the definition of `f` to inform the kind of `a`) and thus the kind of `a` remains as a metavariable `kappa`. In the body of `f`, we have `[G] C kappa a`. We can see this in this snippet of `ddumptctrace` (with `fprintexplicitkinds` enabled):
```
tclevel = 1
work item = [WD] $dC_aoV {0}:: C @{k_aoT[tau:1]}
a_aoU[tau:1] (CNonCanonical)
inerts = {Dictionaries = [G] $dC_aoX {0}:: C @{k_aoT[tau:1]}
a_aoJ[tyv:1] (CDictCan)
```
The variable `k_aoT[tau:1]` is touchable and is not yet filled in. (It ends up being skolemised and quantified over, quite correctly.)
This ticket is to determine whether this situation is pernicious, and, if it is, figure out a way to rule it out.@simonpj believes it would be disastrous to ever have a touchable metavariable in a Given. I'm not quite as sure what the disaster would be, but I admit such a situation is suspect. But we can concoct such a thing:
```hs
{# LANGUAGE PolyKinds, PartialTypeSignatures #}
module Bug where
import Data.Proxy
class C a where
meth :: Proxy a > ()
f :: C a => Proxy a > _
f p = meth p
```
The partial signature for `f` is not kindgeneralized (the fact that it is partial means that we might want the definition of `f` to inform the kind of `a`) and thus the kind of `a` remains as a metavariable `kappa`. In the body of `f`, we have `[G] C kappa a`. We can see this in this snippet of `ddumptctrace` (with `fprintexplicitkinds` enabled):
```
tclevel = 1
work item = [WD] $dC_aoV {0}:: C @{k_aoT[tau:1]}
a_aoU[tau:1] (CNonCanonical)
inerts = {Dictionaries = [G] $dC_aoX {0}:: C @{k_aoT[tau:1]}
a_aoJ[tyv:1] (CDictCan)
```
The variable `k_aoT[tau:1]` is touchable and is not yet filled in. (It ends up being skolemised and quantified over, quite correctly.)
This ticket is to determine whether this situation is pernicious, and, if it is, figure out a way to rule it out.https://gitlab.haskell.org/ghc/ghc//issues/18910Orderdependent type inference due to Note [Instance and Given overlap]20201126T17:47:45ZRichard Eisenbergrae@richarde.devOrderdependent type inference due to Note [Instance and Given overlap]With some effort, I have produced
```hs
{# LANGUAGE ScopedTypeVariables, AllowAmbiguousTypes, TypeApplications,
TypeFamilies, PolyKinds, DataKinds, FlexibleInstances,
MultiParamTypeClasses, FlexibleContexts, PartialTypeSignatures #}
module Bug where
import Data.Proxy
class P a
class Q a
class R a b
newtype Tagged (t :: k) a = Tagged a
type family F a
type instance F (Tagged @Bool t a) = [a]
instance P x => Q [x]
instance (x ~ y) => R y [x]
wob :: forall a b. (Q [b], R b a) => a > Int
wob = undefined
it'sABoolNow :: forall (t :: Bool). Int
it'sABoolNow = undefined
class HasBoolKind t
instance k ~ Bool => HasBoolKind (t :: k)
it'sABoolLater :: forall t. HasBoolKind t => Int
it'sABoolLater = undefined
g :: forall t a. Q (F (Tagged t a)) => Proxy t > [a] > _
g _ x = it'sABoolNow @t + wob x
g2 :: forall t a. Q (F (Tagged t a)) => Proxy t > [a] > _
g2 _ x = wob x + it'sABoolNow @t
g3 :: forall t a. Q (F (Tagged t a)) => Proxy t > [a] > _
g3 _ x = it'sABoolLater @t + wob x
g4 :: forall t a. Q (F (Tagged t a)) => Proxy t > [a] > _
g4 _ x = wob x + it'sABoolLater @t
```
All of `g`, `g2`, and `g3` are accepted. `g4` is rejected. Note that `g4` is identical to `g3` except for changing the order of the summands.
What's going on:
Here is an excerpt from `Note [Instance and Given overlap]`:
```
Example, from the OutsideIn(X) paper:
instance P x => Q [x]
instance (x ~ y) => R y [x]
wob :: forall a b. (Q [b], R b a) => a > Int
g :: forall a. Q [a] => [a] > Int
g x = wob x
From 'g' we get the implication constraint:
forall a. Q [a] => (Q [beta], R beta [a])
If we react (Q [beta]) with its toplevel axiom, we end up with a
(P beta), which we have no way of discharging. On the other hand,
if we react R beta [a] with the toplevel we get (beta ~ a), which
is solvable and can help us rewrite (Q [beta]) to (Q [a]) which is
now solvable by the given Q [a].
```
Here is the scenario in the Note, when typechecking the Note's `g`:
```
[G] Q [a]
[W] Q [beta]
[W] R beta [a]
```
When we process the first Wanted, we might be tempted to use the instance, simplifying the Wanted to `P beta`. Doing this leads to failure. What we'd prefer is to recognize that the Given might be helpful later, and just to leave the Wanted asis. Then, processing the `[W] R beta [a]` tells us that `beta ~ a`, and we go home happy.
The scenario in this ticket is rather more complicated. The instances are unchanged, but now we have a type family `F` in the mix. It all looks like
```
t :: kappa
[G] Q (F (Tagged @kappa t a))
[W] Q [beta]
[W] R beta [a]
```
The question is: when processing the first Wanted, should the Given block GHC from using the global instance? (Sidenote: I've used partial type signatures and polykinds here as a sneaky way of getting a metavariable into a Given. The partial type signature stops GHC from kindgeneralizing the type, and thus `t`'s kind remains as `kappa` when processing the body.) If `kappa` is `Bool`, then the Given will eventually match and should block us from using the instance. If `kappa` is not `Bool`, then the Given will not apply. Yet in all of `g`..`g4`, `kappa` turns out to be `Bool`.
In `g`, we have `it'sABoolNow @t`, and the eager unifier sets `kappa := Bool` before the constraint solver gets a crack. The application of `F` reduces and the Given is recognized as relevant, blocking the use of the global instance.
In `g2`, the same happens.
In `g3`, we get a new `[W] HasBoolKind @kappa t`. This gets processed *before* the `Q [beta]` Wanted, and processing this sets `kappa := Bool`, leading the Given to reduce and block the use of the global instance.
In `g4`, however, the new `[W] HasBoolKind @kappa t` comes *after* the others. So we process `Q [beta]` *before* learning about `kappa`. The global instance is used, and we are left stuck with `[W] P a` that cannot be solved.
This all boils down to the `not (isFskTyVar tv)` check in `GHC.Tc.Solver.Monad.mightMatchLater`, which (effectively) says that type family applications in Givens match only themselves, not any arbitrary type. Removing that check fixes this problem. But it introduces another. The following program is accepted today:
```hs
{# LANGUAGE TypeFamilies, FlexibleInstances, FlexibleContexts #}
module Bug2 where
class C a where
meth :: a > ()
instance C Int where
meth _ = ()
type family F a
foo :: C (F a) => a > Int > ()
foo _ n = meth n
```
If we strike that check from `mightMatchLater`, we get
```
• Overlapping instances for C Int arising from a use of ‘meth’
Matching instances:
instance C Int  Defined at CbvOverlap.hs:10:10
There exists a (perhaps superclass) match:
from the context: C (F a)
bound by the type signature for:
foo :: forall a. C (F a) => a > Int > ()
at CbvOverlap.hs:15:132
(The choice depends on the instantiation of ‘’
To pick the first instance above, use IncoherentInstances
when compiling the other instance declarations)
• In the expression: meth n
In an equation for ‘foo’: foo _ n = meth n
```
The (unrelated) `[G] C (F a)` blocks the useful `instance C Int`. Worse, the error message says that the overlap depends on the instantiation of <<empty list>>.
This new problem is not just theoretical. In my !4149 patch, I essentially made this change unintentionally, and GHC's Parser.hs stopped compiling (in stage 2), due to its `DisambECP` shenanigans. It's easy for me to replicate the current behavior, so my branch can continue, but this bug will remain.
I'm not sure what the solution is. If we allow type family applications in Givens to match any potential type, we will unavoidably cause the second bug. So perhaps the best course of action is to let sleeping dogs lie. Yet I was uncomfortable reinstating the old behavior, because it smelled off... and I wanted to understand it better. Thus this ticket.With some effort, I have produced
```hs
{# LANGUAGE ScopedTypeVariables, AllowAmbiguousTypes, TypeApplications,
TypeFamilies, PolyKinds, DataKinds, FlexibleInstances,
MultiParamTypeClasses, FlexibleContexts, PartialTypeSignatures #}
module Bug where
import Data.Proxy
class P a
class Q a
class R a b
newtype Tagged (t :: k) a = Tagged a
type family F a
type instance F (Tagged @Bool t a) = [a]
instance P x => Q [x]
instance (x ~ y) => R y [x]
wob :: forall a b. (Q [b], R b a) => a > Int
wob = undefined
it'sABoolNow :: forall (t :: Bool). Int
it'sABoolNow = undefined
class HasBoolKind t
instance k ~ Bool => HasBoolKind (t :: k)
it'sABoolLater :: forall t. HasBoolKind t => Int
it'sABoolLater = undefined
g :: forall t a. Q (F (Tagged t a)) => Proxy t > [a] > _
g _ x = it'sABoolNow @t + wob x
g2 :: forall t a. Q (F (Tagged t a)) => Proxy t > [a] > _
g2 _ x = wob x + it'sABoolNow @t
g3 :: forall t a. Q (F (Tagged t a)) => Proxy t > [a] > _
g3 _ x = it'sABoolLater @t + wob x
g4 :: forall t a. Q (F (Tagged t a)) => Proxy t > [a] > _
g4 _ x = wob x + it'sABoolLater @t
```
All of `g`, `g2`, and `g3` are accepted. `g4` is rejected. Note that `g4` is identical to `g3` except for changing the order of the summands.
What's going on:
Here is an excerpt from `Note [Instance and Given overlap]`:
```
Example, from the OutsideIn(X) paper:
instance P x => Q [x]
instance (x ~ y) => R y [x]
wob :: forall a b. (Q [b], R b a) => a > Int
g :: forall a. Q [a] => [a] > Int
g x = wob x
From 'g' we get the implication constraint:
forall a. Q [a] => (Q [beta], R beta [a])
If we react (Q [beta]) with its toplevel axiom, we end up with a
(P beta), which we have no way of discharging. On the other hand,
if we react R beta [a] with the toplevel we get (beta ~ a), which
is solvable and can help us rewrite (Q [beta]) to (Q [a]) which is
now solvable by the given Q [a].
```
Here is the scenario in the Note, when typechecking the Note's `g`:
```
[G] Q [a]
[W] Q [beta]
[W] R beta [a]
```
When we process the first Wanted, we might be tempted to use the instance, simplifying the Wanted to `P beta`. Doing this leads to failure. What we'd prefer is to recognize that the Given might be helpful later, and just to leave the Wanted asis. Then, processing the `[W] R beta [a]` tells us that `beta ~ a`, and we go home happy.
The scenario in this ticket is rather more complicated. The instances are unchanged, but now we have a type family `F` in the mix. It all looks like
```
t :: kappa
[G] Q (F (Tagged @kappa t a))
[W] Q [beta]
[W] R beta [a]
```
The question is: when processing the first Wanted, should the Given block GHC from using the global instance? (Sidenote: I've used partial type signatures and polykinds here as a sneaky way of getting a metavariable into a Given. The partial type signature stops GHC from kindgeneralizing the type, and thus `t`'s kind remains as `kappa` when processing the body.) If `kappa` is `Bool`, then the Given will eventually match and should block us from using the instance. If `kappa` is not `Bool`, then the Given will not apply. Yet in all of `g`..`g4`, `kappa` turns out to be `Bool`.
In `g`, we have `it'sABoolNow @t`, and the eager unifier sets `kappa := Bool` before the constraint solver gets a crack. The application of `F` reduces and the Given is recognized as relevant, blocking the use of the global instance.
In `g2`, the same happens.
In `g3`, we get a new `[W] HasBoolKind @kappa t`. This gets processed *before* the `Q [beta]` Wanted, and processing this sets `kappa := Bool`, leading the Given to reduce and block the use of the global instance.
In `g4`, however, the new `[W] HasBoolKind @kappa t` comes *after* the others. So we process `Q [beta]` *before* learning about `kappa`. The global instance is used, and we are left stuck with `[W] P a` that cannot be solved.
This all boils down to the `not (isFskTyVar tv)` check in `GHC.Tc.Solver.Monad.mightMatchLater`, which (effectively) says that type family applications in Givens match only themselves, not any arbitrary type. Removing that check fixes this problem. But it introduces another. The following program is accepted today:
```hs
{# LANGUAGE TypeFamilies, FlexibleInstances, FlexibleContexts #}
module Bug2 where
class C a where
meth :: a > ()
instance C Int where
meth _ = ()
type family F a
foo :: C (F a) => a > Int > ()
foo _ n = meth n
```
If we strike that check from `mightMatchLater`, we get
```
• Overlapping instances for C Int arising from a use of ‘meth’
Matching instances:
instance C Int  Defined at CbvOverlap.hs:10:10
There exists a (perhaps superclass) match:
from the context: C (F a)
bound by the type signature for:
foo :: forall a. C (F a) => a > Int > ()
at CbvOverlap.hs:15:132
(The choice depends on the instantiation of ‘’
To pick the first instance above, use IncoherentInstances
when compiling the other instance declarations)
• In the expression: meth n
In an equation for ‘foo’: foo _ n = meth n
```
The (unrelated) `[G] C (F a)` blocks the useful `instance C Int`. Worse, the error message says that the overlap depends on the instantiation of <<empty list>>.
This new problem is not just theoretical. In my !4149 patch, I essentially made this change unintentionally, and GHC's Parser.hs stopped compiling (in stage 2), due to its `DisambECP` shenanigans. It's easy for me to replicate the current behavior, so my branch can continue, but this bug will remain.
I'm not sure what the solution is. If we allow type family applications in Givens to match any potential type, we will unavoidably cause the second bug. So perhaps the best course of action is to let sleeping dogs lie. Yet I was uncomfortable reinstating the old behavior, because it smelled off... and I wanted to understand it better. Thus this ticket.https://gitlab.haskell.org/ghc/ghc//issues/18891Kind inference for newtypes in GADT syntax is deeply broken20201125T17:38:55ZRichard Eisenbergrae@richarde.devKind inference for newtypes in GADT syntax is deeply brokenHere are some tales of destruction, all with `XUnliftedNewtypes` and `XNoCUSKs`:
```hs
newtype N :: forall k. TYPE k where
MkN :: N > N
```
gives
```
Scratch.hs:34:3: error:
• Expected a type, but ‘N’ has kind ‘*’
• In the definition of data constructor ‘MkN’
In the newtype declaration for ‘N’
```

```hs
type N :: forall k. TYPE k
newtype N :: forall k. TYPE k where
MkN :: N > N
```
gives
```
Scratch.hs:35:3: error:
• A newtype constructor must have a return type of form T a1 ... an
MkN :: N > N
• In the definition of data constructor ‘MkN’
In the newtype declaration for ‘N’
```

```hs
newtype N :: forall k > TYPE k where
MkN :: N m > N m
```
gives
```
Scratch.hs:35:3: error:
• Expected a type, but ‘N m’ has kind ‘TYPE m’
• In the definition of data constructor ‘MkN’
In the newtype declaration for ‘N’
```

```hs
type N :: forall k > TYPE k
newtype N :: forall k > TYPE k where
MkN :: N m > N m
```
succeeds.
I think all these examples should succeed. All but the last cause a DEBUG build of GHC to panic.
I think the problem is that the `res_kind` passed to `kcConArgTys` has the wrong scope: it mentions variables in the type head, but these are utterly distinct from the variables in the constructor type.Here are some tales of destruction, all with `XUnliftedNewtypes` and `XNoCUSKs`:
```hs
newtype N :: forall k. TYPE k where
MkN :: N > N
```
gives
```
Scratch.hs:34:3: error:
• Expected a type, but ‘N’ has kind ‘*’
• In the definition of data constructor ‘MkN’
In the newtype declaration for ‘N’
```

```hs
type N :: forall k. TYPE k
newtype N :: forall k. TYPE k where
MkN :: N > N
```
gives
```
Scratch.hs:35:3: error:
• A newtype constructor must have a return type of form T a1 ... an
MkN :: N > N
• In the definition of data constructor ‘MkN’
In the newtype declaration for ‘N’
```

```hs
newtype N :: forall k > TYPE k where
MkN :: N m > N m
```
gives
```
Scratch.hs:35:3: error:
• Expected a type, but ‘N m’ has kind ‘TYPE m’
• In the definition of data constructor ‘MkN’
In the newtype declaration for ‘N’
```

```hs
type N :: forall k > TYPE k
newtype N :: forall k > TYPE k where
MkN :: N m > N m
```
succeeds.
I think all these examples should succeed. All but the last cause a DEBUG build of GHC to panic.
I think the problem is that the `res_kind` passed to `kcConArgTys` has the wrong scope: it mentions variables in the type head, but these are utterly distinct from the variables in the constructor type.https://gitlab.haskell.org/ghc/ghc//issues/18875Occurschecky Givens rewrite once, but not twice20201126T17:47:44ZRichard Eisenbergrae@richarde.devOccurschecky Givens rewrite once, but not twiceGHC remarkably accepts this program:
```hs
type family UnMaybe a where
UnMaybe (Maybe b) = b
class C c where
meth :: c
instance C (Maybe d) where
meth = Nothing
f :: (e ~ Maybe (UnMaybe e)) => e
f = meth
```
This is remarkable because satisfying the `C e` constraint arising from the use of `meth` requires using the `e ~ Maybe (UnMaybe e)` given, despite the fact that it has an occurscheck failure. That is, GHC must rewrite `e` to `Maybe (UnMaybe e)` to solve the class constraint, yet not fall into a look trying to expand `e` further. This works due to the way GHC currently uses flatteningskolems to deal with type family applications. (The program above does not work on the current tip of !4149, which avoids this flattening mechanism.)
However, GHC rejects this program:
```hs
type family G a b where
G (Maybe c) d = d
h :: (e ~ Maybe (G e f)) => e > f
h (Just x) = x
```
Here, `h` has a similar given with an occurscheck failure. In contrast to the first example, though, we need to use the equation *twice* in order to accept this program. Specifically, we have
```
[G] e ~ Maybe (G e f)
[W] e ~ Maybe f
```
Using the Given for rewriting once gives us
```
[W] Maybe (G e f) ~ Maybe f
```
which decomposes to
```
[W] G e f ~ f
```
But now, we must use the given *again* to get
```
[W] G (Maybe (G e f)) f ~ f
```
so that can reduce to
```
[W] f ~ f
```
and be solved.
I think this will be hard to achieve in practice (rewriting twice). Might we need even more rewrites in pathological scenarios? I don't know.
The purpose of this ticket is more to record the incompleteness than to actively agitate for a solution. This did not arise in a real application and would likely be hard to fix.GHC remarkably accepts this program:
```hs
type family UnMaybe a where
UnMaybe (Maybe b) = b
class C c where
meth :: c
instance C (Maybe d) where
meth = Nothing
f :: (e ~ Maybe (UnMaybe e)) => e
f = meth
```
This is remarkable because satisfying the `C e` constraint arising from the use of `meth` requires using the `e ~ Maybe (UnMaybe e)` given, despite the fact that it has an occurscheck failure. That is, GHC must rewrite `e` to `Maybe (UnMaybe e)` to solve the class constraint, yet not fall into a look trying to expand `e` further. This works due to the way GHC currently uses flatteningskolems to deal with type family applications. (The program above does not work on the current tip of !4149, which avoids this flattening mechanism.)
However, GHC rejects this program:
```hs
type family G a b where
G (Maybe c) d = d
h :: (e ~ Maybe (G e f)) => e > f
h (Just x) = x
```
Here, `h` has a similar given with an occurscheck failure. In contrast to the first example, though, we need to use the equation *twice* in order to accept this program. Specifically, we have
```
[G] e ~ Maybe (G e f)
[W] e ~ Maybe f
```
Using the Given for rewriting once gives us
```
[W] Maybe (G e f) ~ Maybe f
```
which decomposes to
```
[W] G e f ~ f
```
But now, we must use the given *again* to get
```
[W] G (Maybe (G e f)) f ~ f
```
so that can reduce to
```
[W] f ~ f
```
and be solved.
I think this will be hard to achieve in practice (rewriting twice). Might we need even more rewrites in pathological scenarios? I don't know.
The purpose of this ticket is more to record the incompleteness than to actively agitate for a solution. This did not arise in a real application and would likely be hard to fix.https://gitlab.haskell.org/ghc/ghc//issues/18873Quantified equality constraints are not used for rewriting20201021T22:23:07ZRichard Eisenbergrae@richarde.devQuantified equality constraints are not used for rewritingIf I say
```hs
type family F a b where
F [_] b = b
f :: forall a b. (a ~ [b]) => F a b > b
f x = x
```
GHC smiles upon me: the equality constraint rewrites `a` to `[b]`, and then `F [b] b` can reduce to `b`, and all is well.
But if I say
```hs
type family F a b where
F [_] b = b
class Truth
instance Truth
f :: forall a b. (Truth => a ~ [b]) => F a b > b
f x = x
```
I get an error, saying `F a b` does not match `b`. This is because the equality, hidden behind `Truth`, is not used for rewriting, and thus GHC cannot figure out that `F a b` can reduce.
I don't see an easy solution here.
This isn't just me grousing: a problem on !4149 could be worked around if GHC used such equalities for rewriting. And so if we can solve this problem, we can solve the other one. My expectation is that we won't solve this one, though.If I say
```hs
type family F a b where
F [_] b = b
f :: forall a b. (a ~ [b]) => F a b > b
f x = x
```
GHC smiles upon me: the equality constraint rewrites `a` to `[b]`, and then `F [b] b` can reduce to `b`, and all is well.
But if I say
```hs
type family F a b where
F [_] b = b
class Truth
instance Truth
f :: forall a b. (Truth => a ~ [b]) => F a b > b
f x = x
```
I get an error, saying `F a b` does not match `b`. This is because the equality, hidden behind `Truth`, is not used for rewriting, and thus GHC cannot figure out that `F a b` can reduce.
I don't see an easy solution here.
This isn't just me grousing: a problem on !4149 could be worked around if GHC used such equalities for rewriting. And so if we can solve this problem, we can solve the other one. My expectation is that we won't solve this one, though.https://gitlab.haskell.org/ghc/ghc//issues/18851Nonconfluence around functional dependencies20201109T13:52:11ZRichard Eisenbergrae@richarde.devNonconfluence around functional dependenciesIn #18759 (starting at https://gitlab.haskell.org/ghc/ghc//issues/18759#note_306441 and then refined in https://gitlab.haskell.org/ghc/ghc//issues/18759#note_306722, but you don't need to read that ticket to understand this one), we explored various ways of disabling the coverage condition for functional dependencies. In https://gitlab.haskell.org/ghc/ghc//issues/18759#note_307486, @simonpj asks whether these techniques can disrupt confluence.
They can.
Here is the example:
```hs
{# LANGUAGE FunctionalDependencies, FlexibleInstances, UndecidableInstances,
ScopedTypeVariables, TypeFamilies, TypeApplications,
FlexibleContexts, AllowAmbiguousTypes #}
module Bug where
class C a b  a > b
instance C Int b => C Int b
class IsInt int
instance int ~ Int => IsInt int
data A
instance Show A where
show _ = "A"
data B
instance Show B where
show _ = "B"
f :: forall a b c int. (Show a, Show b, Show c, C int a, C int b, C int c, IsInt int) => String
f = show (undefined :: c)
g = f @A @B
```
`g` evaluates to `"B"`. If I switch the order of the `C int a` and `C int b` constraints in the type of `f`, `g` will evaluate to `"A"`. Urgh.
(Sidenote: this file needs `AllowAmbiguousTypes`, but there are no ambiguous types here. That bug is reported as #18850.)
What's going on? When calling `f` from `g`, GHC needs to figure out how to instantiate the type variables `a`, `b`, `c`, and `int`, and GHC must find dictionaries to supply for all the class constraints. First, GHC creates unification variables `a0`, `b0`, `c0`, and `int0`. The type applications tell us `a0 := A` and `b0 := B`. Good. Then we have these constraints:
```
[W] w1 : Show A
[W] w2 : Show B
[W] w3 : Show c0
[W] w4 : C int0 A
[W] w5 : C int0 B
[W] w6 : C int0 c0
[W] w7 : IsInt int0
```
GHC processes these in the order given. `w1` and `w2` are easily despatched. `w3` doesn't make any progress at all. Neither does `w4` or `w5`. So we're then in this state:
```
worklist: [W] w6 : C int0 c0
[W] w7 : IsInt int0
inerts: [W] w3 : Show c0
[W] w4 : C int0 A
[W] w5 : C int0 B
```
We then look at `w6`. It doesn't make progress. But then GHC looks at the inerts, and sees that `w4` and `w5` have the same first argument to `C` (`int0`) as the work item `w6`. Because of the functional dependency on `C`, this means that `c0` must match the second argument to `C` in the inert. The problem is that there are *two* such inerts! GHC chooses the last one, arbitrarily. Thus, we get `c0 := B` and carry on. If the constraints were processed in a different order, we'd end up with `c0 := A`. This is classic nonconfluence.
Why have `IsInt` here? It's to slow down GHC. If we just wrote an explicit `Int` in the type signature for `f`, then GHC would eagerly solve `w4' : C Int A` and `w5' : C Int B`. When processing `w6' : C Int c0`, GHC wouldn't have any inerts to look at. Instead, it would look at the instance for `C`, which is unhelpful in this case. Indeed, moving the `IsInt int` constraint earlier (before the `C` constraints) in `f`'s type signature causes GHC to error, as it doesn't know how to instantiate `c0`, having lost the hints from the inerts. (More nonconfluence!)
What to do? I think the next step is to compare this to the [constrainthandling rules paper](https://www.researchgate.net/profile/Martin_Sulzmann/publication/213885702_Understanding_Functional_Dependencies_via_Constraint_Handling_Rules/links/09e41511297969891f000000.pdf), which proves confluence, and see whether that paper has a mistake, or where GHC violates an assumption in that paper. (Probably the latter: my instance for `C` is very naughty.)In #18759 (starting at https://gitlab.haskell.org/ghc/ghc//issues/18759#note_306441 and then refined in https://gitlab.haskell.org/ghc/ghc//issues/18759#note_306722, but you don't need to read that ticket to understand this one), we explored various ways of disabling the coverage condition for functional dependencies. In https://gitlab.haskell.org/ghc/ghc//issues/18759#note_307486, @simonpj asks whether these techniques can disrupt confluence.
They can.
Here is the example:
```hs
{# LANGUAGE FunctionalDependencies, FlexibleInstances, UndecidableInstances,
ScopedTypeVariables, TypeFamilies, TypeApplications,
FlexibleContexts, AllowAmbiguousTypes #}
module Bug where
class C a b  a > b
instance C Int b => C Int b
class IsInt int
instance int ~ Int => IsInt int
data A
instance Show A where
show _ = "A"
data B
instance Show B where
show _ = "B"
f :: forall a b c int. (Show a, Show b, Show c, C int a, C int b, C int c, IsInt int) => String
f = show (undefined :: c)
g = f @A @B
```
`g` evaluates to `"B"`. If I switch the order of the `C int a` and `C int b` constraints in the type of `f`, `g` will evaluate to `"A"`. Urgh.
(Sidenote: this file needs `AllowAmbiguousTypes`, but there are no ambiguous types here. That bug is reported as #18850.)
What's going on? When calling `f` from `g`, GHC needs to figure out how to instantiate the type variables `a`, `b`, `c`, and `int`, and GHC must find dictionaries to supply for all the class constraints. First, GHC creates unification variables `a0`, `b0`, `c0`, and `int0`. The type applications tell us `a0 := A` and `b0 := B`. Good. Then we have these constraints:
```
[W] w1 : Show A
[W] w2 : Show B
[W] w3 : Show c0
[W] w4 : C int0 A
[W] w5 : C int0 B
[W] w6 : C int0 c0
[W] w7 : IsInt int0
```
GHC processes these in the order given. `w1` and `w2` are easily despatched. `w3` doesn't make any progress at all. Neither does `w4` or `w5`. So we're then in this state:
```
worklist: [W] w6 : C int0 c0
[W] w7 : IsInt int0
inerts: [W] w3 : Show c0
[W] w4 : C int0 A
[W] w5 : C int0 B
```
We then look at `w6`. It doesn't make progress. But then GHC looks at the inerts, and sees that `w4` and `w5` have the same first argument to `C` (`int0`) as the work item `w6`. Because of the functional dependency on `C`, this means that `c0` must match the second argument to `C` in the inert. The problem is that there are *two* such inerts! GHC chooses the last one, arbitrarily. Thus, we get `c0 := B` and carry on. If the constraints were processed in a different order, we'd end up with `c0 := A`. This is classic nonconfluence.
Why have `IsInt` here? It's to slow down GHC. If we just wrote an explicit `Int` in the type signature for `f`, then GHC would eagerly solve `w4' : C Int A` and `w5' : C Int B`. When processing `w6' : C Int c0`, GHC wouldn't have any inerts to look at. Instead, it would look at the instance for `C`, which is unhelpful in this case. Indeed, moving the `IsInt int` constraint earlier (before the `C` constraints) in `f`'s type signature causes GHC to error, as it doesn't know how to instantiate `c0`, having lost the hints from the inerts. (More nonconfluence!)
What to do? I think the next step is to compare this to the [constrainthandling rules paper](https://www.researchgate.net/profile/Martin_Sulzmann/publication/213885702_Understanding_Functional_Dependencies_via_Constraint_Handling_Rules/links/09e41511297969891f000000.pdf), which proves confluence, and see whether that paper has a mistake, or where GHC violates an assumption in that paper. (Probably the latter: my instance for `C` is very naughty.)https://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/18758Remove NoGhcTc, allow HsType GhcTc, HsDecl GhcTc20200930T20:28:26ZVladislav ZavialovRemove NoGhcTc, allow HsType GhcTc, HsDecl GhcTc## Background
Currently, we carefully avoid `HsType GhcTc` or `HsDecl GhcTc`, by means of the `NoGhcTc` type family:
```
 HsAppType (XAppTypeE p)  After typechecking: the type argument
(LHsExpr p)
(LHsWcType (NoGhcTc p))  ^ Visible type application
```
The primary reason for this is that kindchecking and desugaring of types are intertwined. We mostly work with `TcType` instead of `HsType GhcTc` because it's more convenient in some places (e.g. in `unifyKind` and `unifyType`).
## Motivation A
A better architecture would be to have similar pipelines for terms and types:
* `HsExpr GhcPs > HsExpr GhcRn > HsExpr GhcTc`
* `HsType GhcPs > HsType GhcRn > HsType GhcTc`
This would allow us to talk about e.g. `HsDecl GhcTc`. For example, when discussing #12088, there was an idea of a refactoring that would separate `tcTyClDecl` and zonking. But then we'd like the type of `tcTyClDecl` to be:
```haskell
tcTyClDecl :: LTyClDecl GhcRn > TcM (LTyClDecl GhcTc)
```
And that's not currently possible.
## Motivation B
This would facilitate fixing #15824, for instance, as we could use `HsType GhcTc` as the input to `GHC.Tc.Gen.Splice.reifyType`. This way, we would retain the `HsOpTy` and `HsAppTy` distinction.
## Partial Solution
In order to address Motivation B, we would need to properly embed coercions into `HsType GhcTc` and start using it throughout the type checker. However, that would be a very major, intrusive refactoring. Before we do that, there's a stopgap solution that could be used to address Motivation A.
Define the following `XXType` instance:
```
type instance XXType GhcTc = HsTypeTc
data HsTypeTc = HsTypeTc TcType SDoc
```
Then `HsType GhcTc` would only ever use `XHsType (HsTypeTc ty doc)`. The fields are as follows:
* `TcType` is the kindchecked, desugared type
* `SDoc` is the result of pretty printing `HsType GhcRn`, before parentheses and infix operators were discarded
This is sufficient to let us talk about `HsType GhcTc` and `HsDecl GhcTc`, and remove the `NoGhcTc` type family.
## Full Solution
The full solution would involve using `HsType GhcTc` throughout the type checker, rewriting zonking and unification to work over `HsType GhcTc`, and so on. It would address Motivation A, and also let us remove the notion of `TcType`: the type checker would work with `HsType GhcTc`, and `Type` would be only used in Core. That would be a nice improvement, as we could remove `TcTyVar` and `AnonArgFlag` (maybe something else?) from the syntax of Core.
## Completion
1. The partial solution is implemented.
I think we should start with the partial solution, so that's what this ticket is about. The full solution will require much more thought and design effort, so we can get back to it later.## Background
Currently, we carefully avoid `HsType GhcTc` or `HsDecl GhcTc`, by means of the `NoGhcTc` type family:
```
 HsAppType (XAppTypeE p)  After typechecking: the type argument
(LHsExpr p)
(LHsWcType (NoGhcTc p))  ^ Visible type application
```
The primary reason for this is that kindchecking and desugaring of types are intertwined. We mostly work with `TcType` instead of `HsType GhcTc` because it's more convenient in some places (e.g. in `unifyKind` and `unifyType`).
## Motivation A
A better architecture would be to have similar pipelines for terms and types:
* `HsExpr GhcPs > HsExpr GhcRn > HsExpr GhcTc`
* `HsType GhcPs > HsType GhcRn > HsType GhcTc`
This would allow us to talk about e.g. `HsDecl GhcTc`. For example, when discussing #12088, there was an idea of a refactoring that would separate `tcTyClDecl` and zonking. But then we'd like the type of `tcTyClDecl` to be:
```haskell
tcTyClDecl :: LTyClDecl GhcRn > TcM (LTyClDecl GhcTc)
```
And that's not currently possible.
## Motivation B
This would facilitate fixing #15824, for instance, as we could use `HsType GhcTc` as the input to `GHC.Tc.Gen.Splice.reifyType`. This way, we would retain the `HsOpTy` and `HsAppTy` distinction.
## Partial Solution
In order to address Motivation B, we would need to properly embed coercions into `HsType GhcTc` and start using it throughout the type checker. However, that would be a very major, intrusive refactoring. Before we do that, there's a stopgap solution that could be used to address Motivation A.
Define the following `XXType` instance:
```
type instance XXType GhcTc = HsTypeTc
data HsTypeTc = HsTypeTc TcType SDoc
```
Then `HsType GhcTc` would only ever use `XHsType (HsTypeTc ty doc)`. The fields are as follows:
* `TcType` is the kindchecked, desugared type
* `SDoc` is the result of pretty printing `HsType GhcRn`, before parentheses and infix operators were discarded
This is sufficient to let us talk about `HsType GhcTc` and `HsDecl GhcTc`, and remove the `NoGhcTc` type family.
## Full Solution
The full solution would involve using `HsType GhcTc` throughout the type checker, rewriting zonking and unification to work over `HsType GhcTc`, and so on. It would address Motivation A, and also let us remove the notion of `TcType`: the type checker would work with `HsType GhcTc`, and `Type` would be only used in Core. That would be a nice improvement, as we could remove `TcTyVar` and `AnonArgFlag` (maybe something else?) from the syntax of Core.
## Completion
1. The partial solution is implemented.
I think we should start with the partial solution, so that's what this ticket is about. The full solution will require much more thought and design effort, so we can get back to it later.9.2.1Vladislav ZavialovVladislav Zavialovhttps://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 expression20200929T15:42:03ZArnaud 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/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?20200921T22:31:11ZRichard Eisenbergrae@richarde.devWhy check for fdefertypeerrors in metaTyVarUpdateOK?Function `metaTyVarUpdateOK` changes its behavior depending on the presence of `fdefertypeerrors` in an obscure case around heterogeneous equalities; see the code in `preCheck` that deals with `badCoercionHoleCo`. 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 `metaTyVarUpdateOK` changes its behavior depending on the presence of `fdefertypeerrors` in an obscure case around heterogeneous equalities; see the code in `preCheck` that deals with `badCoercionHoleCo`. 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 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/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!