GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2020-11-09T14:13:59Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/18920ghc-8.8 does not infer kind2020-11-09T14:13:59Zjwaldmannghc-8.8 does not infer kindRejected by ghc-8.8.4 with
```
should.hs:27:12: error:
• Expected kind ‘* -> *’, but ‘solver’ has kind ‘*’
• In the first argument of ‘Solver’, namely ‘solver’
In the type ‘(Solver solver, Queue q, Transformer t) =>
...Rejected by ghc-8.8.4 with
```
should.hs:27:12: error:
• Expected kind ‘* -> *’, but ‘solver’ has kind ‘*’
• In the first argument of ‘Solver’, namely ‘solver’
In the type ‘(Solver solver, Queue q, Transformer t) =>
Int -> q -> t -> EvalState t -> solver (Int, [a])’
In the type declaration for ‘ContinueSig’
```
but accepted by 8.6.5, 8.10.2. 9.0.1-alpha1.
```
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE GADTs #-}
class Monad solver => Solver solver where
type Constraint solver :: *
type Label solver :: *
class Queue q
data Tree s a where
NewVar :: Term s t => (t -> Tree s a) -> Tree s a
class Solver solver => Term solver term
class Transformer t where
type EvalState t :: *
type TreeState t :: *
type ForSolver t :: (* -> *)
type ForResult t :: *
nextT :: SearchSig (ForSolver t) q t (ForResult t)
returnT :: ContinueSig solver q t (ForResult t)
type ContinueSig solver q t a =
( Solver solver, Queue q, Transformer t )
=> Int -> q -> t -> EvalState t
-> solver (Int, [a])
type SearchSig solver q t a =
(Solver solver, Queue q, Transformer t )
=> Int -> Tree solver a -> q -> t -> EvalState t -> TreeState t
-> solver (Int,[a])
```
8.8 accepts this after introducing this:
```
type ContinueSig (solver :: * -> *) q t a =
...
```8.10.1https://gitlab.haskell.org/ghc/ghc/-/issues/18910Order-dependent type inference due to Note [Instance and Given overlap]2022-03-15T22:16:55ZRichard Eisenbergrae@richarde.devOrder-dependent type inference due to Note [Instance and Given overlap]With some effort, I have produced
```hs
{-# LANGUAGE ScopedTypeVariables, AllowAmbiguousTypes, TypeApplications,
TypeFamilies, PolyKinds, DataKinds, FlexibleInstances,
MultiParamTypeClasses, FlexibleContexts, P...With some effort, I have produced
```hs
{-# LANGUAGE ScopedTypeVariables, AllowAmbiguousTypes, TypeApplications,
TypeFamilies, PolyKinds, DataKinds, FlexibleInstances,
MultiParamTypeClasses, FlexibleContexts, PartialTypeSignatures #-}
module Bug where
import Data.Proxy
class P a
class Q a
class R a b
newtype Tagged (t :: k) a = Tagged a
type family F a
type instance F (Tagged @Bool t a) = [a]
instance P x => Q [x]
instance (x ~ y) => R y [x]
wob :: forall a b. (Q [b], R b a) => a -> Int
wob = undefined
it'sABoolNow :: forall (t :: Bool). Int
it'sABoolNow = undefined
class HasBoolKind t
instance k ~ Bool => HasBoolKind (t :: k)
it'sABoolLater :: forall t. HasBoolKind t => Int
it'sABoolLater = undefined
g :: forall t a. Q (F (Tagged t a)) => Proxy t -> [a] -> _
g _ x = it'sABoolNow @t + wob x
g2 :: forall t a. Q (F (Tagged t a)) => Proxy t -> [a] -> _
g2 _ x = wob x + it'sABoolNow @t
g3 :: forall t a. Q (F (Tagged t a)) => Proxy t -> [a] -> _
g3 _ x = it'sABoolLater @t + wob x
g4 :: forall t a. Q (F (Tagged t a)) => Proxy t -> [a] -> _
g4 _ x = wob x + it'sABoolLater @t
```
All of `g`, `g2`, and `g3` are accepted. `g4` is rejected. Note that `g4` is identical to `g3` except for changing the order of the summands.
What's going on:
Here is an excerpt from `Note [Instance and Given overlap]`:
```
Example, from the OutsideIn(X) paper:
instance P x => Q [x]
instance (x ~ y) => R y [x]
wob :: forall a b. (Q [b], R b a) => a -> Int
g :: forall a. Q [a] => [a] -> Int
g x = wob x
From 'g' we get the implication constraint:
forall a. Q [a] => (Q [beta], R beta [a])
If we react (Q [beta]) with its top-level axiom, we end up with a
(P beta), which we have no way of discharging. On the other hand,
if we react R beta [a] with the top-level we get (beta ~ a), which
is solvable and can help us rewrite (Q [beta]) to (Q [a]) which is
now solvable by the given Q [a].
```
Here is the scenario in the Note, when type-checking the Note's `g`:
```
[G] Q [a]
[W] Q [beta]
[W] R beta [a]
```
When we process the first Wanted, we might be tempted to use the instance, simplifying the Wanted to `P beta`. Doing this leads to failure. What we'd prefer is to recognize that the Given might be helpful later, and just to leave the Wanted as-is. Then, processing the `[W] R beta [a]` tells us that `beta ~ a`, and we go home happy.
The scenario in this ticket is rather more complicated. The instances are unchanged, but now we have a type family `F` in the mix. It all looks like
```
t :: kappa
[G] Q (F (Tagged @kappa t a))
[W] Q [beta]
[W] R beta [a]
```
The question is: when processing the first Wanted, should the Given block GHC from using the global instance? (Sidenote: I've used partial type signatures and polykinds here as a sneaky way of getting a metavariable into a Given. The partial type signature stops GHC from kind-generalizing the type, and thus `t`'s kind remains as `kappa` when processing the body.) If `kappa` is `Bool`, then the Given will eventually match and should block us from using the instance. If `kappa` is not `Bool`, then the Given will not apply. Yet in all of `g`..`g4`, `kappa` turns out to be `Bool`.
In `g`, we have `it'sABoolNow @t`, and the eager unifier sets `kappa := Bool` before the constraint solver gets a crack. The application of `F` reduces and the Given is recognized as relevant, blocking the use of the global instance.
In `g2`, the same happens.
In `g3`, we get a new `[W] HasBoolKind @kappa t`. This gets processed *before* the `Q [beta]` Wanted, and processing this sets `kappa := Bool`, leading the Given to reduce and block the use of the global instance.
In `g4`, however, the new `[W] HasBoolKind @kappa t` comes *after* the others. So we process `Q [beta]` *before* learning about `kappa`. The global instance is used, and we are left stuck with `[W] P a` that cannot be solved.
This all boils down to the `not (isFskTyVar tv)` check in `GHC.Tc.Solver.Monad.mightMatchLater`, which (effectively) says that type family applications in Givens match only themselves, not any arbitrary type. Removing that check fixes this problem. But it introduces another. The following program is accepted today:
```hs
{-# LANGUAGE TypeFamilies, FlexibleInstances, FlexibleContexts #-}
module Bug2 where
class C a where
meth :: a -> ()
instance C Int where
meth _ = ()
type family F a
foo :: C (F a) => a -> Int -> ()
foo _ n = meth n
```
If we strike that check from `mightMatchLater`, we get
```
• Overlapping instances for C Int arising from a use of ‘meth’
Matching instances:
instance C Int -- Defined at CbvOverlap.hs:10:10
There exists a (perhaps superclass) match:
from the context: C (F a)
bound by the type signature for:
foo :: forall a. C (F a) => a -> Int -> ()
at CbvOverlap.hs:15:1-32
(The choice depends on the instantiation of ‘’
To pick the first instance above, use IncoherentInstances
when compiling the other instance declarations)
• In the expression: meth n
In an equation for ‘foo’: foo _ n = meth n
```
The (unrelated) `[G] C (F a)` blocks the useful `instance C Int`. Worse, the error message says that the overlap depends on the instantiation of <<empty list>>.
This new problem is not just theoretical. In my !4149 patch, I essentially made this change unintentionally, and GHC's Parser.hs stopped compiling (in stage 2), due to its `DisambECP` shenanigans. It's easy for me to replicate the current behavior, so my branch can continue, but this bug will remain.
I'm not sure what the solution is. If we allow type family applications in Givens to match any potential type, we will unavoidably cause the second bug. So perhaps the best course of action is to let sleeping dogs lie. Yet I was uncomfortable reinstating the old behavior, because it smelled off... and I wanted to understand it better. Thus this ticket.https://gitlab.haskell.org/ghc/ghc/-/issues/18891Kind inference for newtypes in GADT syntax is deeply broken2020-12-08T21:03:16ZRichard Eisenbergrae@richarde.devKind inference for newtypes in GADT syntax is deeply brokenHere are some tales of destruction, all with `-XUnliftedNewtypes` and `-XNoCUSKs`:
```hs
newtype N :: forall k. TYPE k where
MkN :: N -> N
```
gives
```
Scratch.hs:34:3: error:
• Expected a type, but ‘N’ has kind ‘*’
• In th...Here are some tales of destruction, all with `-XUnliftedNewtypes` and `-XNoCUSKs`:
```hs
newtype N :: forall k. TYPE k where
MkN :: N -> N
```
gives
```
Scratch.hs:34:3: error:
• Expected a type, but ‘N’ has kind ‘*’
• In the definition of data constructor ‘MkN’
In the newtype declaration for ‘N’
```
------------------------
```hs
type N :: forall k. TYPE k
newtype N :: forall k. TYPE k where
MkN :: N -> N
```
gives
```
Scratch.hs:35:3: error:
• A newtype constructor must have a return type of form T a1 ... an
MkN :: N -> N
• In the definition of data constructor ‘MkN’
In the newtype declaration for ‘N’
```
-------------------------
```hs
newtype N :: forall k -> TYPE k where
MkN :: N m -> N m
```
gives
```
Scratch.hs:35:3: error:
• Expected a type, but ‘N m’ has kind ‘TYPE m’
• In the definition of data constructor ‘MkN’
In the newtype declaration for ‘N’
```
-------------------------
```hs
type N :: forall k -> TYPE k
newtype N :: forall k -> TYPE k where
MkN :: N m -> N m
```
succeeds.
I think all these examples should succeed. All but the last cause a DEBUG build of GHC to panic.
I think the problem is that the `res_kind` passed to `kcConArgTys` has the wrong scope: it mentions variables in the type head, but these are utterly distinct from the variables in the constructor type.9.2.1https://gitlab.haskell.org/ghc/ghc/-/issues/18875Occurs-check-y Givens rewrite once, but not twice2020-12-04T22:10:52ZRichard Eisenbergrae@richarde.devOccurs-check-y Givens rewrite once, but not twiceGHC remarkably accepts this program:
```hs
type family UnMaybe a where
UnMaybe (Maybe b) = b
class C c where
meth :: c
instance C (Maybe d) where
meth = Nothing
f :: (e ~ Maybe (UnMaybe e)) => e
f = meth
```
This is remarkable...GHC remarkably accepts this program:
```hs
type family UnMaybe a where
UnMaybe (Maybe b) = b
class C c where
meth :: c
instance C (Maybe d) where
meth = Nothing
f :: (e ~ Maybe (UnMaybe e)) => e
f = meth
```
This is remarkable because satisfying the `C e` constraint arising from the use of `meth` requires using the `e ~ Maybe (UnMaybe e)` given, despite the fact that it has an occurs-check failure. That is, GHC must rewrite `e` to `Maybe (UnMaybe e)` to solve the class constraint, yet not fall into a look trying to expand `e` further. This works due to the way GHC currently uses flattening-skolems to deal with type family applications. (The program above does not work on the current tip of !4149, which avoids this flattening mechanism.)
However, GHC rejects this program:
```hs
type family G a b where
G (Maybe c) d = d
h :: (e ~ Maybe (G e f)) => e -> f
h (Just x) = x
```
Here, `h` has a similar given with an occurs-check failure. In contrast to the first example, though, we need to use the equation *twice* in order to accept this program. Specifically, we have
```
[G] e ~ Maybe (G e f)
[W] e ~ Maybe f
```
Using the Given for rewriting once gives us
```
[W] Maybe (G e f) ~ Maybe f
```
which decomposes to
```
[W] G e f ~ f
```
But now, we must use the given *again* to get
```
[W] G (Maybe (G e f)) f ~ f
```
so that can reduce to
```
[W] f ~ f
```
and be solved.
I think this will be hard to achieve in practice (rewriting twice). Might we need even more rewrites in pathological scenarios? I don't know.
The purpose of this ticket is more to record the incompleteness than to actively agitate for a solution. This did not arise in a real application and would likely be hard to fix.https://gitlab.haskell.org/ghc/ghc/-/issues/18873Quantified equality constraints are not used for rewriting2020-12-10T20:30:27ZRichard Eisenbergrae@richarde.devQuantified equality constraints are not used for rewritingIf I say
```hs
type family F a b where
F [_] b = b
f :: forall a b. (a ~ [b]) => F a b -> b
f x = x
```
GHC smiles upon me: the equality constraint rewrites `a` to `[b]`, and then `F [b] b` can reduce to `b`, and all is well.
But i...If I say
```hs
type family F a b where
F [_] b = b
f :: forall a b. (a ~ [b]) => F a b -> b
f x = x
```
GHC smiles upon me: the equality constraint rewrites `a` to `[b]`, and then `F [b] b` can reduce to `b`, and all is well.
But if I say
```hs
type family F a b where
F [_] b = b
class Truth
instance Truth
f :: forall a b. (Truth => a ~ [b]) => F a b -> b
f x = x
```
I get an error, saying `F a b` does not match `b`. This is because the equality, hidden behind `Truth`, is not used for rewriting, and thus GHC cannot figure out that `F a b` can reduce.
I don't see an easy solution here.
This isn't just me grousing: a problem on !4149 could be worked around if GHC used such equalities for rewriting. And so if we can solve this problem, we can solve the other one. My expectation is that we won't solve this one, though.https://gitlab.haskell.org/ghc/ghc/-/issues/18863Visibility mismatch between data declaration and kind signature, accepted!2023-09-27T08:24:13ZIcelandjackVisibility mismatch between data declaration and kind signature, accepted!```haskell
{-# Language PolyKinds #-}
{-# Language RankNTypes #-}
{-# Language StandaloneKindSignatures #-}
import Data.Kind
type ID :: forall i -> i -> Type
data ID :: forall i -> i -> Type
```
This compi...```haskell
{-# Language PolyKinds #-}
{-# Language RankNTypes #-}
{-# Language StandaloneKindSignatures #-}
import Data.Kind
type ID :: forall i -> i -> Type
data ID :: forall i -> i -> Type
```
This compiles on 8.10.0.20191123, if we change the standalone kind signature `forall->` to `forall.` we get an error. Obviously?
```haskell
-- • Couldn't match expected kind ‘forall i1 -> i1 -> *’
-- with actual kind ‘i -> *’
-- • In the data type declaration for ‘ID’
-- |
-- 8 | data ID :: forall i -> i -> Type
-- | ^^^^^^^
type ID :: forall i. i -> Type
data ID :: forall i -> i -> Type
```
But then why does this compile
```haskell
type ID :: forall i -> i -> Type
data ID :: forall i. i -> Type
```9.2.1https://gitlab.haskell.org/ghc/ghc/-/issues/18851Non-confluence in the solver2022-09-06T11:40:53ZRichard Eisenbergrae@richarde.devNon-confluence in the solverIn #18759 (starting at https://gitlab.haskell.org/ghc/ghc/-/issues/18759#note_306441 and then refined in https://gitlab.haskell.org/ghc/ghc/-/issues/18759#note_306722, but you don't need to read that ticket to understand this one), we ex...In #18759 (starting at https://gitlab.haskell.org/ghc/ghc/-/issues/18759#note_306441 and then refined in https://gitlab.haskell.org/ghc/ghc/-/issues/18759#note_306722, but you don't need to read that ticket to understand this one), we explored various ways of disabling the coverage condition for functional dependencies. In https://gitlab.haskell.org/ghc/ghc/-/issues/18759#note_307486, @simonpj asks whether these techniques can disrupt confluence.
They can. (EDIT: Furthermore, more hammering in this direction discovered non-confluence even *without* functional dependencies. See https://gitlab.haskell.org/ghc/ghc/-/issues/18851#note_318471.)
Here is the example:
```hs
{-# LANGUAGE FunctionalDependencies, FlexibleInstances, UndecidableInstances,
ScopedTypeVariables, TypeFamilies, TypeApplications,
FlexibleContexts, AllowAmbiguousTypes #-}
module Bug where
class C a b | a -> b
instance C Int b => C Int b
class IsInt int
instance int ~ Int => IsInt int
data A
instance Show A where
show _ = "A"
data B
instance Show B where
show _ = "B"
f :: forall a b c int. (Show a, Show b, Show c, C int a, C int b, C int c, IsInt int) => String
f = show (undefined :: c)
g = f @A @B
```
`g` evaluates to `"B"`. If I switch the order of the `C int a` and `C int b` constraints in the type of `f`, `g` will evaluate to `"A"`. Urgh.
(Sidenote: this file needs `AllowAmbiguousTypes`, but there are no ambiguous types here. That bug is reported as #18850.)
What's going on? When calling `f` from `g`, GHC needs to figure out how to instantiate the type variables `a`, `b`, `c`, and `int`, and GHC must find dictionaries to supply for all the class constraints. First, GHC creates unification variables `a0`, `b0`, `c0`, and `int0`. The type applications tell us `a0 := A` and `b0 := B`. Good. Then we have these constraints:
```
[W] w1 : Show A
[W] w2 : Show B
[W] w3 : Show c0
[W] w4 : C int0 A
[W] w5 : C int0 B
[W] w6 : C int0 c0
[W] w7 : IsInt int0
```
GHC processes these in the order given. `w1` and `w2` are easily despatched. `w3` doesn't make any progress at all. Neither does `w4` or `w5`. So we're then in this state:
```
worklist: [W] w6 : C int0 c0
[W] w7 : IsInt int0
inerts: [W] w3 : Show c0
[W] w4 : C int0 A
[W] w5 : C int0 B
```
We then look at `w6`. It doesn't make progress. But then GHC looks at the inerts, and sees that `w4` and `w5` have the same first argument to `C` (`int0`) as the work item `w6`. Because of the functional dependency on `C`, this means that `c0` must match the second argument to `C` in the inert. The problem is that there are *two* such inerts! GHC chooses the last one, arbitrarily. Thus, we get `c0 := B` and carry on. If the constraints were processed in a different order, we'd end up with `c0 := A`. This is classic non-confluence.
Why have `IsInt` here? It's to slow down GHC. If we just wrote an explicit `Int` in the type signature for `f`, then GHC would eagerly solve `w4' : C Int A` and `w5' : C Int B`. When processing `w6' : C Int c0`, GHC wouldn't have any inerts to look at. Instead, it would look at the instance for `C`, which is unhelpful in this case. Indeed, moving the `IsInt int` constraint earlier (before the `C` constraints) in `f`'s type signature causes GHC to error, as it doesn't know how to instantiate `c0`, having lost the hints from the inerts. (More non-confluence!)
What to do? I think the next step is to compare this to the [constraint-handling rules paper](https://www.researchgate.net/profile/Martin_Sulzmann/publication/213885702_Understanding_Functional_Dependencies_via_Constraint_Handling_Rules/links/09e41511297969891f000000.pdf), which proves confluence, and see whether that paper has a mistake, or where GHC violates an assumption in that paper. (Probably the latter: my instance for `C` is very naughty.)https://gitlab.haskell.org/ghc/ghc/-/issues/18850Instance/given overlap trips up the ambiguity check2020-10-29T19:00:42ZRichard Eisenbergrae@richarde.devInstance/given overlap trips up the ambiguity checkThursday is a good day to abuse GHC. So I said this:
```hs
{-# LANGUAGE TypeFamilies, FlexibleInstances #-}
module Bug where
class IsBool bool
instance bool ~ Bool => IsBool bool
class C a
instance C Bool
f :: (C bool, IsBool bool) ...Thursday is a good day to abuse GHC. So I said this:
```hs
{-# LANGUAGE TypeFamilies, FlexibleInstances #-}
module Bug where
class IsBool bool
instance bool ~ Bool => IsBool bool
class C a
instance C Bool
f :: (C bool, IsBool bool) => ()
f = ()
```
To me, `f`'s type is unambiguous: the `IsBool bool` constraint fixes the type variable `bool` to be `Bool`. But GHC says
```
/Users/rae/temp/Bug2.hs:11:6: error:
• Could not deduce (C bool0)
from the context: (C bool, IsBool bool)
bound by the type signature for:
f :: forall bool. (C bool, IsBool bool) => ()
at /Users/rae/temp/Bug2.hs:11:6-32
The type variable ‘bool0’ is ambiguous
• In the ambiguity check for ‘f’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature: f :: (C bool, IsBool bool) => ()
|
11 | f :: (C bool, IsBool bool) => ()
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
But maybe I'm wrong. Is the type really ambiguous? No. When I say
```hs
{-# LANGUAGE TypeFamilies, FlexibleInstances, AllowAmbiguousTypes #-}
module Bug where
class IsBool bool
instance bool ~ Bool => IsBool bool
class C a
instance C Bool
f :: (C bool, IsBool bool) => ()
f = ()
g = f
```
my program is accepted. I've added `AllowAmbiguousTypes` and the binding `g = f`. That binding is accepted -- no type applications or other funny business. This suggests that `f`'s type is not actually ambiguous.
What's going on is an over-eager instance/given overlap; see `Note [Instance and Given overlap]` in `GHC.Tc.Solver.Interact`. That Note ends with
```
All of this is disgustingly delicate, so to discourage people from writing
simplifiable class givens, we warn about signatures that contain them;
see GHC.Tc.Validity Note [Simplifiable given constraints].
```
But I don't get the warning! Even in my second program, which is error-free. Hunting further into `GHC.Tc.Validity`, I find this code:
```hs
checkSimplifiableClassConstraint env dflags ctxt cls tys
| not (wopt Opt_WarnSimplifiableClassConstraints dflags)
= return ()
| xopt LangExt.MonoLocalBinds dflags
= return ()
| ...
```
where the `...` includes generating a warning. Of course, I *do* have `-XMonoLocalBinds`, as implied by `-XTypeFamilies`. What happens when I disable this (with an explicit `-XNoMonoLocalBinds`)?
```
/Users/rae/temp/Bug2.hs:11:6: warning: [-Wsimplifiable-class-constraints]
• The constraint ‘IsBool bool’ matches
instance (bool ~ Bool) => IsBool bool
-- Defined at /Users/rae/temp/Bug2.hs:6:10
This makes type inference for inner bindings fragile;
either use MonoLocalBinds, or simplify it using the instance
• In the type signature: f :: (C bool, IsBool bool) => ()
|
11 | f :: (C bool, IsBool bool) => ()
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
Good. The warning fires.
My conclusions:
1. My first program really ought to be accepted. The type is not ambiguous. I'm willing to concede this point to "disgustingly delicate", though, if we don't see an easy way to fix.
2. It looks the warning should fire even when `-XMonoLocalBinds` is in effect. My program has no local generalization involved. How would users disable the warnings? By not writing a simplifiable Given.https://gitlab.haskell.org/ghc/ghc/-/issues/18802Typecheck record update via desugaring2022-05-26T07:45:30ZSimon Peyton JonesTypecheck record update via desugaringThere are quite a few tickets relating to inadequacies of record update, including
* #18311
* #10856
* #2595
* #10808
* #3632: updating existentials if you do all of them at once
* #16501
* #21289
* #21158
Record update is a place whe...There are quite a few tickets relating to inadequacies of record update, including
* #18311
* #10856
* #2595
* #10808
* #3632: updating existentials if you do all of them at once
* #16501
* #21289
* #21158
Record update is a place where our general plan of typechecking the source syntax seems particularly hard to do. It wold be much easier (and correct by construction) to desugar (but still in HsSyn) and typecheck that.
Fortunately we now have a way to do that: our [Re-engineer rebindable syntax](https://gitlab.haskell.org/ghc/ghc/-/issues/17582) ticket, #17582. A lot of attention is paid there to maintaining good error messages, which is the main challenge of this approach.
So this ticket is to propose: let's use the work on #17582 to solve our record-update tickets.
See also #21158 for why this will be a breaking change.9.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/18758Remove NoGhcTc, allow HsType GhcTc, HsDecl GhcTc2023-04-11T11:15:20ZVladislav ZavialovRemove NoGhcTc, allow HsType GhcTc, HsDecl GhcTc## Background
Currently, we carefully avoid `HsType GhcTc` or `HsDecl GhcTc`, by means of the `NoGhcTc` type family:
```
| HsAppType (XAppTypeE p) -- After typechecking: the type argument
(LHsExpr p)
(LHsWcType ...## Background
Currently, we carefully avoid `HsType GhcTc` or `HsDecl GhcTc`, by means of the `NoGhcTc` type family:
```
| HsAppType (XAppTypeE p) -- After typechecking: the type argument
(LHsExpr p)
(LHsWcType (NoGhcTc p)) -- ^ Visible type application
```
The primary reason for this is that kind-checking and desugaring of types are intertwined. We mostly work with `TcType` instead of `HsType GhcTc` because it's more convenient in some places (e.g. in `unifyKind` and `unifyType`).
## Motivation A
A better architecture would be to have similar pipelines for terms and types:
* `HsExpr GhcPs -> HsExpr GhcRn -> HsExpr GhcTc`
* `HsType GhcPs -> HsType GhcRn -> HsType GhcTc`
This would allow us to talk about e.g. `HsDecl GhcTc`. For example, when discussing #12088, there was an idea of a refactoring that would separate `tcTyClDecl` and zonking. But then we'd like the type of `tcTyClDecl` to be:
```haskell
tcTyClDecl :: LTyClDecl GhcRn -> TcM (LTyClDecl GhcTc)
```
And that's not currently possible.
## Motivation B
This would facilitate fixing #15824, for instance, as we could use `HsType GhcTc` as the input to `GHC.Tc.Gen.Splice.reifyType`. This way, we would retain the `HsOpTy` and `HsAppTy` distinction.
## Partial Solution
In order to address Motivation B, we would need to properly embed coercions into `HsType GhcTc` and start using it throughout the type checker. However, that would be a very major, intrusive refactoring. Before we do that, there's a stopgap solution that could be used to address Motivation A.
Define the following `XXType` instance:
```
type instance XXType GhcTc = HsTypeTc
data HsTypeTc = HsTypeTc TcType SDoc
```
Then `HsType GhcTc` would only ever use `XHsType (HsTypeTc ty doc)`. The fields are as follows:
* `TcType` is the kind-checked, desugared type
* `SDoc` is the result of pretty printing `HsType GhcRn`, before parentheses and infix operators were discarded
This is sufficient to let us talk about `HsType GhcTc` and `HsDecl GhcTc`, and remove the `NoGhcTc` type family.
## Full Solution
The full solution would involve using `HsType GhcTc` throughout the type checker, rewriting zonking and unification to work over `HsType GhcTc`, and so on. It would address Motivation A, and also let us remove the notion of `TcType`: the type checker would work with `HsType GhcTc`, and `Type` would be only used in Core. That would be a nice improvement, as we could remove `TcTyVar` and `AnonArgFlag` (maybe something else?) from the syntax of Core.
## Completion
1. The partial solution is implemented.
I think we should start with the partial solution, so that's what this ticket is about. The full solution will require much more thought and design effort, so we can get back to it later.Vladislav ZavialovVladislav Zavialovhttps://gitlab.haskell.org/ghc/ghc/-/issues/18753Tighten up the treatment of loose types in the solver2020-09-30T16:21:20ZRichard Eisenbergrae@richarde.devTighten up the treatment of loose types in the solver`GHC.Tc.Solver.Monad` includes
```
Note [Use loose types in inert set]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Say we know (Eq (a |> c1)) and we need (Eq (a |> c2)). One is clearly
solvable from the other. So, we do lookup in the inert set...`GHC.Tc.Solver.Monad` includes
```
Note [Use loose types in inert set]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Say we know (Eq (a |> c1)) and we need (Eq (a |> c2)). One is clearly
solvable from the other. So, we do lookup in the inert set using
loose types, which omits the kind-check.
We must be careful when using the result of a lookup because it may
not match the requested info exactly!
```
There are several problems.
* We aren't always careful. For example, `lookupInInerts` tries `lookupSolvedDict` and then `lookupInertDict`, both of which use this "loose" lookup. Yet the result of `lookupInInerts` just uses the result, without any special handling to take the fact that the types might not match exactly.
* The Note doesn't actually make sense. The only difference between `Eq (a |> c1)` and `Eq (a |> c2)` is the coercion. But I sincerely hope we never care about the contents of a coercion. So even if we use evidence of type `Eq (a |> c1)` where GHC is expecting `Eq (a |> c2)` (assuming `c1` and `c2` have the same type), all will be well.
* What I think the Note is trying to say will never happen. That is, the actual implementation of the inert-set lookup tries to match types while ignoring their kinds. (Normal type matching requires that the kind matches also.) So a better example would be something like comparing `Eq (a :: k1)` with `Eq (a :: k2)`. But that's impossible, even with casts: all type families and classes have *closed* kinds, meaning that any variables that appear in the kinds of arguments must themselves be earlier arguments. In other words, if I have well-typed `T blah1 (... :: kind1)` and `T blah2 (... :: kind2)`, then either `kind1` equals `kind2` or `blah1` and `blah2` must differ. We use this logic elsewhere -- in particular, in the pure unifier.
Conclusions:
* Using "loose" matching (that is, ignoring kinds) in the solver is the right thing.
* We should update the Note with my argument above.
* No special care needs to be taken when using loose matching in this way. This means we can drop a few redundant equality checks (e.g. in `lookupFlatCache`).
I'm pretty confident about this all, but I'd like a double-check before I commit a fix.https://gitlab.haskell.org/ghc/ghc/-/issues/18739Infer multiplicity of let expression2023-12-21T21:18:04ZArnaud SpiwackInfer multiplicity of let expression## Motivation
In a let expression `let x = rhs in u`, `x` is always bound with multiplicity `Many` (and, correspondingly, `u` is consumed with multiplicity `Many`).
This also holds of where expression `u where x = rhs`.
The situation ...## Motivation
In a let expression `let x = rhs in u`, `x` is always bound with multiplicity `Many` (and, correspondingly, `u` is consumed with multiplicity `Many`).
This also holds of where expression `u where x = rhs`.
The situation is similar to that of case expression as in #18738 .
In #18461 , we are adding a syntax to force polymorphism, but programmers expect let expressions to know their multiplicity on their own (in particular, they expect `let x = y in u` to be the same as `u[x\y]`, but if the latter consumes `y` linearly, the former never does in the current GHC).
## Proposal
Infer the multiplicity of `let` binders instead of choosing `Many` systematically. The multiplicity would be a variable.
A small detail to pay attention to is that, in `let pat = rhs in u`, the outermost pattern of `pat` is lazy. Lazy pattern are only permissible in unrestricted patterns (one way to think about it is that the desugaring of lazy pattern is not linear).
The typechecker doesn't make this property very apparent, so we will have to be careful about it. I suppose the same issue arises in #18461 .https://gitlab.haskell.org/ghc/ghc/-/issues/18738Infer multiplicity of case expression2022-11-25T10:42:33ZArnaud SpiwackInfer multiplicity of case expression## Motivation
As it stands, the following expression
```haskell
case u of {…}
```
is always understood by the typechecker as consuming `u` with multiplicity `Many`. This was done in the first iteration of patch in order to ensure bein...## Motivation
As it stands, the following expression
```haskell
case u of {…}
```
is always understood by the typechecker as consuming `u` with multiplicity `Many`. This was done in the first iteration of patch in order to ensure being fully compatible with regular Haskell without having to delve too much into inference issue.
This applies to case expressions and to pattern guards creating a pattern:
```haskell
| pat <- u, … = …
```
here u is also consumed with multiplicity `Many`.
(In a `\case` or a function definition by equations, the multiplicity is decided by the type that it is checked against, if any. So it may be any multiplicity.)
Core is already equipped to deal with arbitrary multiplicities here.
## Proposal
These expressions should infer the appropriate multiplicity. So typechecking such a case expression should emit a multiplicity variable instead of choosing `Many` systematically.
One somewhat subtle point to keep in mind is that some patterns require that the scrutinee be consumed unrestrictedly. That's the case, for instance, of wildcard patterns (`_`). I believe that the current implementation will handle a variable for the pattern's multiplicity smoothly (see `checkManyPattern` in `GHC.Tc.Gen.Pat` ([currently](https://gitlab.haskell.org/ghc/ghc/-/blob/d7385f7077c6258c2a76ae51b4ea80f6fa9c7015/compiler/GHC/Tc/Gen/Pat.hs#L348-349)). But it's worth double-checking.
For pattern guard the relevant code is the `BindStmt` case of `tcGuardStmt` in `GHC.Tc.Gen.Match`.
cc @monoidalhttps://gitlab.haskell.org/ghc/ghc/-/issues/18715ThBrackCtxt is unused2020-09-21T21:17:06ZRyan ScottThBrackCtxt is unusedThe [`UserTypeCtxt`](https://gitlab.haskell.org/ghc/ghc/-/blob/a1f34d37b47826e86343e368a5c00f1a4b1f2bce/compiler/GHC/Tc/Types/Origin.hs#L57-92) data type defines a context for TH brackets:
```hs
data UserTypeCtxt
= ...
| ThBrackCtxt...The [`UserTypeCtxt`](https://gitlab.haskell.org/ghc/ghc/-/blob/a1f34d37b47826e86343e368a5c00f1a4b1f2bce/compiler/GHC/Tc/Types/Origin.hs#L57-92) data type defines a context for TH brackets:
```hs
data UserTypeCtxt
= ...
| ThBrackCtxt -- Template Haskell type brackets [t| ... |]
| ...
```
However, this does not appear to actually be used anywhere and can be removed relatively easily:
<details>
```diff
diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs
index 3a1ab09c9b..e81a87c3a8 100644
--- a/compiler/GHC/Tc/Gen/HsType.hs
+++ b/compiler/GHC/Tc/Gen/HsType.hs
@@ -2831,7 +2831,6 @@ expectedKindInCtxt :: UserTypeCtxt -> ContextKind
-- Depending on the context, we might accept any kind (for instance, in a TH
-- splice), or only certain kinds (like in type signatures).
expectedKindInCtxt (TySynCtxt _) = AnyKind
-expectedKindInCtxt ThBrackCtxt = AnyKind
expectedKindInCtxt (GhciCtxt {}) = AnyKind
-- The types in a 'default' decl can have varying kinds
-- See Note [Extended defaults]" in GHC.Tc.Utils.Env
diff --git a/compiler/GHC/Tc/Types/Origin.hs b/compiler/GHC/Tc/Types/Origin.hs
index b2fdefa4cd..cc63f7a5c5 100644
--- a/compiler/GHC/Tc/Types/Origin.hs
+++ b/compiler/GHC/Tc/Types/Origin.hs
@@ -92,7 +92,6 @@ data UserTypeCtxt
-- True: stand-alone deriving
-- False: vanilla instance declaration
| SpecInstCtxt -- SPECIALISE instance pragma
- | ThBrackCtxt -- Template Haskell type brackets [t| ... |]
| GenSigCtxt -- Higher-rank or impredicative situations
-- e.g. (f e) where f has a higher-rank type
-- We might want to elaborate this
@@ -136,7 +135,6 @@ pprUserTypeCtxt (StandaloneKindSigCtxt n) = text "a standalone kind signature fo
pprUserTypeCtxt TypeAppCtxt = text "a type argument"
pprUserTypeCtxt (ConArgCtxt c) = text "the type of the constructor" <+> quotes (ppr c)
pprUserTypeCtxt (TySynCtxt c) = text "the RHS of the type synonym" <+> quotes (ppr c)
-pprUserTypeCtxt ThBrackCtxt = text "a Template Haskell quotation [t|...|]"
pprUserTypeCtxt PatSigCtxt = text "a pattern type signature"
pprUserTypeCtxt ResSigCtxt = text "a result type signature"
pprUserTypeCtxt (ForSigCtxt n) = text "the foreign declaration for" <+> quotes (ppr n)
diff --git a/compiler/GHC/Tc/Validity.hs b/compiler/GHC/Tc/Validity.hs
index fba45562b7..05dcb28643 100644
--- a/compiler/GHC/Tc/Validity.hs
+++ b/compiler/GHC/Tc/Validity.hs
@@ -372,7 +372,6 @@ checkValidType ctxt ty
ForSigCtxt _ -> rank1
SpecInstCtxt -> rank1
- ThBrackCtxt -> rank1
GhciCtxt {} -> ArbitraryRank
TyVarBndrKindCtxt _ -> rank0
@@ -500,7 +499,6 @@ vdqAllowed :: UserTypeCtxt -> Bool
vdqAllowed (KindSigCtxt {}) = True
vdqAllowed (StandaloneKindSigCtxt {}) = True
vdqAllowed (TySynCtxt {}) = True
-vdqAllowed (ThBrackCtxt {}) = True
vdqAllowed (GhciCtxt {}) = True
vdqAllowed (TyVarBndrKindCtxt {}) = True
vdqAllowed (DataKindCtxt {}) = True
@@ -1333,7 +1331,6 @@ okIPCtxt ResSigCtxt = True
okIPCtxt GenSigCtxt = True
okIPCtxt (ConArgCtxt {}) = True
okIPCtxt (ForSigCtxt {}) = True -- ??
-okIPCtxt ThBrackCtxt = True
okIPCtxt (GhciCtxt {}) = True
okIPCtxt SigmaCtxt = True
okIPCtxt (DataTyCtxt {}) = True
```
</details>
Is there a good reason to keep this around?https://gitlab.haskell.org/ghc/ghc/-/issues/18704GHC could not deduce constraint from itself2021-10-14T08:52:11ZrybochodonezzarGHC could not deduce constraint from itself## Summary
following code:
```haskell
{-# LANGUAGE GADTs, DataKinds, PolyKinds, ConstraintKinds, TypeApplications, RankNTypes, TypeFamilies, TypeOperators, MultiParamTypeClasses, UndecidableSuperClasses, FlexibleInstances, PatternSynon...## Summary
following code:
```haskell
{-# LANGUAGE GADTs, DataKinds, PolyKinds, ConstraintKinds, TypeApplications, RankNTypes, TypeFamilies, TypeOperators, MultiParamTypeClasses, UndecidableSuperClasses, FlexibleInstances, PatternSynonyms, FlexibleContexts, AllowAmbiguousTypes, ScopedTypeVariables #-}
module Lib where
import GHC.Exts
import GHC.TypeLits
import Data.Proxy
data a ::: b = a ::: b
class Pair f where
type Left f :: a
type Right f :: b
instance Pair (a '::: b) where
type Left (a '::: b) = a
type Right (a '::: b) = b
class NC (x :: k)
instance NC (x :: k)
data L1 c f xs where
LC :: c x => f x -> L1 c f xs -> L1 c f (x ': xs)
LN :: L1 c f '[]
class (c1 (Left f), c2 (Right f)) => PairC c1 c2 f
instance (c1 x, c2 y) => PairC c1 c2 (x '::: y)
data f1 :*: f2 :: (kx ::: ky) -> * where
(:*:) :: f1 x -> f2 y -> (f1 :*: f2) (x '::: y)
pairC :: forall c1 c2 x y e . (c1 x, c2 y) => (PairC c1 c2 (x '::: y) => e) -> e
pairC e = e
type Foo t = L1 (PairC KnownSymbol NC) (Proxy :*: t)
pattern Foo :: forall s a t xs . KnownSymbol s => KnownSymbol s => Proxy s -> t a -> Foo t xs -> Foo t (s '::: a ': xs)
pattern Foo p t xs <- LC (p :*: t) xs where
Foo p t xs = pairC @KnownSymbol @NC @s @a (LC (p :*: t) xs)
```
Results in this compile error:
```
/home/ryba/ghc-bug/src/Lib.hs:38:46: error:
• Could not deduce (PairC KnownSymbol NC (s '::: a))
arising from a use of ‘LC’
from the context: KnownSymbol s
bound by the signature for pattern synonym ‘Foo’
at src/Lib.hs:(37,1)-(38,61)
or from: PairC KnownSymbol NC (s '::: a)
bound by a type expected by the context:
PairC KnownSymbol NC (s '::: a) =>
L1 (PairC KnownSymbol NC) (Proxy :*: t) ((s '::: a) : xs)
at src/Lib.hs:38:45-61
• In the fifth argument of ‘pairC’, namely ‘(LC (p :*: t) xs)’
In the expression: pairC @KnownSymbol @NC @s @a (LC (p :*: t) xs)
In an equation for ‘Foo’:
Foo p t xs = pairC @KnownSymbol @NC @s @a (LC (p :*: t) xs)
|
38 | Foo p t xs = pairC @KnownSymbol @NC @s @a (LC (p :*: t) xs)
| ^^^^^^^^^^^^^^^
```
Which basically boils down to "could not deduce a from a"
## Environment
* GHC version used: 8.10.2
* stack resolver=nightly-2020-09-14
Optional:
* Operating System: Ubuntu
* System Architecture: x86-64https://gitlab.haskell.org/ghc/ghc/-/issues/18689Why check for -fdefer-type-errors in metaTyVarUpdateOK?2020-12-22T13:22:39ZRichard Eisenbergrae@richarde.devWhy check for -fdefer-type-errors in metaTyVarUpdateOK?Function `checkTypeEq` changes its behavior depending on the presence of `-fdefer-type-errors` in an obscure case around heterogeneous equalities; see the code in `go_co`. This is undocumented (in the code), and neither Simon nor I can f...Function `checkTypeEq` changes its behavior depending on the presence of `-fdefer-type-errors` in an obscure case around heterogeneous equalities; see the code in `go_co`. This is undocumented (in the code), and neither Simon nor I can figure out why it's done.
Task: figure this out, and either document or remove this behavior.Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/18645Incremental `tcCheckSatisfiability` API2021-07-26T09:54:10ZSebastian GrafIncremental `tcCheckSatisfiability` APIThe pattern-match checker makes use of the function `tcCheckSatisfiability :: Bag EvVar -> TcM Bool` (henceforth `tcCS`) offered by the type-checker to solve type constraints. Over the course of a pattern-match checking session, such a `...The pattern-match checker makes use of the function `tcCheckSatisfiability :: Bag EvVar -> TcM Bool` (henceforth `tcCS`) offered by the type-checker to solve type constraints. Over the course of a pattern-match checking session, such a `Bag EvVar` is accumulated and incrementally checked after each addition. As #17836 shows in a rather painful way, that scales quadratically, because the type-checker chews through the same type constraints over and over again.
But look at how the pattern-match checker uses `tcCS`:
```hs
-- | Add some extra type constraints to the 'TyState'; return 'Nothing' if we
-- find a contradiction (e.g. @Int ~ Bool@).
tyOracle :: TyState -> Bag PredType -> DsM (Maybe TyState)
tyOracle (TySt inert) cts
= do { evs <- traverse nameTyCt cts
; let new_inert = inert `unionBags` evs
; ... <- initTcDsForSolver $ tcCheckSatisfiability new_inert
; ... }
```
The `inert` set is a `Bag EvVar` for which *we already know they are compatible with each other*, as they were checked by `tcCS` in a previous call. Only `cts :: Bag PredType` are unchecked. And as far as the pattern-match checker is concerned, the type of `inert` is completely opaque, so the API to `tcCS` could very well be
```hs
tcCheckSatisfiability :: TcInert -> Bag EvVar -> TcM (Maybe TcInert)
-- | Add some extra type constraints to the 'TyState'; return 'Nothing' if we
-- find a contradiction (e.g. @Int ~ Bool@).
tyOracle :: TyState -> Bag PredType -> DsM (Maybe TyState)
tyOracle (TySt inert) cts
= do { evs <- traverse nameTyCt cts
; ...mb_new_inert... <- initTcDsForSolver $ tcCheckSatisfiability inert evs
; ... }
```
I'm sure there already is something like `TcInert` in the type-checker. Looking at the implementation of `tcCS`, that might be the unused `EvBindMap`, but I'm not sure. Or is it the `InertCans` in `getInertCans`/`setInertCans`? CC @rae, @RyanGlScott, @simonpj
This blocks #17836 and would probably lead to quite a few (possibly rather drastic) metric decreases in other cases.https://gitlab.haskell.org/ghc/ghc/-/issues/18542Kind error when using partial type signatures2020-08-06T21:34:14Zlennart@augustsson.netKind error when using partial type signatures## Summary
When using a partial type signature I get a kind error, which is surprising.
## Steps to reproduce
Compile the following module. The function bar type checks, whereas baz gets a kind error
```
{-# LANGUAGE RankNTypes #-}...## Summary
When using a partial type signature I get a kind error, which is surprising.
## Steps to reproduce
Compile the following module. The function bar type checks, whereas baz gets a kind error
```
{-# LANGUAGE RankNTypes #-}
module Bug where
foo :: (Functor g) =>
(forall aa . Num aa => f aa -> g aa) ->
f a -> g (f a)
foo f x = undefined
bar :: (forall aa . Num aa => f aa -> Int -> aa) ->
f a -> Int -> f a
bar f = foo f
baz :: (forall aa . Num aa => f aa -> Int -> aa) ->
f a -> _ -> f a
baz f = foo f
```
## Environment
* GHC version used:
The Glorious Glasgow Haskell Compilation System, version 8.10.19.2.1https://gitlab.haskell.org/ghc/ghc/-/issues/18529GHC fails to infer type with FlexibleContexts2022-09-06T11:38:40ZRichard Eisenbergrae@richarde.devGHC fails to infer type with FlexibleContextsIf I say
```hs
{-# LANGUAGE MultiParamTypeClasses, FlexibleContexts #-}
module Bug where
class C a b where
op :: a -> b -> ()
-- foo :: (C a Integer) => a -> ()
foo x = op x 3
```
then GHC complains that the variable `b0` in the t...If I say
```hs
{-# LANGUAGE MultiParamTypeClasses, FlexibleContexts #-}
module Bug where
class C a b where
op :: a -> b -> ()
-- foo :: (C a Integer) => a -> ()
foo x = op x 3
```
then GHC complains that the variable `b0` in the type of `foo` is ambiguous, because it tries to produce `C a b => a -> ()` as the type of `foo`. Instead, it shouldn't quantify `b`, letting it default to `Integer`.
The solution is to use `oclose` instead of `growThetaTyVars` in `decideQuantifiedTyVars`. This will respect functional dependencies, quantifying over `b` only when a fundep exists from `a` to `b`.
I will fix in ongoing work (in the `wip/derived-refactor` branch).Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/18481Improve instantiation of datacons2022-04-12T17:01:42ZKrzysztof GogolewskiImprove instantiation of dataconsThis ticket tracks a possible improvement to `return_data_con`.
When typechecking a datacon `T`, do we instantiate its arguments? We'd like to avoid instantiation, because it breaks VTA.
Currently, we instantiate levity-polymorphic con...This ticket tracks a possible improvement to `return_data_con`.
When typechecking a datacon `T`, do we instantiate its arguments? We'd like to avoid instantiation, because it breaks VTA.
Currently, we instantiate levity-polymorphic constructors. Quoting Note [Linear fields generalization]:
```
A small hitch: if the constructor is levity-polymorphic (unboxed tuples, sums,
certain newtypes with -XUnliftedNewtypes) then this strategy produces
\r1 r2 a b (x # p :: a) (y # q :: b) -> (# a, b #)
Which has type
forall r1 r2 a b. a #p-> b #q-> (# a, b #)
Which violates the levity-polymorphism restriction see Note [Levity polymorphism
checking] in DsMonad.
So we really must instantiate r1 and r2 rather than quantify over them. For
simplicity, we just instantiate the entire type, as described in Note
[Instantiating stupid theta]. It breaks visible type application with unboxed
tuples, sums and levity-polymorphic newtypes, but this doesn't appear to be used
anywhere.
A better plan: let's force all representation variable to be *inferred*, so that
they are not subject to visible type applications. Then we can instantiate
inferred argument eagerly.
```
The goal of this ticket is to implement the last paragraph.