GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2022-10-25T22:38:55Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/21100New wording for error message around associated type families2022-10-25T22:38:55ZRichard Eisenbergrae@richarde.devNew wording for error message around associated type familiesIn https://github.com/haskell/error-messages/issues/13, several of us converged on taking the existing error message
```
Assoc.hs:20:8: error:
‘Genome’ is not a (visible) associated type of class ‘Reproductive’
|
20 | type Geno...In https://github.com/haskell/error-messages/issues/13, several of us converged on taking the existing error message
```
Assoc.hs:20:8: error:
‘Genome’ is not a (visible) associated type of class ‘Reproductive’
|
20 | type Genome a = (Strand a, Strand a)
|
```
and changing it to become
```
Assoc.hs:20:8: error:
A default equation for `Genome` was found, but `Genome` has not been declared.
You can declare the associated type `Genome` by adding:
type Genome a
to the class `Reproductive` in addition to the default equation:
type Genome a = (Strand a, Strand a)
|
20 | type Genome a = (Strand a, Strand a)
|
```
Input:
```hs
{-# LANGUAGE TypeFamilies #-}
class Reproductive a where
-- | A sequence of genetic information for an agent.
type Strand a
-- | Full set (both strands) of genetic information for an organism.
type Genome a = (Strand a, Strand a)
```https://gitlab.haskell.org/ghc/ghc/-/issues/21099GHC does not rewrite in FunTy, part II2022-02-22T15:22:26Zsheafsam.derbyshire@gmail.comGHC does not rewrite in FunTy, part II@rae observed that GHC failed to rewrite kinds in `FunTy` in #19677, and he fixed the issue in MR !2477 by ensuring that in the rewriter, when rewriting `FunTy`, we also rewrite the kinds. See `GHC.Tc.Solver.Rewrite.rewrite_one (FunTy .....@rae observed that GHC failed to rewrite kinds in `FunTy` in #19677, and he fixed the issue in MR !2477 by ensuring that in the rewriter, when rewriting `FunTy`, we also rewrite the kinds. See `GHC.Tc.Solver.Rewrite.rewrite_one (FunTy ...)`.
However, there are other places in the compiler where we rewrite a `FunTy`, but which have not been adapted:
1. `GHC.Core.FamInstEnv.normalise_type`,
2. `GHC.Tc.Solver.Monad.breakTyVarCycle_maybe`.
It seems to me that we should be consistent and do the same thing in these other places.Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/21098Report an error when applying a type family associated with a class to a type...2023-12-17T22:07:48ZMarioReport an error when applying a type family associated with a class to a type that's not an instance of the class## Summary
I wasted at least an hour on this issue, which I originally reported at https://github.com/well-typed/generics-sop/issues/152 . I'm reporting it here as suggested because I can't be the only GHC user dumb enough to be confuse...## Summary
I wasted at least an hour on this issue, which I originally reported at https://github.com/well-typed/generics-sop/issues/152 . I'm reporting it here as suggested because I can't be the only GHC user dumb enough to be confused by the behaviour.
Trying to apply a *class method* to a value whose type is an instance of the type class results in an understandable error message
> No instance for YourType arising from a use of theMethod
Trying to apply an *associated type family* to a type that's not an instance of the type class, in contrast, does not result in any error message by itself: the application will simply remain stuck.
## Steps to reproduce
```
GHCi, version 8.10.7: https://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /tmp/haskell-stack-ghci/2a3bbd58/ghci-script
Prelude> :module + Generics.SOP Generics.SOP.GGP
Prelude Generics.SOP Generics.SOP.GGP> :set -XDeriveGeneric
Prelude Generics.SOP Generics.SOP.GGP> newtype N = N Int deriving GHC.Generics.Generic
Prelude Generics.SOP Generics.SOP.GGP> :k! Code N
Code N :: [[*]]
= Code N
Prelude Generics.SOP Generics.SOP.GGP> :k! GCode N
GCode N :: [[*]]
= '[ '[Int]]
```
## Expected behavior
A clear error message like
> No instance for (Generic N) arising from a use of ‘Code’
## Environment
* GHC version used: 8.10.7 and 9.2.1https://gitlab.haskell.org/ghc/ghc/-/issues/21088Inconsistent instantiation of inferred type variables when they don't all com...2022-03-03T08:25:55Zsheafsam.derbyshire@gmail.comInconsistent instantiation of inferred type variables when they don't all come firstCurrently, in `GHC.Tc.Gen.App.tcInstFun`, when we are instantiating inferred type variables (for example for `:type` in GHCi), we instantiate only the inferred type variables that appear before any other quantified type variables.
Examp...Currently, in `GHC.Tc.Gen.App.tcInstFun`, when we are instantiating inferred type variables (for example for `:type` in GHCi), we instantiate only the inferred type variables that appear before any other quantified type variables.
Example:
```haskell
{r1 :: RuntimeRep} (a :: TYPE r1) {r2 :: RuntimeRep} (b :: TYPE r2)
```
Here we will instantiate `r1`, but not `r2` because `r2` comes after `a` which we are not instantiating because `a` is not an inferred type variable (recall that we are in the case in which `inst_fun = inst_inferred`). This means that `:type` in GHCi could end up reporting a type like
```haskell
forall a {r2 :: RuntimeRep} (b :: TYPE r2)
```
This is just too confusing, in my opinion.
How to fix this?
1. Initially I thought we might make an effort to re-arrange the type variables and still instantiate `r2` even though it appears after `a`. However, as this isn't possible in general (e.g. if the kind of `r2` mentioned `a`, we wouldn't be able to re-arrange the telescope), and @rae dissuaded me from pursuing it further.
2. @mpickering instead suggested that we don't instantiate any inferred type variables when we run into such a situation. This is what I will be pursuing; it only entails adding a single additional check that there are no more splittable quantified variables (in `GHC.Tc.Gen.App.tcInstFun.go1`).sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/21077GHC 9.2.1 typechecking regression with RankNTypes, TemplateHaskell, and compo...2023-08-04T17:02:49ZRyan ScottGHC 9.2.1 typechecking regression with RankNTypes, TemplateHaskell, and compound expressions_(Originally spun off from https://gitlab.haskell.org/ghc/ghc/-/issues/21038#note_407457)_
The `crux-llvm` library (specifically, [this code](https://github.com/GaloisInc/crucible/blob/e1308319eef8e0fcb55ed04df7eb2e9d5e87aac5/crux-llvm/..._(Originally spun off from https://gitlab.haskell.org/ghc/ghc/-/issues/21038#note_407457)_
The `crux-llvm` library (specifically, [this code](https://github.com/GaloisInc/crucible/blob/e1308319eef8e0fcb55ed04df7eb2e9d5e87aac5/crux-llvm/src/Crux/LLVM/Overrides.hs#L149-L153)) typechecks on GHC 9.0.2 and earlier, but fails to typecheck with GHC 9.2.1. I made an attempt to minimize the issue in #21038, but after trying again with that patch, I discovered that `crux-llvm` _still_ does not typecheck. It turns out that my minimization of the issue was a bit too minimal. Here is an example that better illustrates what is going on:
```hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TemplateHaskell #-}
module Bug where
data Foo = MkFoo () (forall a. a -> a)
worksOnAllGHCs1 :: Foo
worksOnAllGHCs1 = MkFoo () (\x -> x)
worksOnAllGHCs2 :: Foo
worksOnAllGHCs2 = MkFoo () $ \x -> x
worksOnAllGHCs42 :: Foo
worksOnAllGHCs42 = (MkFoo ()) $ \x -> x
doesn'tWorkOnGHC9'2 :: Foo
doesn'tWorkOnGHC9'2 = $([| MkFoo () |]) $ \x -> x
```
As the names suggest, all of the things functions will typecheck on GHC 9.0.2 and earlier. The `worksOnAllGHCs{1,2,3}` functions will typecheck on GHC 9.2.1, but `doesn'tWorkOnGHC9'2` will not:
```
$ ghc-9.2.1 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o, Bug.dyn_o )
Bug.hs:17:24: error:
• Couldn't match type: forall a. a -> a
with: p0 -> p0
Expected: (p0 -> p0) -> Foo
Actual: (forall a. a -> a) -> Foo
• In the first argument of ‘($)’, namely ‘(MkFoo ())’
In the expression: (MkFoo ()) $ \ x -> x
In an equation for ‘doesn'tWorkOnGHC9'2’:
doesn'tWorkOnGHC9'2 = (MkFoo ()) $ \ x -> x
|
17 | doesn'tWorkOnGHC9'2 = $([| MkFoo () |]) $ \x -> x
| ^^^^^^^^^^^^^^^^
```
The commit which introduced this regression is 9632f413dc90f39bc64586c064805f515a672ca0 (`Implement Quick Look impredicativity`).
Note that unlike the example in #21038, the expression being spliced isn't a simple identifier (i.e., a "head", to use Quick Look terminology), but rather a compound expression. @simonpj suggests [the following fix](https://gitlab.haskell.org/ghc/ghc/-/issues/21038#note_407705):
> Ah yes. Hmm. Reflecting on this, I think the Right Thing is *to treat a splice that is run in the renamer (i.e. an untyped TH splice) as using the "HsExpansion" mechanism*. See `Note [Handling overloaded and rebindable constructs]` in GHC.Tc.Rename.Expr.
>
> That is, the splice `$(expr)` turns into `HsExpanded $(expr) <result-of-running-splice>`. After all, it really *is* an expansion! Then the stuff in the type checker will deal smoothly with application chains. See `Note [Looking through HsExpanded]` in GHC.Tc.Gen.Head.
>
> In principle that should be pretty easy. But `Note [Delaying modFinalizers in untyped splices]` in GHC.Rename.Splice is a painful wart that will hurt us here.
>
> * Where might we store these modFinalizdrs in the HsExpanded? Maybe in the first (original expression) field?
> * Actually I think I favour separating them out entirely into a new extension constructor for `HsExpr GhcRn`. Currenlty we have
>
> ```
> type instance XXExpr GhcRn = HsExpansion (HsExpr GhcRn) (HsExpr GhcRn)
> type instance XXExpr GhcTc = XXExprGhcTc
> ```
>
> We could instead have
>
> ```
> type instance XXExpr GhcRn = XXExprGhcRn
>
> data XXExprGhcRn = ExpansionRn (HsExpansion (HsExpr GhcRn) (HsExpr GhcRn))
> | AddModFinalizedrs ThModFinalizers (HsExpr GhcRn)
> ```
>
> In exchange we can get rid of `HsSpliced` altogether.
> * We still need to call `addModFinalizersWithLclEnv` on those finalisers; so it looks as if we'd need to make `splitHsApps` monadic. That's a pain, but not actually difficult.
>
> I'm not certain of this. But *something* along these lines seems like the right solution.Ryan ScottRyan Scotthttps://gitlab.haskell.org/ghc/ghc/-/issues/21041Check laziness of Coercion in the Reduction type2023-12-04T15:08:50ZRichard Eisenbergrae@richarde.devCheck laziness of Coercion in the Reduction typeThe `Coercion` stored in a `Reduction` is lazy in order to work with Derived constraints. However, once !5899 lands, Derived constraints will be a part of history. We should then check to see if making this coercion strict would yield a ...The `Coercion` stored in a `Reduction` is lazy in order to work with Derived constraints. However, once !5899 lands, Derived constraints will be a part of history. We should then check to see if making this coercion strict would yield a performance improvement.https://gitlab.haskell.org/ghc/ghc/-/issues/21040Curious kind-checking failure with GHC 9.2.1 and visible dependent quantifica...2022-02-04T14:33:59ZRyan ScottCurious kind-checking failure with GHC 9.2.1 and visible dependent quantificationWhile porting some code over to GHC 9.2.1 recently, I noticed an unusual quirk in the way kind inference interacts with visible dependent quantification. Consider these two modules:
```hs
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTyp...While porting some code over to GHC 9.2.1 recently, I noticed an unusual quirk in the way kind inference interacts with visible dependent quantification. Consider these two modules:
```hs
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneKindSignatures #-}
module A where
import Data.Kind
type T1 :: Type -> Type
data T1 a = MkT1
t1FunA :: (forall a. T1 a -> r) -> r
t1FunA g = g MkT1
t1FunB :: T1 a -> T1 a -> ()
t1FunB _ _ = ()
type T2 :: forall (a :: Type) -> Type
data T2 a = MkT2
t2FunA :: (forall a. T2 a -> r) -> r
t2FunA g = g MkT2
t2FunB :: T2 a -> T2 a -> ()
t2FunB _ _ = ()
```
```hs
{-# LANGUAGE NoPolyKinds #-}
module B where
import A
g1 :: ()
g1 = t1FunA $ \x ->
let y = MkT1
in t1FunB x y
g2 :: ()
g2 = t2FunA $ \x ->
let y = MkT2
in t2FunB x y
```
The `A` module defines two data types, `T1` and `T2`, as well as some functions which use them. The only difference between `T1` and `T2` is that the latter uses visible dependent quantification while the former does not. The `B` module uses these functions in a relatively straightforward way. Note that `B` does _not_ enable `PolyKinds` (I distilled this from a `cabal` project which uses `Haskell2010`).
What's curious about this is that while both `g1` and `g2` will typecheck on GHC 9.0.2, only `g1` typechecks on GHC 9.2.1. On the other hand, `g2` will fail to typecheck in GHC 9.2.1:
```
$ ghc-9.2.1 B.hs
[1 of 2] Compiling A ( A.hs, A.o )
[2 of 2] Compiling B ( B.hs, B.o )
B.hs:14:18: error:
• Couldn't match type ‘a’ with ‘*’
Expected: T2 a
Actual: T2 (*)
‘a’ is a rigid type variable bound by
a type expected by the context:
forall a. T2 a -> ()
at B.hs:(12,15)-(14,18)
• In the second argument of ‘t2FunB’, namely ‘y’
In the expression: t2FunB x y
In the expression: let y = MkT2 in t2FunB x y
• Relevant bindings include x :: T2 a (bound at B.hs:12:16)
|
14 | in t2FunB x y
| ^
```
I'm not confident enough to claim with 100% certainty that this is a regression, since the use of `NoPolyKinds` might be throwing a wrench into things. Indeed, enabling `PolyKinds` is enough to make the program accepted again. Still, the fact that this _only_ fails if the data type uses visible dependent quantification (and _only_ with GHC 9.2.1) is rather strange, so I wanted to file an issue to ask people more knowledgeable in this space than I am.https://gitlab.haskell.org/ghc/ghc/-/issues/21038GHC 9.2.1 typechecking regression with RankNTypes and TemplateHaskell2022-02-14T13:59:23ZRyan ScottGHC 9.2.1 typechecking regression with RankNTypes and TemplateHaskellWhile porting some code over to use GHC 9.2.1, I noticed a typechecking regression that doesn't appear to be explained in the 9.2.1 release notes. Here is a minimal example:
```hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TemplateHaskell...While porting some code over to use GHC 9.2.1, I noticed a typechecking regression that doesn't appear to be explained in the 9.2.1 release notes. Here is a minimal example:
```hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TemplateHaskell #-}
module Bug where
data Foo = MkFoo (forall a. a -> a)
worksOnAllGHCs1 :: Foo
worksOnAllGHCs1 = MkFoo (\x -> x)
worksOnAllGHCs2 :: Foo
worksOnAllGHCs2 = MkFoo $ \x -> x
worksOnAllGHCs3 :: Foo
worksOnAllGHCs3 = $([| MkFoo |]) (\x -> x)
doesn'tWorkOnGHC9'2 :: Foo
doesn'tWorkOnGHC9'2 = $([| MkFoo |]) $ \x -> x
```
All four of these top-level functions will typecheck on GHC 9.0.2 and earlier. On GHC 9.2.1 and HEAD, `worksOnAllGHCs{1,2,3}` functions will typecheck, but the `doesn'tWorkOnGHC9'2` function will not typecheck:
```
$ ghc-9.2.1 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o, Bug.dyn_o )
Bug.hs:17:24: error:
• Couldn't match type: forall a. a -> a
with: p0 -> p0
Expected: (p0 -> p0) -> Foo
Actual: (forall a. a -> a) -> Foo
• In the first argument of ‘($)’, namely ‘(MkFoo)’
In the expression: (MkFoo) $ \ x -> x
In an equation for ‘doesn'tWorkOnGHC9'2’:
doesn'tWorkOnGHC9'2 = (MkFoo) $ \ x -> x
|
17 | doesn'tWorkOnGHC9'2 = $([| MkFoo |]) $ \x -> x
| ^^^^^^^^^^^^^
```
I'm unclear why using a Template Haskell splice would affect typechecking like this, so I believe this is a bug.9.2.2Ryan ScottRyan Scotthttps://gitlab.haskell.org/ghc/ghc/-/issues/21024A deferred type error inferferes with the monomorphism restriction2022-06-09T14:31:57ZRichard Eisenbergrae@richarde.devA deferred type error inferferes with the monomorphism restrictionHere is a fairly simple program:
```
{-# OPTIONS_GHC -fdefer-type-errors #-}
module Bug where
other = ['a', True]
x = 5
```
The monomorphism restriction is in effect, and note that the two definitions do not refer to each other.
GH...Here is a fairly simple program:
```
{-# OPTIONS_GHC -fdefer-type-errors #-}
module Bug where
other = ['a', True]
x = 5
```
The monomorphism restriction is in effect, and note that the two definitions do not refer to each other.
GHC embarrassingly infers the type `Any` for `x`, affected by the presence of the ill-typed `other`.https://gitlab.haskell.org/ghc/ghc/-/issues/21023MonoLocalBinds sometimes monomorphises *global* binds2022-03-07T22:09:56ZRichard Eisenbergrae@richarde.devMonoLocalBinds sometimes monomorphises *global* bindsHere is a fairly simple program:
```hs
{-# LANGUAGE MonoLocalBinds #-}
module Bug where
x = 5
f y = (x, y)
```
Important: the monomorphism restriction is in effect.
GHC embarrassingly infers the type `Any -> (Integer, Any)` for `f`...Here is a fairly simple program:
```hs
{-# LANGUAGE MonoLocalBinds #-}
module Bug where
x = 5
f y = (x, y)
```
Important: the monomorphism restriction is in effect.
GHC embarrassingly infers the type `Any -> (Integer, Any)` for `f`. This is because `f`'s right-hand side mentions `x`, whose type is not yet known. (The monomorphism restriction means it's type is not `Num a => a`.) So, GHC chooses the `NoGen` plan for generalization. With nothing to say what the type of `y` should be, GHC picks `Any`. Bad GHC, bad. Giving `x` a type signature or disabling the monomorphism restriction fixes the problem.
I think the solution is simply never to do `NoGen` for top-level bindings.Simon Peyton JonesSimon Peyton Joneshttps://gitlab.haskell.org/ghc/ghc/-/issues/21020GHC fails to quantify over a quantifiable equality constraint2022-09-06T11:37:31ZRichard Eisenbergrae@richarde.devGHC fails to quantify over a quantifiable equality constraintConsider
```hs
{-# LANGUAGE TypeFamilies, NoMonoLocalBinds #-}
module NoMonoLocal where
type family F a
inject :: a -> F a
inject = undefined
f x = let g y = [x, inject y] in (g 'x', g True)
```
I think this should work, but GHC re...Consider
```hs
{-# LANGUAGE TypeFamilies, NoMonoLocalBinds #-}
module NoMonoLocal where
type family F a
inject :: a -> F a
inject = undefined
f x = let g y = [x, inject y] in (g 'x', g True)
```
I think this should work, but GHC rejects, failing to infer a polymorphic type for `g`.
(Red herring: `NoMonoLocalBinds`. If it helps, imagine the declaration for `F` to occur in another module. The definition for `f` does *not* require `-XTypeFamilies` or `-XMonoLocalBinds` to be enabled.)
The problem is in inferring the type of `g`. Suppose `x :: alpha[1]` and `y :: beta[2]`. We get
```
[W] F beta[2] ~ alpha[1]
```
I would expect, then, for GHC to infer `g :: forall b. (F b ~ a) => b -> [a]`, where `a` is the type of `x` (from an outer scope). Note that GHC *does* allow quantification over equalities of this shape.
The problem is that the `touchabilityTest`, when looking at that Wanted, concludes `TouchableOuterLevel`: that is, GHC wants to say `alpha[1] := F beta[2]`. Of course, this violates the level invariant, and so GHC promotes `beta[2]` to `beta'[1]` first (and then unifies). When it comes around to deciding the quantified type variables for `g`, `beta'[1]` is now at an outer level and is not quantified. It eventually gets monomorphised to `Char` -- not what we want.
I think `touchabilityTest` should not try to unify variables from outer levels when the RHS has an inner level.
Interestingly, even if this immediate bug is fixed, GHC will *still* reject, because of #20668. So perhaps it makes sense to hold off here until #20668 is fixed, but I claim this is a separable problem.https://gitlab.haskell.org/ghc/ghc/-/issues/21010ASSERTION failure when building subcategories2022-02-08T11:01:59ZMatthew PickeringASSERTION failure when building subcategories```
[ 5 of 13] Compiling Control.Subcategory.Bind ( src/Control/Subcategory/Bind.hs, dist/build/Control/Subcategory/Bind.o, dist/build/Control/Subcategory/Bind.dyn_o )
<no location info>: error:
ASSERT failed!
CallStack (from HasC...```
[ 5 of 13] Compiling Control.Subcategory.Bind ( src/Control/Subcategory/Bind.hs, dist/build/Control/Subcategory/Bind.o, dist/build/Control/Subcategory/Bind.dyn_o )
<no location info>: error:
ASSERT failed!
CallStack (from HasCallStack):
massert, called at compiler/GHC/Tc/Solver/Canonical.hs:2485:10 in ghc:GHC.Tc.Solver.Canonical
```
Which is this assertion in `GHC.Tc.Solver.Canonical.canEqCanLHSFinish`.
```
-- by now, (TyEq:N) is already satisfied (if applicable)
; massert (not bad_newtype)
```
Standalone repro: https://gist.github.com/540cf5453a26825e6885ad59cb01957a
Run using `./run`
```
[nix-shell:~/subcategories-0.1.1.0/repro]$ ./run
[1 of 4] Compiling MonoTraversable ( MonoTraversable.hs, out/MonoTraversable.o, out/MonoTraversable.dyn_o )
[2 of 4] Compiling Internal ( Internal.hs, out/Internal.o, out/Internal.dyn_o )
[3 of 4] Compiling BindA ( BindA.hs, out/BindA.o, out/BindA.dyn_o )
[4 of 4] Compiling Bind ( Bind.hs, out/Bind.o, out/Bind.dyn_o )
<no location info>: error:
ASSERT failed!
CallStack (from HasCallStack):
massert, called at compiler/GHC/Tc/Solver/Canonical.hs:2485:10 in ghc:GHC.Tc.Solver.Canonical
```https://gitlab.haskell.org/ghc/ghc/-/issues/21006Unhelpful Kind equality error at the start of file2022-01-28T10:50:09ZJkensikUnhelpful Kind equality error at the start of fileI get an error
```
app\Main.hs:1:1: error:
Couldn't match kind `*' with `Constraint'
When matching types
b :: *
(Set b, Set s) :: Constraint
|
1 | {-# LANGUAGE TypeFamilies #-}
| ^
```
I don't know why b and the ...I get an error
```
app\Main.hs:1:1: error:
Couldn't match kind `*' with `Constraint'
When matching types
b :: *
(Set b, Set s) :: Constraint
|
1 | {-# LANGUAGE TypeFamilies #-}
| ^
```
I don't know why b and the constraint (Set b, Set s) are being matched? I would expect the constraint to existentially quantify the type b but why would it be matching them?
I believe the last thing I changed before getting the error was adding OpOutcome to the class.
here is the code
```
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE RankNTypes #-}
module Main where
import GHC.TypeLits (Symbol)
import GHC.Exts (Constraint)
import Data.Reflection (Reifies, reflect)
import Data.Proxy (Proxy(..))
main :: IO ()
main = print 5
class ((a,b)::Constraint) => HasCtxt a b
instance (a,b) => HasCtxt a b
class Determines a b | a -> b
instance Determines a b => Determines a b
type Set b = (b ~ b)
type OpLayout a = (forall s ctxt b. (OpCtxt a s b ~ ctxt, Determines a b, Determines a ctxt,Reifies s b) => ( HasCtxt ctxt (Reifies s b))) :: Constraint
data Stack a where
Cons :: OpConstructor a -> Stack b -> Stack a
Nil :: Stack "NIL"
class OpLayout a => OpCode (a::Symbol) where
type OpCtxt a s b = (ctxt :: Constraint) | ctxt -> s b
type OpOutcome a :: *
data OpConstructor a
opValue :: Determines a s => Proxy s
opValue = Proxy
popOP :: OpCtxt a s b => Stack a -> (b :: *)
evalOP :: OpConstructor a -> Stack x -> OpOutcome a
instance OpCode "load_val" where
type OpCtxt "load_val" s b = (Set s, Set b)
type OpOutcome "load_val" = Stack "load_val"
data OpConstructor "load_val" = forall b. LOAD_VAL b
popOP stack = reflect opValue
evalOP op stack = op `Cons` stack
```https://gitlab.haskell.org/ghc/ghc/-/issues/21000`isInjectiveTyCon` is overly pessimistic for type synonyms2022-01-26T12:26:12Zsheafsam.derbyshire@gmail.com`isInjectiveTyCon` is overly pessimistic for type synonymsWe currently have:
```haskell
isGenerativeTyCon :: TyCon -> Role -> Bool
isGenerativeTyCon (FamilyTyCon { famTcFlav = DataFamilyTyCon _ }) Nominal = True
isGenerativeTyCon (FamilyTyCon {}) _ = False
isGenerativeTyCon tc r ...We currently have:
```haskell
isGenerativeTyCon :: TyCon -> Role -> Bool
isGenerativeTyCon (FamilyTyCon { famTcFlav = DataFamilyTyCon _ }) Nominal = True
isGenerativeTyCon (FamilyTyCon {}) _ = False
isGenerativeTyCon tc r = isInjectiveTyCon tc r
isInjectiveTyCon :: TyCon -> Role -> Bool
-- ...
isInjectiveTyCon (SynonymTyCon {}) _ = False
-- ...
```
This seems wrong to me:
1. Shouldn't we directly set `isGenerativeTyCon (SynonymTyCon {}) = False`? It doesn't matter whether the type synonym ends up being injective or not, as it will not be generative regardless.
2. All type synonyms are considered "not injective" for `isInjectiveTyCon`. Maybe it's fine to be pessimistic like this (although the documentation of `isInjectiveTyCon` doesn't say that it might pessimistically return `False` when it's not sure), but it seems odd. Clearly `type T a = a` is injective.
Looking at where `isInjectiveTyCon` is used, it seems to always be after we expand type synonyms:
- `GHC.Core.Unify.unify_ty`
- `GHC.Core.Coercion.Opt.{opt_univ, etaTyConAppCo_maybe}`
- `GHC.Tc.Errors.eqInfoMsgs`
- `GHC.Tc.Solver.Canonical.canTyConApp` is only called from within `can_eq_nc'` after expanding type synonyms
- `GHC.Tc.Solver.Canonical.unify_derived`https://gitlab.haskell.org/ghc/ghc/-/issues/20981Error messages and constraints can easily be lost by accident2023-09-13T12:06:57ZSimon Peyton JonesError messages and constraints can easily be lost by accidentToday I rediscovered a nasty, subtle bug, which we have seen before: #19470
The problem is that in the typechecker we use this idiom quite a lot
```
do { (gbl_env, lcl_env) <- tcRnSrcDecls ...
; setGblEnv gbl_env $ setLclEnv lc...Today I rediscovered a nasty, subtle bug, which we have seen before: #19470
The problem is that in the typechecker we use this idiom quite a lot
```
do { (gbl_env, lcl_env) <- tcRnSrcDecls ...
; setGblEnv gbl_env $ setLclEnv lcl_env $
more_stuff }
```
The `tcRnSrcDecls` extends the environments in `gbl_env` and `lcl_env` which we then
want to be in scope in `more stuff`.
The problem is that `lcl_env :: TcLclEnv` has an IORef for error messages `tcl_errs`, and another for constraints (`tcl_lie`),a
and another for Linear Haskell usage information (`tcl_usage`). Now suppose we change it a tiny bit
```
do { (gbl_env, lcl_env) <- checkNoErrs $
tcRnSrcDecls ...
; setGblEnv gbl_env $ setLclEnv lcl_env $
more_stuff }
```
That should be innocuous. But *alas*, `checkNoErrs` gathers errors in a fresh IORef *which is then captured in the returned `lcl_env`. When we do the `setLclEnv` we'll make that captured IORef into the place where we gather error messages -- **but no one is going to look at that IORef any more**, so the errors are simply lost.
This was worked around in the fix to #19470, namely !5495. But it bit me in a different way today.
We should make a more general fix.Matthew PickeringMatthew Pickeringhttps://gitlab.haskell.org/ghc/ghc/-/issues/20974GHCi >= 9.2.1 prints type signatures containing type families in an ugly way2022-05-20T08:22:33ZAndrzej RybczakGHCi >= 9.2.1 prints type signatures containing type families in an ugly wayConsider the following:
```haskell
{-# LANGUAGE DataKinds, KindSignatures, TypeFamilies, TypeOperators #-}
import Data.Kind
class A (m :: Type -> Type)
class B (m :: Type -> Type)
type family F cs (m :: Type -> Type) :: Constraint wh...Consider the following:
```haskell
{-# LANGUAGE DataKinds, KindSignatures, TypeFamilies, TypeOperators #-}
import Data.Kind
class A (m :: Type -> Type)
class B (m :: Type -> Type)
type family F cs (m :: Type -> Type) :: Constraint where
F '[] m = ()
F (c : cs) m = (c m, F cs m)
test :: F [Monad, A, B] m => m ()
test = pure ()
```
The type signature of `test` is pretty-printed in GHCi 9.0.2 and lower:
```
$ ghci-9.0.2
GHCi, version 9.0.2: https://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/unknown/.ghci
>>> :l test
[1 of 1] Compiling Main ( test.hs, interpreted )
Ok, one module loaded.
>>> :t test
test :: (Monad m, A m, B m) => m ()
```
but this is what happens in 9.2.1 and HEAD:
```
$ ghci-9.2.1
GHCi, version 9.2.1: https://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/unknown/.ghci
>>> :l test.hs
[1 of 1] Compiling Main ( test.hs, interpreted )
Ok, one module loaded.
>>> :t test
test :: (Monad m, (A m, (B m, () :: Constraint))) => m ()
```
Looks much worse and I'd consider that a regression.9.2.2sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/20972Use ConcreteTv for metavariables that must only be unified with concrete types2022-04-14T20:54:50Zsheafsam.derbyshire@gmail.comUse ConcreteTv for metavariables that must only be unified with concrete typesCurrently, when we have a constraint of the form `Concrete# ty`, we have a separate evidence term in the form of a coercion hole `{co} :: ty #~ concrete_tv`, for some metavariable `concrete_tv`. This metavariable really belongs to this `...Currently, when we have a constraint of the form `Concrete# ty`, we have a separate evidence term in the form of a coercion hole `{co} :: ty #~ concrete_tv`, for some metavariable `concrete_tv`. This metavariable really belongs to this `Concrete#` constraint, and should not be unified with anything else. This isn't a problem in PHASE 1 of the FixedRuntimeRep plan outlined [on the wiki](https://gitlab.haskell.org/ghc/ghc/-/wikis/FixedRuntimeRep), because the metavariable `concrete_tv` never leaks out. However, once we start actually using the evidence for these constraints, we will insert casts into the typechecked program and suddenly it becomes possible for some other part of the typechecker to unify this metavariable. If we end up unifying with a non-concrete type (e.g. a type family application), then the whole exercise will have been for nought.
The plan to address this is to introduce a special kind of metavariable that can only be unified with concrete types, by adding a new field to `MetaInfo`, say `ConcreteTv`.
## Using ConcreteTv instead of Concrete# constraints
@simonpj then points out that, once we do this, then perhaps we no longer need the `Concrete#` special predicate at all, and could instead work directly with `ConcreteTv` metavariables. I've started thinking about this, here are a few observations:
### Phase 2 for free?
Using `ConcreteTv` directly allows us to re-use GHC's existing infrastructure for inserting casts in some circumstances, instead of manually having to insert them as described in the [FixedRuntimeRep wiki page](https://gitlab.haskell.org/ghc/ghc/-/wikis/FixedRuntimeRep#phase-2).
For example:
```haskell
f x = ... g x ...
g :: forall (a :: TYPE (F Int)). a -> ...
type family F a where
F Int = LiftedRep
```
When typechecking `f`, if we can set things up to have `x :: ty :: TYPE conc_tv` for `conc_tv` one of these `ConcreteTv` metavariables, then we've in very good shape. Indeed, then we will refuse to unify `conc_tv := F Int` because `F Int` is not concrete, but we will rewrite `conc_tv ~# F_Int` to `conc_tv ~# LiftedRep` and will unify `conc_tv := LiftedRep`. Then the rest of the machinery in `tcApp` will insert the necessary casts for the application `g x`.
The problem, as far as I see it, is that this optimistically assumes that the relevant metavariables are assigned `ConcreteTv` at birth. In this particular case I think we're OK: the first thing we see is `x` in a binding position but we otherwise know nothing about `x`, so it stands to reason that we can conjure up a `ConcreteTv` metavariable for its kind and go from there.
However, now that I look at where the existing `hasFixedRuntimeRep` checks take place, we might well instead come across a type first (and do some unification), and only later come across a situation which requires concreteness (e.g. it appears as the kind of a bound variable).
It seems plausible to me that we could end up in a situation where we have `x :: ty :: alpha` for a normal unification variable `alpha`, then we unify `alpha ~ F Int`, and then later on we come across e.g. `x` used in an application, realising too late "oh shoot, we should have made `alpha` a `ConcreteTv`!".
### Error messages
Currently, metavariables don't store any origin information. If we want to report informative representation-polymorphism error messages, we should add some origin information so that if we end up with an unfilled `ConcreteTv` metavariable we can report an appropriate error message.
### Re-using `~#`
It seems like we might benefit from re-using primitive equality. In particular, decomposition of `Concrete#` constraints is quite similar to decomposition for `~#`, so it seems to make sense.
When we come across a type `ty` that we must ensure is concrete, we create a new `ConcreteTv` metavariable `conc_tv` and directly emit `ty ~# conc_tv`. We can attach a `CtOrigin` just as before, so we still have the error messages.
This would avoid a fair bit of special casing, as currently `Concrete#` is unique in the fact that the predicate `Concrete# a` does not match the type of its evidence `a ~ concrete_tv`.sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/20936Decide about naming of variables in TyCons2022-01-17T08:52:38ZSimon Peyton JonesDecide about naming of variables in TyConsConsider
```
type T :: forall (x :: Type). x -> Type -- Standalone kind signature
data T (a :: k) = MkT (a :: k) -- Declaration
```
Now suppose, in GHCi, you say `:kind T`.
* What kind would you expect to see?
* `T :: fora...Consider
```
type T :: forall (x :: Type). x -> Type -- Standalone kind signature
data T (a :: k) = MkT (a :: k) -- Declaration
```
Now suppose, in GHCi, you say `:kind T`.
* What kind would you expect to see?
* `T :: forall x. x -> Type`, taking the name of the kind variable from the kind signature.
* `T :: forall k. k -> Type`, taking the name of the kind variable from the header of the declaration.
* Does it matter anyway?
The names used in the kind signature are fully alpha-renamable. The names used in the header of
the declaration are not so renamable, because they scope over the body of the declaration, in this case
the data constructors. (In a class declaration the type variables in the header scope over the
method signatures and associated types.)
In HEAD we took the names from the kind signature, and used a variety of extra plumbing to
make the declaration variables scope correctly. In !7105 I changed this to use the variable
names from the declaration header, because the ones from the signature are fully alpha-renamable.
If we wanted to revert to the previous behaviour, we could do so by making the `tyConKind` field of a `TyCon` hold
the kind from the signature, perhaps with different naming than the `[TyConBinder]` for the
`TyCon`. (Currently the `tyConKind` field is just a cache for `mkTyConKind tyConBinders tyConResKind`.)
Not difficult, but a bit of extra plumbing.
This ticket is to describe the issue and ask what choice we should make.https://gitlab.haskell.org/ghc/ghc/-/issues/20933matchInstEnv accounts for 50% of typechecker time2022-02-09T17:33:58ZMatthew PickeringmatchInstEnv accounts for 50% of typechecker time![2022-01-11-120537_1838x781](/uploads/54981218c0deaf225d86e747e120fcbf/2022-01-11-120537_1838x781.png)
I created a profile of GHC compiling a large commercial project and noticed that `matchInstEnv` accounted for 50% of time spent type...![2022-01-11-120537_1838x781](/uploads/54981218c0deaf225d86e747e120fcbf/2022-01-11-120537_1838x781.png)
I created a profile of GHC compiling a large commercial project and noticed that `matchInstEnv` accounted for 50% of time spent typechecking the project. That seems like rather a lot. Zooming into just `matchInstEnv`..
![2022-01-11-120754_1917x288](/uploads/caa8b8a41042b4725d2a3685652b00ad/2022-01-11-120754_1917x288.png)
It seems that the cost is split quite evenly between `tc_unify_tys_fg`, `tc_match_tys` and `$instIsVisible`, `instIsVisible` looks quite cheap so I wondered if this function is getting hammered an ungodly number of times.https://gitlab.haskell.org/ghc/ghc/-/issues/20932Inconsistent tidying of implications2022-02-06T02:53:52ZSimon Peyton JonesInconsistent tidying of implicationsConsider this program (`tcfail013`)
```
f [] = 1
f True = 2
```
We get the unsolved implication
```
Wanted: WC {wc_impl =
Implic {
TcLevel = 1
Skolems = a_aur[sk:1] a_axQ[sk:1]
...Consider this program (`tcfail013`)
```
f [] = 1
f True = 2
```
We get the unsolved implication
```
Wanted: WC {wc_impl =
Implic {
TcLevel = 1
Skolems = a_aur[sk:1] a_axQ[sk:1]
Given-eqs = NoGivenEqs
Status = Insoluble
Given =
Wanted =
WC {wc_simple =
[WD] hole{co_axS} {0}:: Bool ~# [a_aur[sk:1]] (CIrredCan(shape))
[WD] $dNum_axR {0}:: Num a_axQ[sk:1] (CDictCan(psc))}
Binds = EvBindsVar<axY>
the inferred type of f :: [a_aur[sk:1]] -> a_axQ[sk:1] }}
```
Note that the two skolems have the same `OccName`, namely `a`. (They both started life as
unification variablex, which we generalised.)
When we tidy the skolems we get
```
reportImplic
Implic {
TcLevel = 1
Skolems = a_auG[sk:1] a1_ay2[sk:1]
Given-eqs = NoGivenEqs
Status = Insoluble
Given =
Wanted =
WC {wc_simple =
[WD] hole{co_ay4} {0}:: Bool
GHC.Prim.~# [a_auG[sk:1]] (CIrredCan(shape))
[WD] $dNum_ay3 {0}:: Num a_ay2[sk:1] (CDictCan(psc))}
Binds = EvBindsVar<ay9>
the inferred type of f :: [a_auG[sk:1]] -> a1_ay2[sk:1] }
```
We have tidied one `a` to `a`, and the other to `a1`. This flat-out contradicts
`Note [Tidying multiple names at once]` in `GHC.Types.Names.Occurrence` in GHC.Types.Names.Occurrence,
where we say that we should not accidentally privilege one of these 'a's over the others.
The reason we don't follow the standard guidance is that in `reportImplic` we have
```
(env1, tvs') = mapAccumL tidyVarBndr (cec_tidy ctxt) $
scopedSort tvs
```
If instead we had
```
(env1, tvs') = tidyVarBndrs (cec_tidy ctxt) $
scopedSort tvs
```
then `tidyVarBndrs` would do the symmetric thing. In our example we'd tidy to `a1` and `a2`.
I think we should do the symmetric thing. But we get a couple of dozen regression failures, as
error messages wibble around. Task: make the change, check the changes, and accept them.
The status quo seems wrong to me.Matthew PickeringMatthew Pickering