GHC issueshttps://gitlab.haskell.org/ghc/ghc//issues20201221T11:00:00Zhttps://gitlab.haskell.org/ghc/ghc//issues/18987Quick Look does not zonk return types20201221T11:00:00ZRichard 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 Givens20210102T14:14:41ZRichard 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/18920ghc8.8 does not infer kind20201109T14:13:59Zjwaldmannghc8.8 does not infer kindRejected by ghc8.8.4 with
```
should.hs:27:12: error:
• Expected kind ‘* > *’, but ‘solver’ has kind ‘*’
• In the first argument of ‘Solver’, namely ‘solver’
In the type ‘(Solver solver, Queue q, Transformer t) =>
Int > q > t > EvalState t > solver (Int, [a])’
In the type declaration for ‘ContinueSig’
```
but accepted by 8.6.5, 8.10.2. 9.0.1alpha1.
```
{# LANGUAGE TypeFamilies #}
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE Rank2Types #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE GADTs #}
class Monad solver => Solver solver where
type Constraint solver :: *
type Label solver :: *
class Queue q
data Tree s a where
NewVar :: Term s t => (t > Tree s a) > Tree s a
class Solver solver => Term solver term
class Transformer t where
type EvalState t :: *
type TreeState t :: *
type ForSolver t :: (* > *)
type ForResult t :: *
nextT :: SearchSig (ForSolver t) q t (ForResult t)
returnT :: ContinueSig solver q t (ForResult t)
type ContinueSig solver q t a =
( Solver solver, Queue q, Transformer t )
=> Int > q > t > EvalState t
> solver (Int, [a])
type SearchSig solver q t a =
(Solver solver, Queue q, Transformer t )
=> Int > Tree solver a > q > t > EvalState t > TreeState t
> solver (Int,[a])
```
8.8 accepts this after introducing this:
```
type ContinueSig (solver :: * > *) q t a =
...
```Rejected by ghc8.8.4 with
```
should.hs:27:12: error:
• Expected kind ‘* > *’, but ‘solver’ has kind ‘*’
• In the first argument of ‘Solver’, namely ‘solver’
In the type ‘(Solver solver, Queue q, Transformer t) =>
Int > q > t > EvalState t > solver (Int, [a])’
In the type declaration for ‘ContinueSig’
```
but accepted by 8.6.5, 8.10.2. 9.0.1alpha1.
```
{# LANGUAGE TypeFamilies #}
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE Rank2Types #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE GADTs #}
class Monad solver => Solver solver where
type Constraint solver :: *
type Label solver :: *
class Queue q
data Tree s a where
NewVar :: Term s t => (t > Tree s a) > Tree s a
class Solver solver => Term solver term
class Transformer t where
type EvalState t :: *
type TreeState t :: *
type ForSolver t :: (* > *)
type ForResult t :: *
nextT :: SearchSig (ForSolver t) q t (ForResult t)
returnT :: ContinueSig solver q t (ForResult t)
type ContinueSig solver q t a =
( Solver solver, Queue q, Transformer t )
=> Int > q > t > EvalState t
> solver (Int, [a])
type SearchSig solver q t a =
(Solver solver, Queue q, Transformer t )
=> Int > Tree solver a > q > t > EvalState t > TreeState t
> solver (Int,[a])
```
8.8 accepts this after introducing this:
```
type ContinueSig (solver :: * > *) q t a =
...
```8.10.1https://gitlab.haskell.org/ghc/ghc//issues/18910Orderdependent type inference due to Note [Instance and Given overlap]20210106T03:39:21ZRichard 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 broken20201208T21:03:16ZRichard 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.9.2.1https://gitlab.haskell.org/ghc/ghc//issues/18875Occurschecky Givens rewrite once, but not twice20201204T22:10:52ZRichard 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 rewriting20201210T20:30:27ZRichard 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/18863Visibility mismatch between data declaration and kind signature, accepted!20201031T11:08:25ZIcelandjackVisibility mismatch between data declaration and kind signature, accepted!```haskell
{# Language PolyKinds #}
{# Language RankNTypes #}
{# Language StandaloneKindSignatures #}
import Data.Kind
type ID :: forall i > i > Type
data ID :: forall i > i > Type
```
This compiles on 8.10.0.20191123, if we change the standalone kind signature `forall>` to `forall.` we get an error. Obviously?
```haskell
 • Couldn't match expected kind ‘forall i1 > i1 > *’
 with actual kind ‘i > *’
 • In the data type declaration for ‘ID’
 
 8  data ID :: forall i > i > Type
  ^^^^^^^
type ID :: forall i. i > Type
data ID :: forall i > i > Type
```
But then why does this compile
```haskell
type ID :: forall i > i > Type
data ID :: forall i. i > Type
``````haskell
{# Language PolyKinds #}
{# Language RankNTypes #}
{# Language StandaloneKindSignatures #}
import Data.Kind
type ID :: forall i > i > Type
data ID :: forall i > i > Type
```
This compiles on 8.10.0.20191123, if we change the standalone kind signature `forall>` to `forall.` we get an error. Obviously?
```haskell
 • Couldn't match expected kind ‘forall i1 > i1 > *’
 with actual kind ‘i > *’
 • In the data type declaration for ‘ID’
 
 8  data ID :: forall i > i > Type
  ^^^^^^^
type ID :: forall i. i > Type
data ID :: forall i > i > Type
```
But then why does this compile
```haskell
type ID :: forall i > i > Type
data ID :: forall i. i > Type
```9.2.1https://gitlab.haskell.org/ghc/ghc//issues/18851Nonconfluence in the solver20210104T22:12:36ZRichard Eisenbergrae@richarde.devNonconfluence in the solverIn #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. (EDIT: Furthermore, more hammering in this direction discovered nonconfluence even *without* functional dependencies. See https://gitlab.haskell.org/ghc/ghc//issues/18851#note_318471.)
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. (EDIT: Furthermore, more hammering in this direction discovered nonconfluence even *without* functional dependencies. See https://gitlab.haskell.org/ghc/ghc//issues/18851#note_318471.)
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 GhcTc20210328T09:35:04ZVladislav 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/18753Tighten up the treatment of loose types in the solver20200930T16:21:20ZRichard Eisenbergrae@richarde.devTighten up the treatment of loose types in the solver`GHC.Tc.Solver.Monad` includes
```
Note [Use loose types in inert set]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Say we know (Eq (a > c1)) and we need (Eq (a > c2)). One is clearly
solvable from the other. So, we do lookup in the inert set using
loose types, which omits the kindcheck.
We must be careful when using the result of a lookup because it may
not match the requested info exactly!
```
There are several problems.
* We aren't always careful. For example, `lookupInInerts` tries `lookupSolvedDict` and then `lookupInertDict`, both of which use this "loose" lookup. Yet the result of `lookupInInerts` just uses the result, without any special handling to take the fact that the types might not match exactly.
* The Note doesn't actually make sense. The only difference between `Eq (a > c1)` and `Eq (a > c2)` is the coercion. But I sincerely hope we never care about the contents of a coercion. So even if we use evidence of type `Eq (a > c1)` where GHC is expecting `Eq (a > c2)` (assuming `c1` and `c2` have the same type), all will be well.
* What I think the Note is trying to say will never happen. That is, the actual implementation of the inertset lookup tries to match types while ignoring their kinds. (Normal type matching requires that the kind matches also.) So a better example would be something like comparing `Eq (a :: k1)` with `Eq (a :: k2)`. But that's impossible, even with casts: all type families and classes have *closed* kinds, meaning that any variables that appear in the kinds of arguments must themselves be earlier arguments. In other words, if I have welltyped `T blah1 (... :: kind1)` and `T blah2 (... :: kind2)`, then either `kind1` equals `kind2` or `blah1` and `blah2` must differ. We use this logic elsewhere  in particular, in the pure unifier.
Conclusions:
* Using "loose" matching (that is, ignoring kinds) in the solver is the right thing.
* We should update the Note with my argument above.
* No special care needs to be taken when using loose matching in this way. This means we can drop a few redundant equality checks (e.g. in `lookupFlatCache`).
I'm pretty confident about this all, but I'd like a doublecheck before I commit a fix.`GHC.Tc.Solver.Monad` includes
```
Note [Use loose types in inert set]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Say we know (Eq (a > c1)) and we need (Eq (a > c2)). One is clearly
solvable from the other. So, we do lookup in the inert set using
loose types, which omits the kindcheck.
We must be careful when using the result of a lookup because it may
not match the requested info exactly!
```
There are several problems.
* We aren't always careful. For example, `lookupInInerts` tries `lookupSolvedDict` and then `lookupInertDict`, both of which use this "loose" lookup. Yet the result of `lookupInInerts` just uses the result, without any special handling to take the fact that the types might not match exactly.
* The Note doesn't actually make sense. The only difference between `Eq (a > c1)` and `Eq (a > c2)` is the coercion. But I sincerely hope we never care about the contents of a coercion. So even if we use evidence of type `Eq (a > c1)` where GHC is expecting `Eq (a > c2)` (assuming `c1` and `c2` have the same type), all will be well.
* What I think the Note is trying to say will never happen. That is, the actual implementation of the inertset lookup tries to match types while ignoring their kinds. (Normal type matching requires that the kind matches also.) So a better example would be something like comparing `Eq (a :: k1)` with `Eq (a :: k2)`. But that's impossible, even with casts: all type families and classes have *closed* kinds, meaning that any variables that appear in the kinds of arguments must themselves be earlier arguments. In other words, if I have welltyped `T blah1 (... :: kind1)` and `T blah2 (... :: kind2)`, then either `kind1` equals `kind2` or `blah1` and `blah2` must differ. We use this logic elsewhere  in particular, in the pure unifier.
Conclusions:
* Using "loose" matching (that is, ignoring kinds) in the solver is the right thing.
* We should update the Note with my argument above.
* No special care needs to be taken when using loose matching in this way. This means we can drop a few redundant equality checks (e.g. in `lookupFlatCache`).
I'm pretty confident about this all, but I'd like a doublecheck before I commit a fix.https://gitlab.haskell.org/ghc/ghc//issues/18739Infer multiplicity of let expression20210412T17:45:47ZArnaud 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 expression20210412T17:45:47ZArnaud 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/18715ThBrackCtxt is unused20200921T21:17:06ZRyan ScottThBrackCtxt is unusedThe [`UserTypeCtxt`](https://gitlab.haskell.org/ghc/ghc//blob/a1f34d37b47826e86343e368a5c00f1a4b1f2bce/compiler/GHC/Tc/Types/Origin.hs#L5792) data type defines a context for TH brackets:
```hs
data UserTypeCtxt
= ...
 ThBrackCtxt  Template Haskell type brackets [t ... ]
 ...
```
However, this does not appear to actually be used anywhere and can be removed relatively easily:
<details>
```diff
diff git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs
index 3a1ab09c9b..e81a87c3a8 100644
 a/compiler/GHC/Tc/Gen/HsType.hs
+++ b/compiler/GHC/Tc/Gen/HsType.hs
@@ 2831,7 +2831,6 @@ expectedKindInCtxt :: UserTypeCtxt > ContextKind
 Depending on the context, we might accept any kind (for instance, in a TH
 splice), or only certain kinds (like in type signatures).
expectedKindInCtxt (TySynCtxt _) = AnyKind
expectedKindInCtxt ThBrackCtxt = AnyKind
expectedKindInCtxt (GhciCtxt {}) = AnyKind
 The types in a 'default' decl can have varying kinds
 See Note [Extended defaults]" in GHC.Tc.Utils.Env
diff git a/compiler/GHC/Tc/Types/Origin.hs b/compiler/GHC/Tc/Types/Origin.hs
index b2fdefa4cd..cc63f7a5c5 100644
 a/compiler/GHC/Tc/Types/Origin.hs
+++ b/compiler/GHC/Tc/Types/Origin.hs
@@ 92,7 +92,6 @@ data UserTypeCtxt
 True: standalone deriving
 False: vanilla instance declaration
 SpecInstCtxt  SPECIALISE instance pragma
  ThBrackCtxt  Template Haskell type brackets [t ... ]
 GenSigCtxt  Higherrank or impredicative situations
 e.g. (f e) where f has a higherrank type
 We might want to elaborate this
@@ 136,7 +135,6 @@ pprUserTypeCtxt (StandaloneKindSigCtxt n) = text "a standalone kind signature fo
pprUserTypeCtxt TypeAppCtxt = text "a type argument"
pprUserTypeCtxt (ConArgCtxt c) = text "the type of the constructor" <+> quotes (ppr c)
pprUserTypeCtxt (TySynCtxt c) = text "the RHS of the type synonym" <+> quotes (ppr c)
pprUserTypeCtxt ThBrackCtxt = text "a Template Haskell quotation [t...]"
pprUserTypeCtxt PatSigCtxt = text "a pattern type signature"
pprUserTypeCtxt ResSigCtxt = text "a result type signature"
pprUserTypeCtxt (ForSigCtxt n) = text "the foreign declaration for" <+> quotes (ppr n)
diff git a/compiler/GHC/Tc/Validity.hs b/compiler/GHC/Tc/Validity.hs
index fba45562b7..05dcb28643 100644
 a/compiler/GHC/Tc/Validity.hs
+++ b/compiler/GHC/Tc/Validity.hs
@@ 372,7 +372,6 @@ checkValidType ctxt ty
ForSigCtxt _ > rank1
SpecInstCtxt > rank1
 ThBrackCtxt > rank1
GhciCtxt {} > ArbitraryRank
TyVarBndrKindCtxt _ > rank0
@@ 500,7 +499,6 @@ vdqAllowed :: UserTypeCtxt > Bool
vdqAllowed (KindSigCtxt {}) = True
vdqAllowed (StandaloneKindSigCtxt {}) = True
vdqAllowed (TySynCtxt {}) = True
vdqAllowed (ThBrackCtxt {}) = True
vdqAllowed (GhciCtxt {}) = True
vdqAllowed (TyVarBndrKindCtxt {}) = True
vdqAllowed (DataKindCtxt {}) = True
@@ 1333,7 +1331,6 @@ okIPCtxt ResSigCtxt = True
okIPCtxt GenSigCtxt = True
okIPCtxt (ConArgCtxt {}) = True
okIPCtxt (ForSigCtxt {}) = True  ??
okIPCtxt ThBrackCtxt = True
okIPCtxt (GhciCtxt {}) = True
okIPCtxt SigmaCtxt = True
okIPCtxt (DataTyCtxt {}) = True
```
</details>
Is there a good reason to keep this around?The [`UserTypeCtxt`](https://gitlab.haskell.org/ghc/ghc//blob/a1f34d37b47826e86343e368a5c00f1a4b1f2bce/compiler/GHC/Tc/Types/Origin.hs#L5792) data type defines a context for TH brackets:
```hs
data UserTypeCtxt
= ...
 ThBrackCtxt  Template Haskell type brackets [t ... ]
 ...
```
However, this does not appear to actually be used anywhere and can be removed relatively easily:
<details>
```diff
diff git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs
index 3a1ab09c9b..e81a87c3a8 100644
 a/compiler/GHC/Tc/Gen/HsType.hs
+++ b/compiler/GHC/Tc/Gen/HsType.hs
@@ 2831,7 +2831,6 @@ expectedKindInCtxt :: UserTypeCtxt > ContextKind
 Depending on the context, we might accept any kind (for instance, in a TH
 splice), or only certain kinds (like in type signatures).
expectedKindInCtxt (TySynCtxt _) = AnyKind
expectedKindInCtxt ThBrackCtxt = AnyKind
expectedKindInCtxt (GhciCtxt {}) = AnyKind
 The types in a 'default' decl can have varying kinds
 See Note [Extended defaults]" in GHC.Tc.Utils.Env
diff git a/compiler/GHC/Tc/Types/Origin.hs b/compiler/GHC/Tc/Types/Origin.hs
index b2fdefa4cd..cc63f7a5c5 100644
 a/compiler/GHC/Tc/Types/Origin.hs
+++ b/compiler/GHC/Tc/Types/Origin.hs
@@ 92,7 +92,6 @@ data UserTypeCtxt
 True: standalone deriving
 False: vanilla instance declaration
 SpecInstCtxt  SPECIALISE instance pragma
  ThBrackCtxt  Template Haskell type brackets [t ... ]
 GenSigCtxt  Higherrank or impredicative situations
 e.g. (f e) where f has a higherrank type
 We might want to elaborate this
@@ 136,7 +135,6 @@ pprUserTypeCtxt (StandaloneKindSigCtxt n) = text "a standalone kind signature fo
pprUserTypeCtxt TypeAppCtxt = text "a type argument"
pprUserTypeCtxt (ConArgCtxt c) = text "the type of the constructor" <+> quotes (ppr c)
pprUserTypeCtxt (TySynCtxt c) = text "the RHS of the type synonym" <+> quotes (ppr c)
pprUserTypeCtxt ThBrackCtxt = text "a Template Haskell quotation [t...]"
pprUserTypeCtxt PatSigCtxt = text "a pattern type signature"
pprUserTypeCtxt ResSigCtxt = text "a result type signature"
pprUserTypeCtxt (ForSigCtxt n) = text "the foreign declaration for" <+> quotes (ppr n)
diff git a/compiler/GHC/Tc/Validity.hs b/compiler/GHC/Tc/Validity.hs
index fba45562b7..05dcb28643 100644
 a/compiler/GHC/Tc/Validity.hs
+++ b/compiler/GHC/Tc/Validity.hs
@@ 372,7 +372,6 @@ checkValidType ctxt ty
ForSigCtxt _ > rank1
SpecInstCtxt > rank1
 ThBrackCtxt > rank1
GhciCtxt {} > ArbitraryRank
TyVarBndrKindCtxt _ > rank0
@@ 500,7 +499,6 @@ vdqAllowed :: UserTypeCtxt > Bool
vdqAllowed (KindSigCtxt {}) = True
vdqAllowed (StandaloneKindSigCtxt {}) = True
vdqAllowed (TySynCtxt {}) = True
vdqAllowed (ThBrackCtxt {}) = True
vdqAllowed (GhciCtxt {}) = True
vdqAllowed (TyVarBndrKindCtxt {}) = True
vdqAllowed (DataKindCtxt {}) = True
@@ 1333,7 +1331,6 @@ okIPCtxt ResSigCtxt = True
okIPCtxt GenSigCtxt = True
okIPCtxt (ConArgCtxt {}) = True
okIPCtxt (ForSigCtxt {}) = True  ??
okIPCtxt ThBrackCtxt = True
okIPCtxt (GhciCtxt {}) = True
okIPCtxt SigmaCtxt = True
okIPCtxt (DataTyCtxt {}) = True
```
</details>
Is there a good reason to keep this around?https://gitlab.haskell.org/ghc/ghc//issues/18704GHC could not deduce constraint from itself20200930T21:23:04ZrybochodonezzarGHC could not deduce constraint from itself## Summary
following code:
```haskell
{# LANGUAGE GADTs, DataKinds, PolyKinds, ConstraintKinds, TypeApplications, RankNTypes, TypeFamilies, TypeOperators, MultiParamTypeClasses, UndecidableSuperClasses, FlexibleInstances, PatternSynonyms, FlexibleContexts, AllowAmbiguousTypes, ScopedTypeVariables #}
module Lib where
import GHC.Exts
import GHC.TypeLits
import Data.Proxy
data a ::: b = a ::: b
class Pair f where
type Left f :: a
type Right f :: b
instance Pair (a '::: b) where
type Left (a '::: b) = a
type Right (a '::: b) = b
class NC (x :: k)
instance NC (x :: k)
data L1 c f xs where
LC :: c x => f x > L1 c f xs > L1 c f (x ': xs)
LN :: L1 c f '[]
class (c1 (Left f), c2 (Right f)) => PairC c1 c2 f
instance (c1 x, c2 y) => PairC c1 c2 (x '::: y)
data f1 :*: f2 :: (kx ::: ky) > * where
(:*:) :: f1 x > f2 y > (f1 :*: f2) (x '::: y)
pairC :: forall c1 c2 x y e . (c1 x, c2 y) => (PairC c1 c2 (x '::: y) => e) > e
pairC e = e
type Foo t = L1 (PairC KnownSymbol NC) (Proxy :*: t)
pattern Foo :: forall s a t xs . KnownSymbol s => KnownSymbol s => Proxy s > t a > Foo t xs > Foo t (s '::: a ': xs)
pattern Foo p t xs < LC (p :*: t) xs where
Foo p t xs = pairC @KnownSymbol @NC @s @a (LC (p :*: t) xs)
```
Results in this compile error:
```
/home/ryba/ghcbug/src/Lib.hs:38:46: error:
• Could not deduce (PairC KnownSymbol NC (s '::: a))
arising from a use of ‘LC’
from the context: KnownSymbol s
bound by the signature for pattern synonym ‘Foo’
at src/Lib.hs:(37,1)(38,61)
or from: PairC KnownSymbol NC (s '::: a)
bound by a type expected by the context:
PairC KnownSymbol NC (s '::: a) =>
L1 (PairC KnownSymbol NC) (Proxy :*: t) ((s '::: a) : xs)
at src/Lib.hs:38:4561
• In the fifth argument of ‘pairC’, namely ‘(LC (p :*: t) xs)’
In the expression: pairC @KnownSymbol @NC @s @a (LC (p :*: t) xs)
In an equation for ‘Foo’:
Foo p t xs = pairC @KnownSymbol @NC @s @a (LC (p :*: t) xs)

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

38  Foo p t xs = pairC @KnownSymbol @NC @s @a (LC (p :*: t) xs)
 ^^^^^^^^^^^^^^^
```
Which basically boils down to "could not deduce a from a"
## Environment
* GHC version used: 8.10.2
* stack resolver=nightly20200914
Optional:
* Operating System: Ubuntu
* System Architecture: x8664https://gitlab.haskell.org/ghc/ghc//issues/18689Why check for fdefertypeerrors in metaTyVarUpdateOK?20201222T13:22:39ZRichard Eisenbergrae@richarde.devWhy check for fdefertypeerrors in metaTyVarUpdateOK?Function `checkTypeEq` changes its behavior depending on the presence of `fdefertypeerrors` in an obscure case around heterogeneous equalities; see the code in `go_co`. This is undocumented (in the code), and neither Simon nor I can figure out why it's done.
Task: figure this out, and either document or remove this behavior.Function `checkTypeEq` changes its behavior depending on the presence of `fdefertypeerrors` in an obscure case around heterogeneous equalities; see the code in `go_co`. This is undocumented (in the code), and neither Simon nor I can figure out why it's done.
Task: figure this out, and either document or remove this behavior.Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/18645Incremental `tcCheckSatisfiability` API20200914T13:16:06ZSebastian GrafIncremental `tcCheckSatisfiability` APIThe patternmatch checker makes use of the function `tcCheckSatisfiability :: Bag EvVar > TcM Bool` (henceforth `tcCS`) offered by the typechecker to solve type constraints. Over the course of a patternmatch checking session, such a `Bag EvVar` is accumulated and incrementally checked after each addition. As #17836 shows in a rather painful way, that scales quadratically, because the typechecker chews through the same type constraints over and over again.
But look at how the patternmatch checker uses `tcCS`:
```hs
  Add some extra type constraints to the 'TyState'; return 'Nothing' if we
 find a contradiction (e.g. @Int ~ Bool@).
tyOracle :: TyState > Bag PredType > DsM (Maybe TyState)
tyOracle (TySt inert) cts
= do { evs < traverse nameTyCt cts
; let new_inert = inert `unionBags` evs
; ... < initTcDsForSolver $ tcCheckSatisfiability new_inert
; ... }
```
The `inert` set is a `Bag EvVar` for which *we already know they are compatible with each other*, as they were checked by `tcCS` in a previous call. Only `cts :: Bag PredType` are unchecked. And as far as the patternmatch checker is concerned, the type of `inert` is completely opaque, so the API to `tcCS` could very well be
```hs
tcCheckSatisfiability :: TcInert > Bag EvVar > TcM (Maybe TcInert)
  Add some extra type constraints to the 'TyState'; return 'Nothing' if we
 find a contradiction (e.g. @Int ~ Bool@).
tyOracle :: TyState > Bag PredType > DsM (Maybe TyState)
tyOracle (TySt inert) cts
= do { evs < traverse nameTyCt cts
; ...mb_new_inert... < initTcDsForSolver $ tcCheckSatisfiability inert evs
; ... }
```
I'm sure there already is something like `TcInert` in the typechecker. Looking at the implementation of `tcCS`, that might be the unused `EvBindMap`, but I'm not sure. Or is it the `InertCans` in `getInertCans`/`setInertCans`? CC @rae, @RyanGlScott, @simonpj
This blocks #17836 and would probably lead to quite a few (possibly rather drastic) metric decreases in other cases.The patternmatch checker makes use of the function `tcCheckSatisfiability :: Bag EvVar > TcM Bool` (henceforth `tcCS`) offered by the typechecker to solve type constraints. Over the course of a patternmatch checking session, such a `Bag EvVar` is accumulated and incrementally checked after each addition. As #17836 shows in a rather painful way, that scales quadratically, because the typechecker chews through the same type constraints over and over again.
But look at how the patternmatch checker uses `tcCS`:
```hs
  Add some extra type constraints to the 'TyState'; return 'Nothing' if we
 find a contradiction (e.g. @Int ~ Bool@).
tyOracle :: TyState > Bag PredType > DsM (Maybe TyState)
tyOracle (TySt inert) cts
= do { evs < traverse nameTyCt cts
; let new_inert = inert `unionBags` evs
; ... < initTcDsForSolver $ tcCheckSatisfiability new_inert
; ... }
```
The `inert` set is a `Bag EvVar` for which *we already know they are compatible with each other*, as they were checked by `tcCS` in a previous call. Only `cts :: Bag PredType` are unchecked. And as far as the patternmatch checker is concerned, the type of `inert` is completely opaque, so the API to `tcCS` could very well be
```hs
tcCheckSatisfiability :: TcInert > Bag EvVar > TcM (Maybe TcInert)
  Add some extra type constraints to the 'TyState'; return 'Nothing' if we
 find a contradiction (e.g. @Int ~ Bool@).
tyOracle :: TyState > Bag PredType > DsM (Maybe TyState)
tyOracle (TySt inert) cts
= do { evs < traverse nameTyCt cts
; ...mb_new_inert... < initTcDsForSolver $ tcCheckSatisfiability inert evs
; ... }
```
I'm sure there already is something like `TcInert` in the typechecker. Looking at the implementation of `tcCS`, that might be the unused `EvBindMap`, but I'm not sure. Or is it the `InertCans` in `getInertCans`/`setInertCans`? CC @rae, @RyanGlScott, @simonpj
This blocks #17836 and would probably lead to quite a few (possibly rather drastic) metric decreases in other cases.https://gitlab.haskell.org/ghc/ghc//issues/18542Kind error when using partial type signatures20200806T21:34:14Zlennart@augustsson.netKind error when using partial type signatures## Summary
When using a partial type signature I get a kind error, which is surprising.
## Steps to reproduce
Compile the following module. The function bar type checks, whereas baz gets a kind error
```
{# LANGUAGE RankNTypes #}
module Bug where
foo :: (Functor g) =>
(forall aa . Num aa => f aa > g aa) >
f a > g (f a)
foo f x = undefined
bar :: (forall aa . Num aa => f aa > Int > aa) >
f a > Int > f a
bar f = foo f
baz :: (forall aa . Num aa => f aa > Int > aa) >
f a > _ > f a
baz f = foo f
```
## Environment
* GHC version used:
The Glorious Glasgow Haskell Compilation System, version 8.10.1## Summary
When using a partial type signature I get a kind error, which is surprising.
## Steps to reproduce
Compile the following module. The function bar type checks, whereas baz gets a kind error
```
{# LANGUAGE RankNTypes #}
module Bug where
foo :: (Functor g) =>
(forall aa . Num aa => f aa > g aa) >
f a > g (f a)
foo f x = undefined
bar :: (forall aa . Num aa => f aa > Int > aa) >
f a > Int > f a
bar f = foo f
baz :: (forall aa . Num aa => f aa > Int > aa) >
f a > _ > f a
baz f = foo f
```
## Environment
* GHC version used:
The Glorious Glasgow Haskell Compilation System, version 8.10.19.2.1