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

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

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

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

All this arose in #18148 and #18213, but is only tangentially related in the end.https://gitlab.haskell.org/ghc/ghc//issues/18196Type synonym lost with GADTs20200518T18:35:05ZIdentical SnowflakeType synonym lost with GADTsConsider the following:
```haskell
type Joules = Double
type Grams = Double
data Unit a where
Energy :: Unit Joules
Mass :: Unit Grams
test :: Unit a > a
test Energy = _
```
GHC reports the hole as `_ :: Double`, but I expected the synonym to remain intact, i.e., that the hole would be `_ :: Joules`.Consider the following:
```haskell
type Joules = Double
type Grams = Double
data Unit a where
Energy :: Unit Joules
Mass :: Unit Grams
test :: Unit a > a
test Energy = _
```
GHC reports the hole as `_ :: Double`, but I expected the synonym to remain intact, i.e., that the hole would be `_ :: Joules`.https://gitlab.haskell.org/ghc/ghc//issues/18151Etaexpansion of a leftsection20210112T23:04:49ZRichard Eisenbergrae@richarde.devEtaexpansion of a leftsectionIf I say
```hs
x = seq (True `undefined`) ()
```
what should I get when evaluating `x`?
According to my understanding of the Haskell Report, I should get `()`. And according to my understanding of GHC's source code (in `GHC.Tc.Gen.Expr`), I should get `()`. But I get an exception.
Why?
NB: `XPostfixOperators` is off. If it were on, the exception would be expected.
Spun off from https://github.com/ghcproposals/ghcproposals/pull/275#issuecomment624282022If I say
```hs
x = seq (True `undefined`) ()
```
what should I get when evaluating `x`?
According to my understanding of the Haskell Report, I should get `()`. And according to my understanding of GHC's source code (in `GHC.Tc.Gen.Expr`), I should get `()`. But I get an exception.
Why?
NB: `XPostfixOperators` is off. If it were on, the exception would be expected.
Spun off from https://github.com/ghcproposals/ghcproposals/pull/275#issuecomment6242820229.0.1Vladislav ZavialovVladislav Zavialovhttps://gitlab.haskell.org/ghc/ghc//issues/18073Outofdate commentary in Tc.Deriv.Infer20200423T03:49:06ZRichard Eisenbergrae@richarde.devOutofdate commentary in Tc.Deriv.InferCheck out https://gitlab.haskell.org/ghc/ghc//blob/15ab6cd548f284732a7f89d78c2b89b1bfc4ea1d/compiler/GHC/Tc/Deriv/Infer.hs#L805
* The commentary there talks about creating a variable `unsolved`, which does not seem to exist.
* In addition, the partition below creates `bad`, which is just ignored. Maybe this is right  I have not thought about it. But if it is right, it should be documented.
cc @RyanGlScottCheck out https://gitlab.haskell.org/ghc/ghc//blob/15ab6cd548f284732a7f89d78c2b89b1bfc4ea1d/compiler/GHC/Tc/Deriv/Infer.hs#L805
* The commentary there talks about creating a variable `unsolved`, which does not seem to exist.
* In addition, the partition below creates `bad`, which is just ignored. Maybe this is right  I have not thought about it. But if it is right, it should be documented.
cc @RyanGlScotthttps://gitlab.haskell.org/ghc/ghc//issues/18062A cast might get in the way of instantiation20200427T10:20:56ZSimon Peyton JonesA cast might get in the way of instantiationSuppose we have a type signature `f :: forall a. Eq a => blah`, and it somehow kindchecks to
```
forall a. ((Eq a => Blah) > co)
```
In principle this can happen:
```
tc_hs_type mode (HsQualTy { hst_ctxt = ctxt, hst_body = rn_ty }) exp_kind
= do { ctxt' < tc_hs_context mode ctxt
; ek < newOpenTypeKind  The body kind (result of the function) can
 be TYPE r, for any r, hence newOpenTypeKind
; ty' < tc_lhs_type mode rn_ty ek
; checkExpectedKind (unLoc rn_ty) (mkPhiTy ctxt' ty')
liftedTypeKind exp_kind }
```
That `checkExpectedKind` can add a cast.
If this happens, our instantiation mechanisms would fall over in a heap. We'd instantiate the `forall a`, but then fail to instantiate the `Eq a =>`; instead we'd unify `(Eq a => blah) > co` with the function body. Bad, bad.
This popped up when fixing #18008, when a missing zonk in `tcHsPartialSigType` was producing just such a forall (with a Refl coercion). But it seems plausible that it could happen for real.
EDIT: And it does:
```hs
{# LANGUAGE KindSignatures, TypeFamilies, DataKinds #}
module Bug where
import Data.Kind ( Type )
type family Star where
Star = Type
f :: ((Eq a => a > Bool) :: Star)
f x = x == x
```
produces
```
Bug.hs:11:1: error:
• Couldn't match kind ‘Constraint’ with ‘*’
When matching types
a0 :: *
Eq a :: Constraint
Expected type: Eq a => a > Bool
Actual type: a0 > Bool
• The equation(s) for ‘f’ have one argument,
but its type ‘Eq a => a > Bool’ has none
• Relevant bindings include
f :: Eq a => a > Bool (bound at Bug.hs:11:1)

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

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

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

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

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

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

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

:{
test :: IO ()
test = do
Pair X x < pure (Pair X [])
print (x /= [10])
:}
test
 True
 putting the code inside a function, also fixes inference??
:{
test1 :: IO (Pair X [])
test1 = pure (Pair X [])
test2 :: Pair X [] > IO ()
test2 (Pair X x) = print (x /= [10])
:}
test1 >>= test2
 True
 separating the functions also works, and we never hint x's type
```
</details>
</summary>
I think this is different from #2206 and #14065 since the error message here is a pretty generic "Couldn't match type" rather than the GADTspecific error messages in those tickets ("GADT pattern match with nonrigid result type", "untouchable inside the constraints"), and it only affects GHCi.
https://gitlab.haskell.org/ghc/ghc//issues/17955mkNewTyConRhs panic when trying to constrain newtype with Coercible20210123T06:44:33ZmatzemathicsmkNewTyConRhs panic when trying to constrain newtype with Coercible## Summary
The following code panics in ghc 8.8.3:
```haskell
{# LANGUAGE FlexibleContexts #}
import Data.Coerce
newtype T = Coercible () T => T ()
```
Error message:
```
[1 of 1] Compiling Main ( abug.hs, abug.o )
ghc: panic! (the 'impossible' happened)
(GHC version 8.8.3 for x86_64unknownlinux):
mkNewTyConRhs
T [Coercible () T, ()]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1159:37 in ghc:Outputable
pprPanic, called at compiler/iface/BuildTyCl.hs:65:27 in ghc:BuildTyCl
```
This seems to come from whatever is done to infer Coercible's instances.
Any other Constraint (weather or not using a multi parameter class) gives an error message:
```haskell
{# LANGUAGE FlexibleContexts #}
newtype T = Show T => T ()
```
results in:
```
[1 of 1] Compiling Main ( abug.hs, abug.o )
abug.hs:3:13: error:
* A newtype constructor cannot have a context in its type
T :: Show T => () > T
* In the definition of data constructor `T'
In the newtype declaration for `T'

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

3  newtype T = Show T => T ()
 ^^^^^^^^^^^^^^
```
## Expected behavior
Should most likely print an error message as in the second example.
## Environment
* GHC version used: 8.8.39.0.1https://gitlab.haskell.org/ghc/ghc//issues/17934Consider using specificity to disambiguate quantified constraints20210221T15:37:18ZRichard Eisenbergrae@richarde.devConsider using specificity to disambiguate quantified constraints**Summary:** Currently, quantified constraints shadow global instances. This ticket proposes to use specificity (in the sense used by overlapping instances) instead of shadowing.
**Motivation**
This looks like a sensible way of having a datatype that can store something of a type that supports some class interface:
```haskell
data Some (c :: Type > Constraint) where
Some :: c a => a > Some c
```
But now I want to write a `Show` instance. I can do this only when the existential `a` supports `Show`. But I don't wish to require that `c ~ Show`  maybe `c a` implies `Show a`. So I write this:
```haskell
instance (forall x . c x => Show x) => Show (Some c) where
showsPrec n (Some a) = showsPrec n a
```
But now this fails. The problem is that the instance gets expanded to
```haskell
instance (forall x . c x => Show x) => Show (Some c) where
showsPrec n (Some a) = showsPrec n a
show = $dmshow
```
where `$dmshow :: Show a => a > String` is the default method implementation for `show`. When typechecking this method, GHC needs to satisfy `Show (Some c)`. The context includes two possibilities: the quantified constraint, and the toplevel instance declaration. Because local instances (= quantified constraints) shadow global ones, we use the first. So we reduce `[W] Show (Some c)` to `[W] c (Some c)`, which cannot be solved, leading to disaster.
This example first came to light in https://gitlab.haskell.org/ghc/ghc/issues/16502#note_253501, where it was copied from #17794.
Taking this new approach will likely fix #16502 and allow the original program in #17202 to be accepted. See also https://gitlab.haskell.org/ghc/ghc/issues/16502#note_253501 and https://gitlab.haskell.org/ghc/ghc/issues/16502#note_259055 for more test cases.
**Background**:
The current instance lookup (as documented [here](https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#instancelookup)) works as follows to solve a `[W] C T` constraint (for some class `C` and type `T`).
1. Look for local (nonquantified) assumptions for `[G] C T`.
2. Look for local quantified constraints whose conclusions match `C T`. If exactly one matches, select the constraint. Then, check whether any quantified constraints *unify* with `C T` (allowing any variables in `C T` to be bound). If any do, abort, complaining about potential incoherence. Otherwise, reduce `[W] C T` to the premise of the quantified constraint.
3. Same as (2), but using the global instance table.
**Proposal**:
Use specificity to disambiguate.
* Let `<=spec` denote a partial order on instance heads. `C T1 <=spec C T2` iff there exists a substitution `S` such that `S(T2) = T1`  just as is used with overlapping instances today.
* Let metavariable `I` denote givens. These can be nonquantified, quantified (local), or global.
* Define `locality(I)` be a number that denotes how local `I` is. The locality of a nonquantified given is 1, of a quantified local given is 2, and of a global is 3.
* Define partial order `<=` on instances as follows:
1. If `I1 <=spec I2` and `I2 <=spec I1`, then `I1 <= I2` is `locality(I1) <= locality(I2)`.
2. If neither `I1 <=spec I2` nor `I2 <=spec I1`, then `I1 <= I2` is `locality(I1) <= locality(I2)`.
3. Otherwise, `I1 <= I2` if `I1 <=spec I2`.
Here is the proposed instance lookup procedure:
1. Collect all givens `I` (of all localities) that match a target. Call this set `Is`. If `Is` is empty, fail.
2. Let `I0` be the minimum element of `Is` with respect to `<=`. (Consider `Is` to be setlike, discarding duplicates.) If `I0` is not defined, fail.
3. Let `Is'` be the set `Is` excluding `I0`. Case on the locality of `I0`:
* `locality(I0) = 1`: Succeed with `I0` (skipping last check, below).
* `locality(I0) = 2`: Go on to next step if `Is'` contains only global instances. If `Is'` contains local instances, fail.
* `locality(I0) = 3`: Fail if any element in `Is'` is a local quantified instance. Go on to next step if, for every `I'` in `Is'`, either `I0` is *overlapping* or `I'` is *overlappable*.
4. Collect all givens (of all localities) that *unify* with a target, excluding those in `Is`. If `IncoherentInstances` is off and this set contains at least one instances not labeled **incoherent**, fail.
5. Succeed with `I0`.
**Discussion**:
This new algorithm is meant to replicate current behavior, except in the scenario where a global instance is more specific than a local one, in which the global instance should be selected. I have tried to capture current behavior w.r.t. incoherent and overlapping instances. In any case, if my algorithm deviates from current behavior w.r.t. incoherent or overlapping instances, this deviation is unintentional.
Another possible approach is to put local and global instances on even footing (that is, set both to have locality 2) but to allow users to explicitly label local instances as overlapping. I prefer the tiered approach above, but there's something simpler about local overlapping instances, in that it's one mechanism to think about.**Summary:** Currently, quantified constraints shadow global instances. This ticket proposes to use specificity (in the sense used by overlapping instances) instead of shadowing.
**Motivation**
This looks like a sensible way of having a datatype that can store something of a type that supports some class interface:
```haskell
data Some (c :: Type > Constraint) where
Some :: c a => a > Some c
```
But now I want to write a `Show` instance. I can do this only when the existential `a` supports `Show`. But I don't wish to require that `c ~ Show`  maybe `c a` implies `Show a`. So I write this:
```haskell
instance (forall x . c x => Show x) => Show (Some c) where
showsPrec n (Some a) = showsPrec n a
```
But now this fails. The problem is that the instance gets expanded to
```haskell
instance (forall x . c x => Show x) => Show (Some c) where
showsPrec n (Some a) = showsPrec n a
show = $dmshow
```
where `$dmshow :: Show a => a > String` is the default method implementation for `show`. When typechecking this method, GHC needs to satisfy `Show (Some c)`. The context includes two possibilities: the quantified constraint, and the toplevel instance declaration. Because local instances (= quantified constraints) shadow global ones, we use the first. So we reduce `[W] Show (Some c)` to `[W] c (Some c)`, which cannot be solved, leading to disaster.
This example first came to light in https://gitlab.haskell.org/ghc/ghc/issues/16502#note_253501, where it was copied from #17794.
Taking this new approach will likely fix #16502 and allow the original program in #17202 to be accepted. See also https://gitlab.haskell.org/ghc/ghc/issues/16502#note_253501 and https://gitlab.haskell.org/ghc/ghc/issues/16502#note_259055 for more test cases.
**Background**:
The current instance lookup (as documented [here](https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#instancelookup)) works as follows to solve a `[W] C T` constraint (for some class `C` and type `T`).
1. Look for local (nonquantified) assumptions for `[G] C T`.
2. Look for local quantified constraints whose conclusions match `C T`. If exactly one matches, select the constraint. Then, check whether any quantified constraints *unify* with `C T` (allowing any variables in `C T` to be bound). If any do, abort, complaining about potential incoherence. Otherwise, reduce `[W] C T` to the premise of the quantified constraint.
3. Same as (2), but using the global instance table.
**Proposal**:
Use specificity to disambiguate.
* Let `<=spec` denote a partial order on instance heads. `C T1 <=spec C T2` iff there exists a substitution `S` such that `S(T2) = T1`  just as is used with overlapping instances today.
* Let metavariable `I` denote givens. These can be nonquantified, quantified (local), or global.
* Define `locality(I)` be a number that denotes how local `I` is. The locality of a nonquantified given is 1, of a quantified local given is 2, and of a global is 3.
* Define partial order `<=` on instances as follows:
1. If `I1 <=spec I2` and `I2 <=spec I1`, then `I1 <= I2` is `locality(I1) <= locality(I2)`.
2. If neither `I1 <=spec I2` nor `I2 <=spec I1`, then `I1 <= I2` is `locality(I1) <= locality(I2)`.
3. Otherwise, `I1 <= I2` if `I1 <=spec I2`.
Here is the proposed instance lookup procedure:
1. Collect all givens `I` (of all localities) that match a target. Call this set `Is`. If `Is` is empty, fail.
2. Let `I0` be the minimum element of `Is` with respect to `<=`. (Consider `Is` to be setlike, discarding duplicates.) If `I0` is not defined, fail.
3. Let `Is'` be the set `Is` excluding `I0`. Case on the locality of `I0`:
* `locality(I0) = 1`: Succeed with `I0` (skipping last check, below).
* `locality(I0) = 2`: Go on to next step if `Is'` contains only global instances. If `Is'` contains local instances, fail.
* `locality(I0) = 3`: Fail if any element in `Is'` is a local quantified instance. Go on to next step if, for every `I'` in `Is'`, either `I0` is *overlapping* or `I'` is *overlappable*.
4. Collect all givens (of all localities) that *unify* with a target, excluding those in `Is`. If `IncoherentInstances` is off and this set contains at least one instances not labeled **incoherent**, fail.
5. Succeed with `I0`.
**Discussion**:
This new algorithm is meant to replicate current behavior, except in the scenario where a global instance is more specific than a local one, in which the global instance should be selected. I have tried to capture current behavior w.r.t. incoherent and overlapping instances. In any case, if my algorithm deviates from current behavior w.r.t. incoherent or overlapping instances, this deviation is unintentional.
Another possible approach is to put local and global instances on even footing (that is, set both to have locality 2) but to allow users to explicitly label local instances as overlapping. I prefer the tiered approach above, but there's something simpler about local overlapping instances, in that it's one mechanism to think about.https://gitlab.haskell.org/ghc/ghc//issues/17873Lazy instantiation is incompatible with implicit parameters20200715T09:06:16ZRichard Eisenbergrae@richarde.devLazy instantiation is incompatible with implicit parametersIn thinking about issues around #17173, I came up with this silliness:
```hs
getx :: (?x :: Bool > Bool) => Bool > Bool
getx = ?x
z3 = (let ?x = not in getx) False
```
GHC's current response is utter garbage:
```
Scratch.hs:52:23: error:
• Couldn't match type ‘?x::Bool > Bool’ with ‘Bool’
Expected type: Bool > Bool > Bool
Actual type: (?x::Bool > Bool) => Bool > Bool
• In the expression: getx
In the expression: let ?x = not in getx
In the expression: (let ?x = not in getx) False

52  z3 = (let ?x = not in getx) False

```
The "couldn't match type" bit is illkinded, and I have no idea why GHC is expecting `Bool > Bool > Bool` here. But the root cause, I believe, is lazy instantiation. Functions are instantiated lazily. So the `let ?x = not in getx` is instantiated lazily. The body of a `let` inherits its instantiation behavior from the outer context. So the `getx` is instantiated lazily. This means that GHC happily infers type `(?x :: Bool > Bool) => Bool > Bool` for `getx`. And then, with no incentive to instantiate, it infers `(let ?x = not in getx) :: (?x :: Bool > Bool) => Bool > Bool`. Now, when we apply such a thing to a term argument, GHC instantiates. But, lo!, there is no longer a `?x :: Bool > Bool` constraint in scope, causing unhappiness.
If we instantiate eagerly, I claim this should all work just fine.
I believe this will be fixed alongside #17173, but given that #17173 is about general improvement rather than bugfixing, I made this outright bug a separate ticket.In thinking about issues around #17173, I came up with this silliness:
```hs
getx :: (?x :: Bool > Bool) => Bool > Bool
getx = ?x
z3 = (let ?x = not in getx) False
```
GHC's current response is utter garbage:
```
Scratch.hs:52:23: error:
• Couldn't match type ‘?x::Bool > Bool’ with ‘Bool’
Expected type: Bool > Bool > Bool
Actual type: (?x::Bool > Bool) => Bool > Bool
• In the expression: getx
In the expression: let ?x = not in getx
In the expression: (let ?x = not in getx) False

52  z3 = (let ?x = not in getx) False

```
The "couldn't match type" bit is illkinded, and I have no idea why GHC is expecting `Bool > Bool > Bool` here. But the root cause, I believe, is lazy instantiation. Functions are instantiated lazily. So the `let ?x = not in getx` is instantiated lazily. The body of a `let` inherits its instantiation behavior from the outer context. So the `getx` is instantiated lazily. This means that GHC happily infers type `(?x :: Bool > Bool) => Bool > Bool` for `getx`. And then, with no incentive to instantiate, it infers `(let ?x = not in getx) :: (?x :: Bool > Bool) => Bool > Bool`. Now, when we apply such a thing to a term argument, GHC instantiates. But, lo!, there is no longer a `?x :: Bool > Bool` constraint in scope, causing unhappiness.
If we instantiate eagerly, I claim this should all work just fine.
I believe this will be fixed alongside #17173, but given that #17173 is about general improvement rather than bugfixing, I made this outright bug a separate ticket.https://gitlab.haskell.org/ghc/ghc//issues/17841"No skolem info" panic with PolyKinds20201019T09:16:46ZJakob Brünker"No skolem info" panic with PolyKinds## Summary
Making a class with a kindpolymorphic parameter and a single method can lead to a GHC panic stating "No skolem info".
## Steps to reproduce
The following program
```haskell
{# LANGUAGE PolyKinds #}
data Proxy a = Proxy
class Foo (t :: k) where foo :: Proxy (a :: t)
```
results in the error
```
Bug.hs:5:40: error:ghc: panic! (the 'impossible' happened)
(GHC version 8.11.0.20200215:
No skolem info:
[k_a1q3[sk:1]]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1187:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcErrors.hs:2793:17 in ghc:TcErrors
```
On 8.6.5, it instead emits the error message
```
Bug.hs:5:45: error:
• Expected a type, but ‘t’ has kind ‘k’
• In the kind ‘t’
In the first argument of ‘Proxy’, namely ‘(a :: t)’
In the type signature: foo :: Proxy (a :: t)

5  class Foo (t :: k) where foo :: Proxy (a :: t)

```
I thought at first it might be https://gitlab.haskell.org/ghc/ghc/issues/16245 but for the facts that that issue specifically mentions RankNTypes, and produces an error already on GHC 8.6, which this example doesn't.
## Expected behavior
It should probably emit the same error message it emitted in 8.6.
## Environment
* GHC versions used: 8.8.1, HEAD
* Does *not* happen on 8.6.5
Optional:
* Operating System: linux
* System Architecture: x86_64## Summary
Making a class with a kindpolymorphic parameter and a single method can lead to a GHC panic stating "No skolem info".
## Steps to reproduce
The following program
```haskell
{# LANGUAGE PolyKinds #}
data Proxy a = Proxy
class Foo (t :: k) where foo :: Proxy (a :: t)
```
results in the error
```
Bug.hs:5:40: error:ghc: panic! (the 'impossible' happened)
(GHC version 8.11.0.20200215:
No skolem info:
[k_a1q3[sk:1]]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1187:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcErrors.hs:2793:17 in ghc:TcErrors
```
On 8.6.5, it instead emits the error message
```
Bug.hs:5:45: error:
• Expected a type, but ‘t’ has kind ‘k’
• In the kind ‘t’
In the first argument of ‘Proxy’, namely ‘(a :: t)’
In the type signature: foo :: Proxy (a :: t)

5  class Foo (t :: k) where foo :: Proxy (a :: t)

```
I thought at first it might be https://gitlab.haskell.org/ghc/ghc/issues/16245 but for the facts that that issue specifically mentions RankNTypes, and produces an error already on GHC 8.6, which this example doesn't.
## Expected behavior
It should probably emit the same error message it emitted in 8.6.
## Environment
* GHC versions used: 8.8.1, HEAD
* Does *not* happen on 8.6.5
Optional:
* Operating System: linux
* System Architecture: x86_648.10.2https://gitlab.haskell.org/ghc/ghc//issues/17827Deduplicate overlapping Notes [TyVar/TyVar orientation] in TcUnify and [Canon...20200214T16:54:11ZRichard Eisenbergrae@richarde.devDeduplicate overlapping Notes [TyVar/TyVar orientation] in TcUnify and [Canonical orientation for tyvar/tyvar equality constraints] in TcCanonicalThese Notes cover similar ground but say different things.These Notes cover similar ground but say different things.https://gitlab.haskell.org/ghc/ghc//issues/17790`case` needn't instantiate its scrutinee20200205T15:31:19ZRichard Eisenbergrae@richarde.dev`case` needn't instantiate its scrutineeConsider
```hs
foo = case id of id' > (id' 'x', id' True)
```
Should this be accepted or rejected? GHC currently rejects. But simply by changing [this line](https://gitlab.haskell.org/ghc/ghc/blob/4bada77d5882974514d85d4bd0fd4e1801dad755/compiler/typecheck/TcExpr.hs#L528) to use `tcInferSigma` instead of `tcInferRho`, the program is accepted. (That's really it! Try it at home!)
Should we make this change? It makes our language more expressive. It also gets us closer to the Platonic ideal of a HindleyMilner language design, in that users should never have to think about instantiation or generalization. And ML does it. If I write
```ml
let ex = match fun x > x with
 f > (f 'x', f true)
```
then `ocamlc` accepts without complaint. Actually, this ML example is even more interesting: not only does it *preserve* the polymorphism in the scrutinee, it actually *generalizes*. Really, if Damas and Milner had been examining a language with `case`, they would have said that we need generalization at `let` and at `case`.
Of course, we could use `tcInferSigma` (enabling the Haskell example) but not to generalization. That means that `foo` would be accepted, but this `bar` would be rejected:
```hs
bar = case \x > x of id' > (id' 'x', id' True)
```
That's a bit of a shame.
This ticket is to track this small design decision.Consider
```hs
foo = case id of id' > (id' 'x', id' True)
```
Should this be accepted or rejected? GHC currently rejects. But simply by changing [this line](https://gitlab.haskell.org/ghc/ghc/blob/4bada77d5882974514d85d4bd0fd4e1801dad755/compiler/typecheck/TcExpr.hs#L528) to use `tcInferSigma` instead of `tcInferRho`, the program is accepted. (That's really it! Try it at home!)
Should we make this change? It makes our language more expressive. It also gets us closer to the Platonic ideal of a HindleyMilner language design, in that users should never have to think about instantiation or generalization. And ML does it. If I write
```ml
let ex = match fun x > x with
 f > (f 'x', f true)
```
then `ocamlc` accepts without complaint. Actually, this ML example is even more interesting: not only does it *preserve* the polymorphism in the scrutinee, it actually *generalizes*. Really, if Damas and Milner had been examining a language with `case`, they would have said that we need generalization at `let` and at `case`.
Of course, we could use `tcInferSigma` (enabling the Haskell example) but not to generalization. That means that `foo` would be accepted, but this `bar` would be rejected:
```hs
bar = case \x > x of id' > (id' 'x', id' True)
```
That's a bit of a shame.
This ticket is to track this small design decision.https://gitlab.haskell.org/ghc/ghc//issues/17789Instantiation doesn't look through dictionaries20200205T11:16:36ZRichard Eisenbergrae@richarde.devInstantiation doesn't look through dictionariesThe bug is simple to state in terms of GHC's implementation: `topInstantiate` does not look past dictionaries. Thus a type like `forall a. C a => forall b. ...` only gets its `a` instantiated, not its `b`. This can be witnessed is some uglylooking code:
```hs
data Rec a b = MkRec { x :: Bool }
class C a where
r :: Rec a b
instance C Int where
r = MkRec { x = True }
foo :: Rec Int Bool
foo = r { x = False }
```
This fails with
```
/Users/rae/temp/Bug.hs:10:7: error:
• Ambiguous type variable ‘a0’ arising from a use of ‘r’
prevents the constraint ‘(C a0)’ from being solved.
Probable fix: use a type annotation to specify what ‘a0’ should be.
These potential instance exist:
instance C Int  Defined at /Users/rae/temp/Bug.hs:6:10
• In the expression: r
In the expression: r {x = False}
In an equation for ‘foo’: foo = r {x = False}
```
I have no idea why it's an ambiguousvariable error, but let's not get distracted by that. The problem is that GHC does not instantiate `r` vigorously enough to notice that it's a record. The solution is straightforward: have `topInstantiate` be recursive, looking past dictionaries. `topInstantiate` is used in other places, too, and perhaps there are other similar bugs to find.The bug is simple to state in terms of GHC's implementation: `topInstantiate` does not look past dictionaries. Thus a type like `forall a. C a => forall b. ...` only gets its `a` instantiated, not its `b`. This can be witnessed is some uglylooking code:
```hs
data Rec a b = MkRec { x :: Bool }
class C a where
r :: Rec a b
instance C Int where
r = MkRec { x = True }
foo :: Rec Int Bool
foo = r { x = False }
```
This fails with
```
/Users/rae/temp/Bug.hs:10:7: error:
• Ambiguous type variable ‘a0’ arising from a use of ‘r’
prevents the constraint ‘(C a0)’ from being solved.
Probable fix: use a type annotation to specify what ‘a0’ should be.
These potential instance exist:
instance C Int  Defined at /Users/rae/temp/Bug.hs:6:10
• In the expression: r
In the expression: r {x = False}
In an equation for ‘foo’: foo = r {x = False}
```
I have no idea why it's an ambiguousvariable error, but let's not get distracted by that. The problem is that GHC does not instantiate `r` vigorously enough to notice that it's a record. The solution is straightforward: have `topInstantiate` be recursive, looking past dictionaries. `topInstantiate` is used in other places, too, and perhaps there are other similar bugs to find.https://gitlab.haskell.org/ghc/ghc//issues/17772CUSKless class typechecks on 8.4, but not on 8.6+20200608T10:56:41ZRyan ScottCUSKless class typechecks on 8.4, but not on 8.6+This code will typecheck with GHC 8.0.2 through 8.4.4:
```hs
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
module Bug where
import Data.Kind
import Data.Proxy
class C f where
type T (x :: f a) :: Type
sT :: forall a (x :: f a).
Proxy x > T x
```
However, it mysteriously _does_ not typecheck on GHC 8.6.5 or later:
```
$ /opt/ghc/8.8.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:13:22: error:
• Expected kind ‘f a’, but ‘x’ has kind ‘f a1’
• In the first argument of ‘T’, namely ‘x’
In the type signature: sT :: forall a (x :: f a). Proxy x > T x
In the class declaration for ‘C’

13  Proxy x > T x
 ^
```
I cannot think of a good reason why this shouldn't typecheck, especially since there appears to be no polymorphic recursion happening in `C`, `T`, or `sT`.
Some observations:
* Giving `C` a CUSK (i.e., `class C (f :: k > Type) where ...`) makes it typecheck:
* Splitting up `C` into two classes like so also makes it typecheck:
```hs
class C1 f where
type T (x :: f a) :: Type
class C2 f where
sT :: forall a (x :: f a).
Proxy x > T x
```This code will typecheck with GHC 8.0.2 through 8.4.4:
```hs
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
module Bug where
import Data.Kind
import Data.Proxy
class C f where
type T (x :: f a) :: Type
sT :: forall a (x :: f a).
Proxy x > T x
```
However, it mysteriously _does_ not typecheck on GHC 8.6.5 or later:
```
$ /opt/ghc/8.8.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:13:22: error:
• Expected kind ‘f a’, but ‘x’ has kind ‘f a1’
• In the first argument of ‘T’, namely ‘x’
In the type signature: sT :: forall a (x :: f a). Proxy x > T x
In the class declaration for ‘C’

13  Proxy x > T x
 ^
```
I cannot think of a good reason why this shouldn't typecheck, especially since there appears to be no polymorphic recursion happening in `C`, `T`, or `sT`.
Some observations:
* Giving `C` a CUSK (i.e., `class C (f :: k > Type) where ...`) makes it typecheck:
* Splitting up `C` into two classes like so also makes it typecheck:
```hs
class C1 f where
type T (x :: f a) :: Type
class C2 f where
sT :: forall a (x :: f a).
Proxy x > T x
```https://gitlab.haskell.org/ghc/ghc//issues/17737Recursive superclass check is defeated by quantified constraints20200310T14:21:59ZRichard Eisenbergrae@richarde.devRecursive superclass check is defeated by quantified constraintsThis is accepted:
```hs
{# LANGUAGE QuantifiedConstraints, KindSignatures, ConstraintKinds #}
module Bug where
import Data.Kind
class ((() :: Constraint) => C a) => C a
```
The vacuous constraint `()` hides the recursive superclass `C a`. Note that I do not have `RecursiveSuperclasses` enabled.
The culprit is `TcTyDecls.checkClassCycles`.
This is not a "real" bug report, in that I found the problem only by reading the source code, not by observing the misbehavior. Still, it shouldn't be hard to fix. Should we just look through quantified constraints always?This is accepted:
```hs
{# LANGUAGE QuantifiedConstraints, KindSignatures, ConstraintKinds #}
module Bug where
import Data.Kind
class ((() :: Constraint) => C a) => C a
```
The vacuous constraint `()` hides the recursive superclass `C a`. Note that I do not have `RecursiveSuperclasses` enabled.
The culprit is `TcTyDecls.checkClassCycles`.
This is not a "real" bug report, in that I found the problem only by reading the source code, not by observing the misbehavior. Still, it shouldn't be hard to fix. Should we just look through quantified constraints always?Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/17719Note [Do not add duplicate quantified instances] is simplistic, causing rejec...20200714T19:14:38ZRichard Eisenbergrae@richarde.devNote [Do not add duplicate quantified instances] is simplistic, causing rejection of programsCopied wholesale from https://gitlab.haskell.org/ghc/ghc/merge_requests/2283#note_242042:
Consider
```haskell
{# LANGUAGE QuantifiedConstraints, ConstraintKinds,
ExistentialQuantification #}
module Bug where
class C1 a
class (forall z. C1 z) => C2 y
class (forall y. C2 y) => C3 x
data Dict c = c => Dict
foo :: (C2 a, C3 a) => a > Dict (C1 a)
foo _ = Dict
```
Amazingly, with *either* `C2 a` or `C3 a`, `foo` is accepted. But with both, it is rejected.
The problem is that, after eagerly expanding superclasses of quantified constraints (that's the new bit), we end up with
```
[G] g1 :: forall z. C1 z  from the C2 a constraint
[G] g2 :: forall y z. C1 z  from the C3 a constraint
```
So when we want to solve `C1 a`, we don't know which quantified constraint to use, and so we stop. (Also strange: `g2` is quantified over the unused `y`. It's clear where this comes from, and it seems harmless, but it's a bit strange. This detail is *not* salient. It is *not* the reason we're struggling here.) This has been seen before, in another guise: #15244. And we have
```
{ Note [Do not add duplicate quantified instances]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider this (#15244):
f :: (C g, D g) => ....
class S g => C g where ...
class S g => D g where ...
class (forall a. Eq a => Eq (g a)) => S g where ...
Then in f's RHS there are two identical quantified constraints
available, one via the superclasses of C and one via the superclasses
of D. The two are identical, and it seems wrong to reject the program
because of that. But without doing duplicateelimination we will have
two matching QCInsts when we try to solve constraints arising from f's
RHS.
The simplest thing is simply to eliminate duplicates, which we do here.
}
```
which is duly implemented. However, here, we don't have duplicates  we have nearduplicates, which are not caught by the simple (`tcEqType`) check.
I wonder if the way forward is to really try to "solve" quantified instances. That is, before labeling them inert, we try to interact them with inerts. Then, we might discover that one constraint is implied by another, which will get rid of this problem (and replace that Note).Copied wholesale from https://gitlab.haskell.org/ghc/ghc/merge_requests/2283#note_242042:
Consider
```haskell
{# LANGUAGE QuantifiedConstraints, ConstraintKinds,
ExistentialQuantification #}
module Bug where
class C1 a
class (forall z. C1 z) => C2 y
class (forall y. C2 y) => C3 x
data Dict c = c => Dict
foo :: (C2 a, C3 a) => a > Dict (C1 a)
foo _ = Dict
```
Amazingly, with *either* `C2 a` or `C3 a`, `foo` is accepted. But with both, it is rejected.
The problem is that, after eagerly expanding superclasses of quantified constraints (that's the new bit), we end up with
```
[G] g1 :: forall z. C1 z  from the C2 a constraint
[G] g2 :: forall y z. C1 z  from the C3 a constraint
```
So when we want to solve `C1 a`, we don't know which quantified constraint to use, and so we stop. (Also strange: `g2` is quantified over the unused `y`. It's clear where this comes from, and it seems harmless, but it's a bit strange. This detail is *not* salient. It is *not* the reason we're struggling here.) This has been seen before, in another guise: #15244. And we have
```
{ Note [Do not add duplicate quantified instances]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider this (#15244):
f :: (C g, D g) => ....
class S g => C g where ...
class S g => D g where ...
class (forall a. Eq a => Eq (g a)) => S g where ...
Then in f's RHS there are two identical quantified constraints
available, one via the superclasses of C and one via the superclasses
of D. The two are identical, and it seems wrong to reject the program
because of that. But without doing duplicateelimination we will have
two matching QCInsts when we try to solve constraints arising from f's
RHS.
The simplest thing is simply to eliminate duplicates, which we do here.
}
```
which is duly implemented. However, here, we don't have duplicates  we have nearduplicates, which are not caught by the simple (`tcEqType`) check.
I wonder if the way forward is to really try to "solve" quantified instances. That is, before labeling them inert, we try to interact them with inerts. Then, we might discover that one constraint is implied by another, which will get rid of this problem (and replace that Note).https://gitlab.haskell.org/ghc/ghc//issues/17718Refactor solver to leave breadcrumbs20200120T21:32:21ZRichard Eisenbergrae@richarde.devRefactor solver to leave breadcrumbsToday, the solver works hard to find how givens can imply wanteds. If it fails, it exits with unsolved wanteds. These wanteds are then scrutinized carefully in the TcErrors module in order to produce nice, userreadable error messages. However, the current design means that TcErrors needs to do much work trying to analyze the tea leaves that the solver has left behind. That is, it must reconstruct *why* a constraint was failed to be solved. This involves some duplicate code and duplicate work (such as looking in instance environments).
Instead, we can imagine a structure, stored within a `CtLoc`, that records the solver's movements, including movements it failed to make (such as "tried to unify, but hit an occurscheck failure"). This structure could then be consumed in TcErrors. Effectively, this means that the solver could more directly communicate with users and explain its reasoning. We might also imagine a future where users can query GHC for information about even typecorrect programs.
This ticket is to track this refactoring opportunity.Today, the solver works hard to find how givens can imply wanteds. If it fails, it exits with unsolved wanteds. These wanteds are then scrutinized carefully in the TcErrors module in order to produce nice, userreadable error messages. However, the current design means that TcErrors needs to do much work trying to analyze the tea leaves that the solver has left behind. That is, it must reconstruct *why* a constraint was failed to be solved. This involves some duplicate code and duplicate work (such as looking in instance environments).
Instead, we can imagine a structure, stored within a `CtLoc`, that records the solver's movements, including movements it failed to make (such as "tried to unify, but hit an occurscheck failure"). This structure could then be consumed in TcErrors. Effectively, this means that the solver could more directly communicate with users and explain its reasoning. We might also imagine a future where users can query GHC for information about even typecorrect programs.
This ticket is to track this refactoring opportunity.https://gitlab.haskell.org/ghc/ghc//issues/17717Refactor mapType/mapCoercion so that they inline20200323T13:53:00ZRichard Eisenbergrae@richarde.devRefactor mapType/mapCoercion so that they inline`mapType` and `mapCoercion` are very convenient functions for writing transformations over types and coercions. But they current don't inline properly, meaning that the `TyCoMapper` that describes their behavior is not inlined, and thus preventing other optimizations.
Instead, they should be refactored to be like https://gitlab.haskell.org/ghc/ghc/blob/wip/T17509/compiler/types/TyCoRep.hs#L1742, where we have carefully ensured that similar functions inline.
Main work done in #!2683.
Remaining task: use `mapType` more!`mapType` and `mapCoercion` are very convenient functions for writing transformations over types and coercions. But they current don't inline properly, meaning that the `TyCoMapper` that describes their behavior is not inlined, and thus preventing other optimizations.
Instead, they should be refactored to be like https://gitlab.haskell.org/ghc/ghc/blob/wip/T17509/compiler/types/TyCoRep.hs#L1742, where we have carefully ensured that similar functions inline.
Main work done in #!2683.
Remaining task: use `mapType` more!https://gitlab.haskell.org/ghc/ghc//issues/17710Polykinded rewrite rule fails to typecheck (HEAD only)20200315T18:51:16ZRyan ScottPolykinded rewrite rule fails to typecheck (HEAD only)I originally noticed this issue since it prevents the `freealgebras0.0.8.1` library from building with HEAD (build log [here](https://gitlab.haskell.org/RyanGlScott/head.hackage//jobs/240129)). Here is a minimized example that demonstrates the issue:
```hs
{# LANGUAGE PolyKinds #}
{# LANGUAGE RankNTypes #}
module Bug where
import Data.Proxy
foo :: forall k (b :: k). (forall (a :: k). Proxy a > Proxy a) > Proxy b
foo g = g Proxy
{# INLINABLE [1] foo #}
{# RULES "foo" forall (g :: forall (a :: k). Proxy a > Proxy a). foo g = g Proxy #}
```
This typechecks on GHC 8.8.2 and 8.10.1alpha2, but on HEAD it fails to typecheck:
```
$ ~/Software/ghc5/inplace/bin/ghcstage2 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:10:11: error:
• Cannot generalise type; skolem ‘k’ would escape its scope
if I tried to quantify (b0 :: k) in this type:
forall k. Proxy @{k} b0
(Indeed, I sometimes struggle even printing this correctly,
due to its illscoped nature.)
• When checking the transformation rule "foo"

10  {# RULES "foo" forall (g :: forall (a :: k). Proxy a > Proxy a). foo g = g Proxy #}
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
Judging by the error message, this regression was likely introduced in commit 350e2b78788d47255d27489dfc62d664498b5de4 (`Don't zap to Any; error instead`). cc'ing @rae, the author of that commit.I originally noticed this issue since it prevents the `freealgebras0.0.8.1` library from building with HEAD (build log [here](https://gitlab.haskell.org/RyanGlScott/head.hackage//jobs/240129)). Here is a minimized example that demonstrates the issue:
```hs
{# LANGUAGE PolyKinds #}
{# LANGUAGE RankNTypes #}
module Bug where
import Data.Proxy
foo :: forall k (b :: k). (forall (a :: k). Proxy a > Proxy a) > Proxy b
foo g = g Proxy
{# INLINABLE [1] foo #}
{# RULES "foo" forall (g :: forall (a :: k). Proxy a > Proxy a). foo g = g Proxy #}
```
This typechecks on GHC 8.8.2 and 8.10.1alpha2, but on HEAD it fails to typecheck:
```
$ ~/Software/ghc5/inplace/bin/ghcstage2 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:10:11: error:
• Cannot generalise type; skolem ‘k’ would escape its scope
if I tried to quantify (b0 :: k) in this type:
forall k. Proxy @{k} b0
(Indeed, I sometimes struggle even printing this correctly,
due to its illscoped nature.)
• When checking the transformation rule "foo"

10  {# RULES "foo" forall (g :: forall (a :: k). Proxy a > Proxy a). foo g = g Proxy #}
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
Judging by the error message, this regression was likely introduced in commit 350e2b78788d47255d27489dfc62d664498b5de4 (`Don't zap to Any; error instead`). cc'ing @rae, the author of that commit.9.0.1https://gitlab.haskell.org/ghc/ghc//issues/17679Superclass expansion fails in instance declaration20200115T18:01:59ZRichard Eisenbergrae@richarde.devSuperclass expansion fails in instance declarationI'm sure I'm doing something very silly.
```hs
{# LANGUAGE FlexibleInstances, UndecidableInstances #}
module Bug where
class A a
class A a => B a
class A a => C a
instance B a => C a
```
GHC rejects, saying it can't prove `A a`, required in order to write the `C a` instance. But shouldn't my `B a` constraint imply `A a`?
Help?I'm sure I'm doing something very silly.
```hs
{# LANGUAGE FlexibleInstances, UndecidableInstances #}
module Bug where
class A a
class A a => B a
class A a => C a
instance B a => C a
```
GHC rejects, saying it can't prove `A a`, required in order to write the `C a` instance. But shouldn't my `B a` constraint imply `A a`?
Help?