GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2020-05-22T23:36:26Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/18220Improve Coercible under foralls2020-05-22T23: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 o...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 value-level 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 term-level 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 GADTs2021-10-17T13:38:04ZIdentical 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 ...Consider the following:
```haskell
type Joules = Double
type Grams = Double
data Unit a where
Energy :: Unit Joules
Mass :: Unit Grams
test :: Unit a -> a
test Energy = _
```
GHC reports the hole as `_ :: Double`, but I expected the synonym to remain intact, i.e., that the hole would be `_ :: Joules`.https://gitlab.haskell.org/ghc/ghc/-/issues/18062A cast might get in the way of instantiation2020-04-27T10: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 kind-checks to
```
forall a. ((Eq a => Blah) |> co)
```
In principle this can happen:
```
tc_hs_type mode (HsQualTy { hst_ctxt = ctxt, hst_body = rn_ty }) ...Suppose we have a type signature `f :: forall a. Eq a => blah`, and it somehow kind-checks 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 too-general type when pattern-matching on existential GADT2022-09-06T11:38:59Zinfinity0GHCi infers too-general type when pattern-matching on existential GADTRun the following in ghci, I tested with version 8.8.3:
<summary>
`ghci -ghci-script Test.hs`
<details>
```haskell
:set -XGADTs
:set -XScopedTypeVariables
-- standard GADT with restricted type param
data X a where X :: X Int; XB :: ...Run the following in ghci, I tested with version 8.8.3:
<summary>
`ghci -ghci-script 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 GADT-syntax 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 GADT-specific error messages in those tickets ("GADT pattern match with non-rigid result type", "untouchable inside the constraints"), and it only affects GHCi.https://gitlab.haskell.org/ghc/ghc/-/issues/17934Consider using specificity to disambiguate quantified constraints2021-02-21T15: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 ...**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 type-checking this method, GHC needs to satisfy `Show (Some c)`. The context includes two possibilities: the quantified constraint, and the top-level 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#instance-lookup)) works as follows to solve a `[W] C T` constraint (for some class `C` and type `T`).
1. Look for local (non-quantified) 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 non-quantified, quantified (local), or global.
* Define `locality(I)` be a number that denotes how local `I` is. The locality of a non-quantified 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 set-like, discarding duplicates.) If `I0` is not defined, fail.
3. Let `Is'` be the set `Is` excluding `I0`. Case on the locality of `I0`:
* `locality(I0) = 1`: Succeed with `I0` (skipping last check, below).
* `locality(I0) = 2`: Go on to next step if `Is'` contains only global instances. If `Is'` contains local instances, fail.
* `locality(I0) = 3`: Fail if any element in `Is'` is a local quantified instance. Go on to next step if, for every `I'` in `Is'`, either `I0` is *overlapping* or `I'` is *overlappable*.
4. Collect all givens (of all localities) that *unify* with a target, excluding those in `Is`. If `IncoherentInstances` is off and this set contains at least one instances not labeled **incoherent**, fail.
5. Succeed with `I0`.
**Discussion**:
This new algorithm is meant to replicate current behavior, except in the scenario where a global instance is more specific than a local one, in which the global instance should be selected. I have tried to capture current behavior w.r.t. incoherent and overlapping instances. In any case, if my algorithm deviates from current behavior w.r.t. incoherent or overlapping instances, this deviation is unintentional.
Another possible approach is to put local and global instances on even footing (that is, set both to have locality 2) but to allow users to explicitly label local instances as overlapping. I prefer the tiered approach above, but there's something simpler about local overlapping instances, in that it's one mechanism to think about.https://gitlab.haskell.org/ghc/ghc/-/issues/17790`case` needn't instantiate its scrutinee2020-02-05T15: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/4bada77d5882974514d85d4bd0fd4e1801dad...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 Hindley-Milner language design, in that users should never have to think about instantiation or generalization. And ML does it. If I write
```ml
let ex = match fun x -> x with
| f -> (f 'x', f true)
```
then `ocamlc` accepts without complaint. Actually, this ML example is even more interesting: not only does it *preserve* the polymorphism in the scrutinee, it actually *generalizes*. Really, if Damas and Milner had been examining a language with `case`, they would have said that we need generalization at `let` and at `case`.
Of course, we could use `tcInferSigma` (enabling the Haskell example) but not to generalization. That means that `foo` would be accepted, but this `bar` would be rejected:
```hs
bar = case \x -> x of id' -> (id' 'x', id' True)
```
That's a bit of a shame.
This ticket is to track this small design decision.https://gitlab.haskell.org/ghc/ghc/-/issues/17737Recursive superclass check is defeated by quantified constraints2020-03-10T14: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 superclas...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...2020-07-14T19: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...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 duplicate-elimination 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 near-duplicates, 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 breadcrumbs2023-06-30T15:06:13ZRichard 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, user-readable error messages. H...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, user-readable 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 occurs-check 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 type-correct programs.
This ticket is to track this refactoring opportunity.https://gitlab.haskell.org/ghc/ghc/-/issues/17717Refactor mapType/mapCoercion so that they inline2020-03-23T13: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 ...`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/17679Superclass expansion fails in instance declaration2020-01-15T18: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`, r...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?https://gitlab.haskell.org/ghc/ghc/-/issues/17644Loop in the constraint solver around variables free in kinds2020-01-20T18:20:09ZRichard Eisenbergrae@richarde.devLoop in the constraint solver around variables free in kindsSpun off from the bowels of #17323 (https://gitlab.haskell.org/ghc/ghc/issues/17323#note_243178, https://gitlab.haskell.org/ghc/ghc/issues/17323#note_243577, https://gitlab.haskell.org/ghc/ghc/issues/17323#note_244748), but I think ortho...Spun off from the bowels of #17323 (https://gitlab.haskell.org/ghc/ghc/issues/17323#note_243178, https://gitlab.haskell.org/ghc/ghc/issues/17323#note_243577, https://gitlab.haskell.org/ghc/ghc/issues/17323#note_244748), but I think orthogonal to that ticket. No need to read that ticket to understand this one.
Here is a simple form of the potential problem (due to @simonpj):
```
Inert set:
[G] b ~ a
Work item:
[G] (a :: *) ~ (c :: b -> *) (d :: b)
```
I think GHC will add that work item to the inert set, despite the fact that it seems loopy.
And in this example, I think we'll actually get a loop:
```
a :: e
b :: d -> e
c :: d
d :: Type
e :: Type
f :: e -> Type
g :: d -> Type
inert set:
[D] a ~ b c
[D] e ~ g c
[G] g1 :: d ~ f a -- just having `a` here would violate K3a of Note [Extending the inert equalities]
work item: [D] e ~ f a
```
Let's see what happens.
1. `can_eq_nc'` will get to its flattening clause, so both sides get flattened, yielding `[D] g c ~ f (b c)`.
2. `can_eq_nc'` then decomposes to `[D] g ~ f` and `[D] c ~ b c`. We'll continue here with the latter.
3. On the new work item `[D] c ~ b c`, `can_eq_nc'` will get to its flattening clause, so both sides get flattened, causing no change.
4. Then, we go to `canEqTyVar`. We have `c :: d` but `b c :: e`, so we flatten both kinds. We thus get `[D] (c |> g1) ~ b c`, where `g1 :: d ~ f a` comes from flattening. We then emit `[D] f a ~ e`. The first is irreducible, but the second brings us right back where we started. (Note that `e` isn't rewritten by flattening because the equality for `e` is a Derived, which cannot be used to rewrite a kind.)
[This comment](https://gitlab.haskell.org/ghc/ghc/issues/17644#note_245566) below shows `f8` which shows an actual loop from this case. Plus: the other examples there show cases where simply re-ordering the constraints in a type changes the accept/reject behaviour; this is Bad.https://gitlab.haskell.org/ghc/ghc/-/issues/17563Validity check quantified constraints2021-11-17T21:20:04ZRichard Eisenbergrae@richarde.devValidity check quantified constraintsThis module is accepted:
```hs
{-# LANGUAGE QuantifiedConstraints #-}
module Bug2 where
blah :: (forall a. a b ~ a c) => b -> c
blah = undefined
```
But it shouldn't be: it uses `~` with neither `GADTs` nor `TypeFamilies` enabled.This module is accepted:
```hs
{-# LANGUAGE QuantifiedConstraints #-}
module Bug2 where
blah :: (forall a. a b ~ a c) => b -> c
blah = undefined
```
But it shouldn't be: it uses `~` with neither `GADTs` nor `TypeFamilies` enabled.8.10.2https://gitlab.haskell.org/ghc/ghc/-/issues/17545Coercion variables appearing where they shouldn't2020-01-20T00:24:32ZKrzysztof GogolewskiCoercion variables appearing where they shouldn'tDuring review of !2268, we've discovered a few places where a coercion variable can appear where it shouldn't. Those are calls to "OrCoVar" functions in:
* [ ] `newLocal` in `MkId`
* [ ] `bindIfaceId` in `TcIface`
* [ ] `tcPatBndr` in `...During review of !2268, we've discovered a few places where a coercion variable can appear where it shouldn't. Those are calls to "OrCoVar" functions in:
* [ ] `newLocal` in `MkId`
* [ ] `bindIfaceId` in `TcIface`
* [ ] `tcPatBndr` in `TcPat`
that happen when running tests T13990 T14285 T15648.
The goal is to fix this, or come up with a convincing reason that a coercion makes sense there.https://gitlab.haskell.org/ghc/ghc/-/issues/17432Wildcards in standalone kind signatures2023-07-14T19:19:52ZRichard Eisenbergrae@richarde.devWildcards in standalone kind signaturesWe should allow partial kind signatures as well as partial type signatures:
```hs
type Maybe :: _ -> Type
data Maybe a = Nothing | Just a
type Proxy :: forall (k :: _). k -> _
data Proxy = MkP
```
Of course, this would mean that polym...We should allow partial kind signatures as well as partial type signatures:
```hs
type Maybe :: _ -> Type
data Maybe a = Nothing | Just a
type Proxy :: forall (k :: _). k -> _
data Proxy = MkP
```
Of course, this would mean that polymorphic recursion would not be allowed. It's all just like at the term level.https://gitlab.haskell.org/ghc/ghc/-/issues/17368Implement homogeneous equality2021-06-16T15:54:59ZRichard Eisenbergrae@richarde.devImplement homogeneous equalityAs observed in [two](https://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1076&context=compsci_pubs) [papers](https://richarde.dev/papers/2019/dep-roles/dep-roles.pdf), the primitive equality type in GHC can be made homogeneous. T...As observed in [two](https://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1076&context=compsci_pubs) [papers](https://richarde.dev/papers/2019/dep-roles/dep-roles.pdf), the primitive equality type in GHC can be made homogeneous. This is both a simplification over the status quo (heterogeneous equality) and an important step toward implementing dependent types.
This ticket is to track this change.
Step 1: Modify the type-checker to use predicates instead of types internally. This will essentially be a glorification of `PredTree` (renamed `Pred`), and a `CtEvidence` will now store a `Pred`, not a `PredType`.
See also https://gitlab.haskell.org/ghc/ghc/wikis/dependent-haskell/phase2, which has much discussion.Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/17333Coercible solver does not look through "class newtypes"2023-06-10T10:55:13ZRyan ScottCoercible solver does not look through "class newtypes"The code below makes use of the "class newtype" design pattern:
```hs
class Show a => MyShow a
instance Show a => MyShow a
```
`MyShow` is a newtype around `Show` in the sense that when compiled to Core, a `MyShow` dictionary is lit...The code below makes use of the "class newtype" design pattern:
```hs
class Show a => MyShow a
instance Show a => MyShow a
```
`MyShow` is a newtype around `Show` in the sense that when compiled to Core, a `MyShow` dictionary is literally a newtype around `Show`. Unfortunately, this newtype treatment does not extend to the `Coercible` solver, as the following example demonstrates:
```hs
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MonoLocalBinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
module Bug where
import Data.Coerce
class Show a => MyShow a
instance Show a => MyShow a
newtype T1 a = MkT1 ( Show a => a -> a -> String)
newtype T2 a = MkT2 (MyShow a => a -> a -> String)
f :: T1 a -> T2 a
f = coerce
```
```
$ /opt/ghc/8.8.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:20:5: error:
• Couldn't match representation of type ‘MyShow a’
with that of ‘Show a’
arising from a use of ‘coerce’
The data constructor ‘Bug.C:MyShow’
of newtype ‘MyShow’ is not in scope
• In the expression: coerce
In an equation for ‘f’: f = coerce
• Relevant bindings include
f :: T1 a -> T2 a (bound at Bug.hs:20:1)
|
20 | f = coerce
| ^^^^^^
```
Somewhat surprisingly, this does not work. Even the error message indicates that `MyShow` is a newtype (which is a bit odd, but whatever), but since the internal `C:MyShow` constructor is not exposed, the `Coercible` solver doesn't have enough information to proceed.
If the following change is applied to GHC, then it typechecks:
```diff
diff --git a/compiler/typecheck/FamInst.hs b/compiler/typecheck/FamInst.hs
index a339dd7b57..8640b3e3e0 100644
--- a/compiler/typecheck/FamInst.hs
+++ b/compiler/typecheck/FamInst.hs
@@ -41,7 +41,7 @@ import Name
import Pair
import Panic
import VarSet
-import Bag( Bag, unionBags, unitBag )
+import Bag( Bag, emptyBag, unionBags, unitBag )
import Control.Monad
#include "HsVersions.h"
@@ -577,6 +577,10 @@ tcTopNormaliseNewTypeTF_maybe faminsts rdr_env ty
= mapStepResult (\co -> (unitBag gre, co)) $
unwrapNewTypeStepper rec_nts tc tys
+ | isClassTyCon tc && isNewTyCon tc
+ = mapStepResult (\co -> (emptyBag, co)) $
+ unwrapNewTypeStepper rec_nts tc tys
+
| otherwise
= NS_Done
```
The simplified example above is somewhat contrived, although I have legitimate need of this feature in more complicated scenarios like this one (inspired by [Generic Programming of All Kinds](https://victorcmiraldo.github.io/data/hask2018_draft.pdf)):
```hs
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
module GOAK where
import Data.Coerce
import Data.Kind
newtype T = MkT ((forall a. Show a) => Int)
type TRep = Field (ForAllQ (Kon Show :@: Var VZ) :=>>: Kon Int) LoT0
f :: T -> TRep
f (MkT x) = Field (coerce @((forall a. Show a) => Int)
@(Interpret (ForAllQ (Kon Show :@: Var VZ) :=>>: Kon Int) LoT0)
x)
-----
infixr 5 :&&:
data LoT :: Type -> Type where
LoT0 :: LoT Type
(:&&:) :: k -> LoT ks -> LoT (k -> ks)
type family HeadLoT (tys :: LoT (k -> k')) :: k where
HeadLoT (a :&&: _) = a
type family TailLoT (tys :: LoT (k -> k')) :: LoT k' where
TailLoT (_ :&&: as) = as
data TyVar :: Type -> Type -> Type where
VZ :: TyVar (x -> xs) x
VS :: TyVar xs k -> TyVar (x -> xs) k
data Atom :: Type -> Type -> Type where
Var :: TyVar d k -> Atom d k
Kon :: k -> Atom d k
(:@:) :: Atom d (k1 -> k2) -> Atom d k1 -> Atom d k2
(:=>>:) :: Atom d Constraint -> Atom d Type -> Atom d Type
ForAllQ :: Atom (d1 -> d) Constraint -> Atom d Constraint
type family InterpretVar (t :: TyVar d k) (tys :: LoT d) :: k where
InterpretVar 'VZ tys = HeadLoT tys
InterpretVar ('VS v) tys = InterpretVar v (TailLoT tys)
type family Interpret (t :: Atom d k) (tys :: LoT d) :: k where
Interpret ('Var v) tys = InterpretVar v tys
Interpret ('Kon t) tys = t
Interpret (f ':@: x) tys = (Interpret f tys) (Interpret x tys)
Interpret (c ':=>>: f) tys = SuchThatI c f tys
Interpret (ForAllQ f) tys = ForAllQI f tys
newtype SuchThatI :: Atom d Constraint -> Atom d Type -> LoT d -> Type where
SuchThatI :: (Interpret c tys => Interpret f tys) -> SuchThatI c f tys
class (forall t. WrappedQI f (t ':&&: tys)) => ForAllQI (f :: Atom (d1 -> d) Constraint) (tys :: LoT d)
instance (forall t. WrappedQI f (t ':&&: tys)) => ForAllQI (f :: Atom (d1 -> d) Constraint) (tys :: LoT d)
class Interpret f tys => WrappedQI (f :: Atom d Constraint) (tys :: LoT d)
instance Interpret f tys => WrappedQI (f :: Atom d Constraint) (tys :: LoT d)
newtype Field :: Atom d Type -> LoT d -> Type where
Field :: { unField :: Interpret t x } -> Field t x
```
`f` will not typecheck without the ability to coerce from `ForAllQI f tys` to `forall t. WrappedQI f (t ':&&: tys)`. Moreover, it would be extremely difficult to write `f` _without_ `coerce`.https://gitlab.haskell.org/ghc/ghc/-/issues/17327Kind-checking associated types2020-02-18T16:17:45ZmniipKind-checking associated types## Summary
When kind checking associated type declarations in an `instance` declaration, the instance context seems to be ignored.
## Steps to reproduce
Minimal complete example:
```haskell
{-# LANGUAGE DataKinds, PolyKinds, TypeFamil...## Summary
When kind checking associated type declarations in an `instance` declaration, the instance context seems to be ignored.
## Steps to reproduce
Minimal complete example:
```haskell
{-# LANGUAGE DataKinds, PolyKinds, TypeFamilies, FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, TypeApplications #-}
class C (k :: *) (a :: *) where
type F k a :: k
data D k (x :: k)
instance C k (D k x) where
type F k (D k x) = x -- good
instance (k ~ l) => C l (D k x) where
type F l (D k x) = x -- bad
{-
b.hs:11:22: error:
• Expected kind ‘l’, but ‘x’ has kind ‘k’
• In the type ‘x’
In the type instance declaration for ‘F’
In the instance declaration for ‘C l (D k x)’
|
11 | type F l (D k x) = x -- bad
| ^
-}
```
## Expected behavior
The second instance should kind-check (it has better instance resolution properties than the first which is why we want it).
## Environment
Tested on GHC 8.6.5 and GHC HEADhttps://gitlab.haskell.org/ghc/ghc/-/issues/17323The Purely Kinded Type Invariant (PKTI) is not good enough2020-01-24T11:45:59ZRichard Eisenbergrae@richarde.devThe Purely Kinded Type Invariant (PKTI) is not good enoughRequired reading: `Note [The Purely Kinded Type Invariant (PKTI)]` and `Note [mkAppTyM]`, both in TcHsType.
The PKTI has at least two problems.
1. Suppose we have the type `a -> b` stored in `ty`. If we say `splitTyConApp ty`, we shoul...Required reading: `Note [The Purely Kinded Type Invariant (PKTI)]` and `Note [mkAppTyM]`, both in TcHsType.
The PKTI has at least two problems.
1. Suppose we have the type `a -> b` stored in `ty`. If we say `splitTyConApp ty`, we should expect to get `(funTyCon, [r1, r2, a, b])` where `a :: TYPE r1` and `b :: TYPE r2`. But what if `a` doesn't have type `TYPE r1` or `b` doesn't have type `TYPE r2`? This can happen if, say, `a :: kappa` and `kappa := TYPE r1`, but we haven't zonked. The PKTI must address this. This means that we will have to write `mkFunTyM` just like `mkAppTyM`. We might even need `mkTyConAppM` to handle the case when the tycon is `(->)`. :(
2. Nasty case 2 of `Note [mkAppTyM]` isn't sufficient. That case considers a type synonym. What about a type family?
```hs
type family F (a :: Type -> Type) (b :: Type) where
F a b = a b
```
According to its current text of the PKTI, `F (a :: kappa1) (b :: kappa2)` satisfies the PKTI. Yet if we reduce this type family, `a b` does not satisfy the PKTI. Yet we sometimes reduce type families in a pure context (`normaliseType`) and, moreover, the main type-family-reduction engine in TcFlatten does not respect the PKTI in this case as it does rewriting. (Actually, it does, because the flattener zonks thoroughly. But we're exploring the possibility of not zonking as thoroughly in the future. And, in any case, there is no documented connection between the flattener's desire to zonk and the PKTI.)
With some plumbing, etc., I'm confident we can fix (1). But I really have no idea how to fix (2). I worry we will have to abandon the idea of pure reductions, and we'll have to teach the flattener to check for "tricky tvs" (see `isTrickyTvBinder`) much like `mkAppTyM` does. Or, we can abandon pure reductions and just keep the flattener zonking thoroughly. :)https://gitlab.haskell.org/ghc/ghc/-/issues/17311Type family equality gets stuck on types that fail the occurs check2020-12-11T15:47:16ZisovectorType family equality gets stuck on types that fail the occurs check## Summary
A type family that should check two types for equality gets stuck, even though their equality would fail the occurs check.
## Steps to reproduce
The following program doesn't compile:
```haskell
{-# LANGUAGE AllowAmbiguous...## Summary
A type family that should check two types for equality gets stuck, even though their equality would fail the occurs check.
## Steps to reproduce
The following program doesn't compile:
```haskell
{-# LANGUAGE AllowAmbiguousTypes #-}
module Occurs where
import Data.Functor.Identity
import Data.Proxy
type family Equal a b where
Equal a a = 'True
Equal a b = 'False
foo :: Proxy (Equal (Identity a) a) -> Proxy 'False
foo = id
```
with error:
```
• Couldn't match type ‘Equal (Identity a) a’ with ‘'False’
Expected type: Proxy (Equal (Identity a) a) -> Proxy 'False
Actual type: Proxy 'False -> Proxy 'False
• In the expression: id
In an equation for ‘foo’: foo = id
• Relevant bindings include
foo :: Proxy (Equal (Identity a) a) -> Proxy 'False
(bound at /home/sandy/Vikrem.hs:14:1)
|
14 | foo = id
|
```
The `Equal` type family is stuck due to `a` being a variable, but the only way `Equal (Identity a) a ~ 'True` is for an infinite instantiation of `a`. As such, this thing should reduce.
## Expected behavior
I expect the above program to compile, with `Equal (Identity a) a` reducing to `'False`.
## Environment
* GHC version used: 8.6.5
Optional:
* Operating System: Archlinux
* System Architecture: x86_64