[Git][ghc/ghc][wip/T26345] 12 commits: Revert "STM: don't create a transaction in the rhs of catchRetry# (#26028)"
by Simon Peyton Jones (＠simonpj) 29 Aug '25
by Simon Peyton Jones (＠simonpj) 29 Aug '25
29 Aug '25
Simon Peyton Jones pushed to branch wip/T26345 at Glasgow Haskell Compiler / GHC
Commits:
5b5d9d47 by Ben Gamari at 2025-08-25T14:29:35-04:00
Revert "STM: don't create a transaction in the rhs of catchRetry# (#26028)"
This reverts commit 0a5836891ca29836a24c306d2a364c2e4b5377fd
- - - - -
10f06163 by Cheng Shao at 2025-08-25T14:30:16-04:00
wasm: ensure setKeepCAFs() is called in ghci
This patch is a critical bugfix for #26106, see comment and linked
issue for details.
- - - - -
bedc1004 by Cheng Shao at 2025-08-26T09:31:18-04:00
compiler: use zero cost coerce in hoopl setElems/mapToList
This patch is a follow-up of !14680 and changes setElems/mapToList in
GHC/Cmm/Dataflow/Label to use coerce instead of mapping mkHooplLabel
over the keys.
- - - - -
13250d97 by Ryan Scott at 2025-08-26T09:31:59-04:00
Reject infix promoted data constructors without DataKinds
In the rename, make sure to apply the same `DataKinds` checks for both
`HsTyVar` (for prefix promoted data constructors) and `HsOpTy` (for infix
promoted data constructors) alike.
Fixes #26318.
- - - - -
37655c46 by Teo Camarasu at 2025-08-26T15:24:51-04:00
tests: disable T22859 under LLVM
This test was failing under the LLVM backend since the allocations
differ from the NCG.
Resolves #26282
- - - - -
2cbba9d6 by Teo Camarasu at 2025-08-26T15:25:33-04:00
base-exports: update version numbers
As the version of the compiler has been bumped, a lot of the embedded
version numbers will need to be updated if we ever run this test with
`--test-accept` so let's just update them now, and keep future diffs
clean.
- - - - -
f9f2ffcf by Alexandre Esteves at 2025-08-27T07:19:14-04:00
Import new name for 'utimbuf' on windows to fix #26337
Fixes an `-Wincompatible-pointer-types` instance that turns into an error on
recent toolchains and surfaced as such on nixpkgs when doing linux->ucrt cross.
This long-standing warning has been present at least since 9.4:
```
C:\GitLabRunner\builds\0\1709189\tmp\ghc16652_0\ghc_4.c:26:115: error:
warning: incompatible pointer types passing 'struct utimbuf *' to parameter of type 'struct _utimbuf *' [-Wincompatible-pointer-types]
|
26 | HsInt32 ghczuwrapperZC9ZCbaseZCSystemziPosixziInternalsZCzuutime(char* a1, struct utimbuf* a2) {return _utime(a1, a2);}
| ^
HsInt32 ghczuwrapperZC9ZCbaseZCSystemziPosixziInternalsZCzuutime(char* a1, struct utimbuf* a2) {return _utime(a1, a2);}
^~
C:\GitLabRunner\builds\0\1709189\_build\stage0\lib\..\..\mingw\x86_64-w64-mingw32\include\sys\utime.h:109:72: error:
note: passing argument to parameter '_Utimbuf' here
|
109 | __CRT_INLINE int __cdecl _utime(const char *_Filename,struct _utimbuf *_Utimbuf) {
| ^
__CRT_INLINE int __cdecl _utime(const char *_Filename,struct _utimbuf *_Utimbuf) {
```
- - - - -
ae89f000 by Hassan Al-Awwadi at 2025-08-27T07:19:56-04:00
Adds the fucnction addDependentDirectory to Q, resolving issue #26148.
This function adds a new directory to the list of things a module depends upon. That means that when the contents of the directory change, the recompilation checker will notice this and the module will be recompiled. Documentation has also been added for addDependentFunction and addDependentDirectory in the user guide.
- - - - -
00478944 by Simon Peyton Jones at 2025-08-27T16:48:30+01:00
Comments only
- - - - -
a7884589 by Simon Peyton Jones at 2025-08-28T11:08:23+01:00
Type-family occurs check in unification
The occurs check in `GHC.Core.Unify.uVarOrFam` was inadequate in dealing
with type families.
Better now. See Note [The occurs check in the Core unifier].
As I did this I realised that the whole apartness thing is trickier than I
thought: see the new Note [Shortcomings of the apartness test]
- - - - -
8adfc222 by sheaf at 2025-08-28T19:47:17-04:00
Fix orientation in HsWrapper composition (<.>)
This commit fixes the order in which WpCast HsWrappers are composed,
fixing a bug introduced in commit 56b32c5a2d5d7cad89a12f4d74dc940e086069d1.
Fixes #26350
- - - - -
6d786831 by Simon Peyton Jones at 2025-08-29T11:09:04+01:00
Fix a long standing bug in the coercion optimiser
We were mis-optimising ForAllCo, leading to #26345
Part of the poblem was the tricky tower of abstractions leading to
the dreadful
GHC.Core.TyCo.Subst.substForAllCoTyVarBndrUsing
This function was serving two masters: regular substitution, but also
coercion optimsation. So tricky was it that it did so wrong.
In this MR I locate all the fancy footwork for coercion optimisation
in GHC.Core.Coercion.Opt, where it belongs. That leaves substitution
free to be much simpler.
- - - - -
55 changed files:
- compiler/GHC/Cmm/Dataflow/Label.hs
- compiler/GHC/Core/Coercion.hs
- compiler/GHC/Core/Coercion/Opt.hs
- compiler/GHC/Core/TyCo/Compare.hs
- compiler/GHC/Core/TyCo/Subst.hs
- compiler/GHC/Core/Type.hs
- compiler/GHC/Core/Unify.hs
- compiler/GHC/HsToCore/Usage.hs
- compiler/GHC/Iface/Make.hs
- compiler/GHC/Iface/Recomp.hs
- compiler/GHC/Iface/Recomp/Types.hs
- compiler/GHC/Rename/HsType.hs
- compiler/GHC/Tc/Gen/App.hs
- compiler/GHC/Tc/Gen/Splice.hs
- compiler/GHC/Tc/Types.hs
- compiler/GHC/Tc/Types/Evidence.hs
- compiler/GHC/Tc/Utils/Monad.hs
- compiler/GHC/Tc/Utils/Unify.hs
- compiler/GHC/Unit/Finder.hs
- compiler/GHC/Unit/Finder/Types.hs
- compiler/GHC/Unit/Module/Deps.hs
- docs/users_guide/9.16.1-notes.rst
- docs/users_guide/separate_compilation.rst
- libraries/ghc-internal/src/GHC/Internal/System/Posix/Internals.hs
- libraries/ghc-internal/src/GHC/Internal/TH/Syntax.hs
- libraries/ghci/GHCi/Message.hs
- libraries/ghci/GHCi/TH.hs
- libraries/template-haskell/Language/Haskell/TH/Syntax.hs
- rts/PrimOps.cmm
- rts/RaiseAsync.c
- rts/STM.c
- testsuite/.gitignore
- testsuite/tests/interface-stability/base-exports.stdout
- testsuite/tests/interface-stability/base-exports.stdout-javascript-unknown-ghcjs
- testsuite/tests/interface-stability/base-exports.stdout-mingw32
- testsuite/tests/interface-stability/base-exports.stdout-ws-32
- testsuite/tests/interface-stability/template-haskell-exports.stdout
- − testsuite/tests/lib/stm/T26028.hs
- − testsuite/tests/lib/stm/T26028.stdout
- − testsuite/tests/lib/stm/all.T
- testsuite/tests/rts/all.T
- testsuite/tests/th/Makefile
- + testsuite/tests/th/TH_Depends_Dir.hs
- + testsuite/tests/th/TH_Depends_Dir.stdout
- + testsuite/tests/th/TH_Depends_Dir_External.hs
- testsuite/tests/th/all.T
- + testsuite/tests/typecheck/should_compile/T26345.hs
- + testsuite/tests/typecheck/should_compile/T26346.hs
- + testsuite/tests/typecheck/should_compile/T26350.hs
- + testsuite/tests/typecheck/should_compile/T26358.hs
- testsuite/tests/typecheck/should_compile/all.T
- + testsuite/tests/typecheck/should_fail/T26318.hs
- + testsuite/tests/typecheck/should_fail/T26318.stderr
- testsuite/tests/typecheck/should_fail/all.T
- utils/jsffi/dyld.mjs
The diff was not included because it is too large.
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/fdb7ab1ee7ea15678cdb48c1e58c38…
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/fdb7ab1ee7ea15678cdb48c1e58c38…
You're receiving this email because of your account on gitlab.haskell.org.
1
0
Simon Peyton Jones pushed new branch wip/T26345 at Glasgow Haskell Compiler / GHC
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/tree/wip/T26345
You're receiving this email because of your account on gitlab.haskell.org.
1
0
29 Aug '25
Matthew Pickering pushed to branch wip/bytecode-library at Glasgow Haskell Compiler / GHC
Commits:
e98da5a9 by Matthew Pickering at 2025-08-29T10:04:12+01:00
Missing file
- - - - -
1 changed file:
- + compiler/GHC/Linker/ByteCode.hs
Changes:
=====================================
compiler/GHC/Linker/ByteCode.hs
=====================================
@@ -0,0 +1,29 @@
+-- Utilities for creating bytecode libraries
+module GHC.Linker.ByteCode where
+
+import GHC.Prelude
+import GHC.ByteCode.Serialize
+import GHC.Driver.Session
+import GHC.Utils.Error
+import GHC.Driver.Env
+import GHC.Utils.Outputable
+
+
+linkBytecodeLib :: HscEnv -> [ByteCodeObject] -> IO ()
+linkBytecodeLib hsc_env gbcs = do
+ let dflags = hsc_dflags hsc_env
+ -- The .gbc files from the command line
+ let bytecodeObjects = [f | FileOption _ f <- ldInputs dflags]
+
+ -- INSERT_YOUR_CODE
+ let logger = hsc_logger hsc_env
+ let allFiles = (map text bytecodeObjects) ++ [ angleBrackets (text "in-memory" <+> ppr (bco_module bco)) | bco <- gbcs ]
+ debugTraceMsg logger 2 $
+ text "linkBytecodeLib: linking the following bytecode objects:" $$
+ vcat allFiles
+
+ bytecodeLib <- mkBytecodeLib hsc_env bytecodeObjects gbcs
+ let output_fn = case outputFile dflags of { Just s -> s; Nothing -> "a.out"; }
+ writeBytecodeLib bytecodeLib output_fn
+ return ()
+
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/e98da5a9a171d3c754d996853f9df1c…
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/e98da5a9a171d3c754d996853f9df1c…
You're receiving this email because of your account on gitlab.haskell.org.
1
0
29 Aug '25
Simon Peyton Jones pushed to branch wip/T26331 at Glasgow Haskell Compiler / GHC
Commits:
00478944 by Simon Peyton Jones at 2025-08-27T16:48:30+01:00
Comments only
- - - - -
a7884589 by Simon Peyton Jones at 2025-08-28T11:08:23+01:00
Type-family occurs check in unification
The occurs check in `GHC.Core.Unify.uVarOrFam` was inadequate in dealing
with type families.
Better now. See Note [The occurs check in the Core unifier].
As I did this I realised that the whole apartness thing is trickier than I
thought: see the new Note [Shortcomings of the apartness test]
- - - - -
8adfc222 by sheaf at 2025-08-28T19:47:17-04:00
Fix orientation in HsWrapper composition (<.>)
This commit fixes the order in which WpCast HsWrappers are composed,
fixing a bug introduced in commit 56b32c5a2d5d7cad89a12f4d74dc940e086069d1.
Fixes #26350
- - - - -
1ad0218f by Simon Peyton Jones at 2025-08-29T09:53:13+01:00
Fix deep subsumption again
This commit fixed #26255:
commit 56b32c5a2d5d7cad89a12f4d74dc940e086069d1
Author: sheaf <sam.derbyshire(a)gmail.com>
Date: Mon Aug 11 15:50:47 2025 +0200
Improve deep subsumption
This commit improves the DeepSubsumption sub-typing implementation
in GHC.Tc.Utils.Unify.tc_sub_type_deep by being less eager to fall back
to unification.
But alas it still wasn't quite right for view patterns: #26331
This MR does a generalisation to fix it. A bit of a sledgehammer to crack
a nut, but nice.
* Add a field `ir_inst :: InferInstFlag` to `InferResult`, where
```
data InferInstFlag = IIF_Sigma | IIF_ShallowRho | IIF_DeepRho
```
* The flag says exactly how much `fillInferResult` should instantiate
before filling the hole.
* We can also use this to replace the previous very ad-hoc `tcInferSigma`
that was used to implement GHCi's `:type` command.
- - - - -
22 changed files:
- compiler/GHC/Core/TyCo/Compare.hs
- compiler/GHC/Core/Unify.hs
- compiler/GHC/Tc/Gen/App.hs
- compiler/GHC/Tc/Gen/Bind.hs
- compiler/GHC/Tc/Gen/Expr.hs
- compiler/GHC/Tc/Gen/Expr.hs-boot
- compiler/GHC/Tc/Gen/Head.hs
- compiler/GHC/Tc/Gen/HsType.hs
- compiler/GHC/Tc/Gen/Match.hs
- compiler/GHC/Tc/Gen/Pat.hs
- compiler/GHC/Tc/Module.hs
- compiler/GHC/Tc/Types/Evidence.hs
- compiler/GHC/Tc/Utils/TcMType.hs
- compiler/GHC/Tc/Utils/TcType.hs
- compiler/GHC/Tc/Utils/Unify.hs
- + testsuite/tests/patsyn/should_compile/T26331.hs
- + testsuite/tests/patsyn/should_compile/T26331a.hs
- testsuite/tests/patsyn/should_compile/all.T
- + testsuite/tests/typecheck/should_compile/T26346.hs
- + testsuite/tests/typecheck/should_compile/T26350.hs
- + testsuite/tests/typecheck/should_compile/T26358.hs
- testsuite/tests/typecheck/should_compile/all.T
Changes:
=====================================
compiler/GHC/Core/TyCo/Compare.hs
=====================================
@@ -229,6 +229,8 @@ tcEqTyConApps tc1 args1 tc2 args2
= tc1 == tc2 && tcEqTyConAppArgs args1 args2
tcEqTyConAppArgs :: [Type] -> [Type] -> Bool
+-- Args do not have to have equal length;
+-- we discard the excess of the longer one
tcEqTyConAppArgs args1 args2
= and (zipWith tcEqTypeNoKindCheck args1 args2)
-- No kind check necessary: if both arguments are well typed, then
=====================================
compiler/GHC/Core/Unify.hs
=====================================
@@ -245,16 +245,21 @@ give up on), but for /substitutivity/. If we have (F x x), we can see that (F x
can reduce to Double. So, it had better be the case that (F blah blah) can
reduce to Double, no matter what (blah) is!
-To achieve this, `go_fam` in `uVarOrFam` does this;
+To achieve this, `go` in `uVarOrFam` does this;
+
+* We maintain /two/ substitutions, not just one:
+ * um_tv_env: the regular substitution, mapping TyVar :-> Type
+ * um_fam_env: maps (TyCon,[Type]) :-> Type, where the LHS is a type-fam application
+ In effect, these constitute one substitution mapping
+ CanEqLHS :-> Types
* When we attempt to unify (G Float) ~ Int, we return MaybeApart..
- but we /also/ extend a "family substitution" [G Float :-> Int],
- in `um_fam_env`, alongside the regular [tyvar :-> type] substitution in
- `um_tv_env`. See the `BindMe` case of `go_fam` in `uVarOrFam`.
+ but we /also/ add a "family substitution" [G Float :-> Int],
+ to `um_fam_env`. See the `BindMe` case of `go` in `uVarOrFam`.
* When we later encounter (G Float) ~ Bool, we apply the family substitution,
very much as we apply the conventional [tyvar :-> type] substitution
- when we encounter a type variable. See the `lookupFamEnv` in `go_fam` in
+ when we encounter a type variable. See the `lookupFamEnv` in `go` in
`uVarOrFam`.
So (G Float ~ Bool) becomes (Int ~ Bool) which is SurelyApart. Bingo.
@@ -329,7 +334,7 @@ Wrinkles
alternative path. So `noMatchableGivenDicts` must return False;
so `mightMatchLater` must return False; so when um_bind_fam_fun returns
`DontBindMe`, the unifier must return `SurelyApart`, not `MaybeApart`. See
- `go_fam` in `uVarOrFam`
+ `go` in `uVarOrFam`
(ATF6) When /matching/ can we ever have a type-family application on the LHS, in
the template? You might think not, because type-class-instance and
@@ -426,6 +431,9 @@ Wrinkles
(ATF12) There is a horrid exception for the injectivity check. See (UR1) in
in Note [Specification of unification].
+(ATF13) We have to be careful about the occurs check.
+ See Note [The occurs check in the Core unifier]
+
SIDE NOTE. The paper "Closed type families with overlapping equations"
http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/axioms-e…
tries to achieve the same effect with a standard yes/no unifier, by "flattening"
@@ -449,6 +457,49 @@ and all is lost. But with the current algorithm we have that
a a ~ (Var A) (Var B)
is SurelyApart, so the first equation definitely doesn't match and we can try the
second, which does. END OF SIDE NOTE.
+
+Note [Shortcomings of the apartness test]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Note [Apartness and type families] is very clever.
+
+But it still has shortcomings (#26358). Consider unifying
+ [F a, F Int, Int] ~ [Bool, Char, a]
+Working left to right you might think we would build the mapping
+ F a :-> Bool
+ F Int :-> Char
+Now we discover that `a` unifies with `Int`. So really these two lists are Apart
+because F Int can't be both Bool and Char.
+
+Just the same applies when adding a type-family binding to um_fam_env:
+ [F (G Float), F Int, G Float] ~ [Bool, Char, Iont]
+Again these are Apart, because (G Float = Int),
+and (F Int) can't be both Bool and Char
+
+But achieving this is very tricky! Perhaps whenever we unify a type variable,
+or a type family, we should run it over the domain and (maybe range) of the
+type-family mapping too? Sigh.
+
+For now we make no such attempt.
+* The um_fam_env has only /un-substituted/ types.
+* We look up only /un-substituted/ types in um_fam_env
+
+This may make us say MaybeApart when we could say SurelyApart, but it has no
+effect on the correctness of unification: if we return Unifiable, it really is
+Unifiable.
+
+This is all quite subtle. suppose we have:
+ um_tv_env: c :-> b
+ um_fam_env F b :-> a
+and we are trying to add a :-> F c. We will call lookupFamEnv on (F, [c]), which will
+fail because b and c are not equal. So we go ahead and add a :-> F c as a new tyvar eq,
+getting:
+ um_tv_env: a :-> F c, c :-> b
+ um_fam_env F b :-> a
+
+Does that loop, like this:
+ a --> F c --> F b --> a?
+No, because we do not substitute (F c) to (F b) and then look up in um_fam_env;
+we look up only un-substituted types.
-}
{- *********************************************************************
@@ -1767,6 +1818,11 @@ uVarOrFam :: UMEnv -> CanEqLHS -> InType -> OutCoercion -> UM ()
-- Why saturated? See (ATF4) in Note [Apartness and type families]
uVarOrFam env ty1 ty2 kco
= do { substs <- getSubstEnvs
+-- ; pprTrace "uVarOrFam" (vcat
+-- [ text "ty1" <+> ppr ty1
+-- , text "ty2" <+> ppr ty2
+-- , text "tv_env" <+> ppr (um_tv_env substs)
+-- , text "fam_env" <+> ppr (um_fam_env substs) ]) $
; go NotSwapped substs ty1 ty2 kco }
where
-- `go` takes two bites at the cherry; if the first one fails
@@ -1776,16 +1832,12 @@ uVarOrFam env ty1 ty2 kco
-- E.g. a ~ F p q
-- Starts with: go a (F p q)
-- if `a` not bindable, swap to: go (F p q) a
- go swapped substs (TyVarLHS tv1) ty2 kco
- = go_tv swapped substs tv1 ty2 kco
-
- go swapped substs (TyFamLHS tc tys) ty2 kco
- = go_fam swapped substs tc tys ty2 kco
-----------------------------
- -- go_tv: LHS is a type variable
+ -- LHS is a type variable
-- The sequence of tests is very similar to go_tv
- go_tv swapped substs tv1 ty2 kco
+ go :: SwapFlag -> UMState -> CanEqLHS -> InType -> OutCoercion -> UM ()
+ go swapped substs lhs@(TyVarLHS tv1) ty2 kco
| Just ty1' <- lookupVarEnv (um_tv_env substs) tv1'
= -- We already have a substitution for tv1
if | um_unif env -> unify_ty env ty1' ty2 kco
@@ -1837,9 +1889,8 @@ uVarOrFam env ty1 ty2 kco
where
tv1' = umRnOccL env tv1
ty2_fvs = tyCoVarsOfType ty2
- rhs_fvs = ty2_fvs `unionVarSet` tyCoVarsOfCo kco
rhs = ty2 `mkCastTy` mkSymCo kco
- tv1_is_bindable | not (tv1' `elemVarSet` um_foralls env)
+ tv1_is_bindable | not (tv1' `elemVarSet` foralld_tvs)
-- tv1' is not forall-bound, but tv1 can still differ
-- from tv1; see Note [Cloning the template binders]
-- in GHC.Core.Rules. So give tv1' to um_bind_tv_fun.
@@ -1848,16 +1899,16 @@ uVarOrFam env ty1 ty2 kco
| otherwise
= False
- occurs_check = um_unif env &&
- occursCheck (um_tv_env substs) tv1 rhs_fvs
+ foralld_tvs = um_foralls env
+ occurs_check = um_unif env && uOccursCheck substs foralld_tvs lhs rhs
-- Occurs check, only when unifying
-- see Note [Infinitary substitutions]
- -- Make sure you include `kco` in rhs_tvs #14846
+ -- Make sure you include `kco` in rhs #14846
-----------------------------
- -- go_fam: LHS is a saturated type-family application
+ -- LHS is a saturated type-family application
-- Invariant: ty2 is not a TyVarTy
- go_fam swapped substs tc1 tys1 ty2 kco
+ go swapped substs lhs@(TyFamLHS tc1 tys1) ty2 kco
-- If we are under a forall, just give up and return MaybeApart
-- see (ATF3) in Note [Apartness and type families]
| not (isEmptyVarSet (um_foralls env))
@@ -1878,14 +1929,17 @@ uVarOrFam env ty1 ty2 kco
-- Check for equality F tys1 ~ F tys2
| Just (tc2, tys2) <- isSatFamApp ty2
, tc1 == tc2
- = go_fam_fam tc1 tys1 tys2 kco
+ = go_fam_fam substs tc1 tys1 tys2 kco
-- Now check if we can bind the (F tys) to the RHS
-- This can happen even when matching: see (ATF7)
| BindMe <- um_bind_fam_fun env tc1 tys1 rhs
- = -- ToDo: do we need an occurs check here?
- do { extendFamEnv tc1 tys1 rhs
- ; maybeApart MARTypeFamily }
+ = if uOccursCheck substs emptyVarSet lhs rhs
+ then maybeApart MARInfinite
+ else do { extendFamEnv tc1 tys1 rhs
+ -- We don't substitute tys1 before extending
+ -- See Note [Shortcomings of the apartness test]
+ ; maybeApart MARTypeFamily }
-- Swap in case of (F a b) ~ (G c d e)
-- Maybe um_bind_fam_fun is False of (F a b) but true of (G c d e)
@@ -1905,7 +1959,8 @@ uVarOrFam env ty1 ty2 kco
-----------------------------
-- go_fam_fam: LHS and RHS are both saturated type-family applications,
-- for the same type-family F
- go_fam_fam tc tys1 tys2 kco
+ -- Precondition: um_foralls is empty
+ go_fam_fam substs tc tys1 tys2 kco
-- Decompose (F tys1 ~ F tys2): (ATF9)
-- Use injectivity information of F: (ATF10)
-- But first bind the type-fam if poss: (ATF11)
@@ -1925,13 +1980,13 @@ uVarOrFam env ty1 ty2 kco
bind_fam_if_poss
| not (um_unif env) -- Not when matching (ATF11-1)
= return ()
- | tcEqTyConAppArgs tys1 tys2 -- Detect (F tys ~ F tys);
- = return () -- otherwise we'd build an infinite substitution
| BindMe <- um_bind_fam_fun env tc tys1 rhs1
- = extendFamEnv tc tys1 rhs1
- | um_unif env
- , BindMe <- um_bind_fam_fun env tc tys2 rhs2
- = extendFamEnv tc tys2 rhs2
+ = unless (uOccursCheck substs emptyVarSet (TyFamLHS tc tys1) rhs1) $
+ extendFamEnv tc tys1 rhs1
+ -- At this point um_unif=True, so we can unify either way
+ | BindMe <- um_bind_fam_fun env tc tys2 rhs2
+ = unless (uOccursCheck substs emptyVarSet (TyFamLHS tc tys2) rhs2) $
+ extendFamEnv tc tys2 rhs2
| otherwise
= return ()
@@ -1939,17 +1994,92 @@ uVarOrFam env ty1 ty2 kco
rhs2 = mkTyConApp tc tys1 `mkCastTy` kco
-occursCheck :: TvSubstEnv -> TyVar -> TyCoVarSet -> Bool
-occursCheck env tv1 tvs
- = anyVarSet bad tvs
+uOccursCheck :: UMState
+ -> TyVarSet -- Bound by enclosing foralls; see (OCU1)
+ -> CanEqLHS -> Type -- Can we unify (lhs := ty)?
+ -> Bool
+-- See Note [The occurs check in the Core unifier] and (ATF13)
+uOccursCheck (UMState { um_tv_env = tv_env, um_fam_env = fam_env }) bvs lhs ty
+ = go bvs ty
where
- bad tv | Just ty <- lookupVarEnv env tv
- = anyVarSet bad (tyCoVarsOfType ty)
- | otherwise
- = tv == tv1
-
-{- Note [Unifying coercion-foralls]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+ go :: TyCoVarSet -- Bound by enclosing foralls; see (OCU1)
+ -> Type -> Bool
+ go bvs ty | Just ty' <- coreView ty = go bvs ty'
+ go bvs (TyVarTy tv) | Just ty' <- lookupVarEnv tv_env tv
+ = go bvs ty'
+ | TyVarLHS tv' <- lhs, tv==tv'
+ = True
+ | otherwise
+ = go bvs (tyVarKind tv)
+ go bvs (AppTy ty1 ty2) = go bvs ty1 || go bvs ty2
+ go _ (LitTy {}) = False
+ go bvs (FunTy _ w arg res) = go bvs w || go bvs arg || go bvs res
+ go bvs (TyConApp tc tys) = go_tc bvs tc tys
+
+ go bvs (ForAllTy (Bndr tv _) ty)
+ = go bvs (tyVarKind tv) ||
+ (case lhs of
+ TyVarLHS tv' | tv==tv' -> False -- Shadowing
+ | otherwise -> go (bvs `extendVarSet` tv) ty
+ TyFamLHS {} -> False) -- Lookups don't happen under a forall
+
+ go bvs (CastTy ty _co) = go bvs ty -- ToDo: should we worry about `co`?
+ go _ (CoercionTy _co) = False -- ToDo: should we worry about `co`?
+
+ go_tc bvs tc tys
+ | isEmptyVarSet bvs -- Never look up in um_fam_env under a forall (ATF3)
+ , isTypeFamilyTyCon tc
+ , Just ty' <- lookupFamEnv fam_env tc (take arity tys)
+ -- NB: we look up /un-substituted/ types;
+ -- See Note [Shortcomings of the apartness test]
+ = go bvs ty' || any (go bvs) (drop arity tys)
+
+ | TyFamLHS tc' tys' <- lhs
+ , tc == tc'
+ , tys `lengthAtLeast` arity -- Saturated, or over-saturated
+ , tcEqTyConAppArgs tys tys'
+ = True
+
+ | otherwise
+ = any (go bvs) tys
+ where
+ arity = tyConArity tc
+
+{- Note [The occurs check in the Core unifier]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The unifier applies both substitutions (um_tv_env and um_fam_env) as it goes,
+so we'll get an infinite loop if we have, for example
+ um_tv_env: a :-> F b -- (1)
+ um_fam_env F b :-> a -- (2)
+
+So (uOccursCheck substs lhs ty) returns True iff extending `substs` with `lhs :-> ty`
+could lead to a loop. That is, could there by a type `s` such that
+ applySubsts( (substs + lhs:->ty), s ) is infinite
+
+It's vital that we do both at once: we might have (1) already and add (2);
+or we might have (2) already and add (1).
+
+A very similar task is done by GHC.Tc.Utils.Unify.checkTyEqRhs.
+
+(OCU1) We keep track of the forall-bound variables because the um_fam_env is inactive
+ under a forall; indeed it is /unsound/ to consult it because we may have a binding
+ (F a :-> Int), and then unify (forall a. ...(F a)...) with something. We don't
+ want to map that (F a) to Int!
+
+(OCU2) Performance. Consider unifying
+ [a, b] ~ [big-ty, (a,a,a)]
+ We'll unify a:=big-ty. Then we'll attempt b:=(a,a,a), but must do an occurs check.
+ So we'll walk over big-ty, looking for `b`. And then again, and again, once for
+ each occurrence of `a`. A similar thing happens for
+ [a, (b,b,b)] ~ [big-ty, (a,a,a)]
+ albeit a bit less obviously.
+
+ Potentially we could use a cache to record checks we have already done;
+ but I have not attempted that yet. Precisely similar remarks would apply
+ to GHC.Tc.Utils.Unify.checkTyEqRhs
+
+Note [Unifying coercion-foralls]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we try to unify (forall cv. t1) ~ (forall cv. t2).
See Note [ForAllTy] in GHC.Core.TyCo.Rep.
=====================================
compiler/GHC/Tc/Gen/App.hs
=====================================
@@ -16,7 +16,6 @@
module GHC.Tc.Gen.App
( tcApp
- , tcInferSigma
, tcExprPrag ) where
import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcPolyExpr )
@@ -165,26 +164,6 @@ Note [Instantiation variables are short lived]
-}
-{- *********************************************************************
-* *
- tcInferSigma
-* *
-********************************************************************* -}
-
-tcInferSigma :: Bool -> LHsExpr GhcRn -> TcM TcSigmaType
--- Used only to implement :type; see GHC.Tc.Module.tcRnExpr
--- True <=> instantiate -- return a rho-type
--- False <=> don't instantiate -- return a sigma-type
-tcInferSigma inst (L loc rn_expr)
- = addExprCtxt rn_expr $
- setSrcSpanA loc $
- do { (fun@(rn_fun,fun_ctxt), rn_args) <- splitHsApps rn_expr
- ; do_ql <- wantQuickLook rn_fun
- ; (tc_fun, fun_sigma) <- tcInferAppHead fun
- ; (inst_args, app_res_sigma) <- tcInstFun do_ql inst (tc_fun, fun_ctxt) fun_sigma rn_args
- ; _ <- tcValArgs do_ql inst_args
- ; return app_res_sigma }
-
{- *********************************************************************
* *
Typechecking n-ary applications
@@ -219,7 +198,7 @@ using the application chain route, and we can just recurse to tcExpr.
A "head" has three special cases (for which we can infer a polytype
using tcInferAppHead_maybe); otherwise is just any old expression (for
-which we can infer a rho-type (via tcInfer).
+which we can infer a rho-type (via runInferExpr).
There is no special treatment for HsHole (HsVar ...), HsOverLit, etc, because
we can't get a polytype from them.
@@ -403,13 +382,22 @@ tcApp rn_expr exp_res_ty
-- Step 2: Infer the type of `fun`, the head of the application
; (tc_fun, fun_sigma) <- tcInferAppHead fun
; let tc_head = (tc_fun, fun_ctxt)
+ -- inst_final: top-instantiate the result type of the application,
+ -- EXCEPT if we are trying to infer a sigma-type
+ inst_final = case exp_res_ty of
+ Check {} -> True
+ Infer (IR {ir_inst=iif}) ->
+ case iif of
+ IIF_ShallowRho -> True
+ IIF_DeepRho -> True
+ IIF_Sigma -> False
-- Step 3: Instantiate the function type (taking a quick look at args)
; do_ql <- wantQuickLook rn_fun
; (inst_args, app_res_rho)
<- setQLInstLevel do_ql $ -- See (TCAPP1) and (TCAPP2) in
-- Note [tcApp: typechecking applications]
- tcInstFun do_ql True tc_head fun_sigma rn_args
+ tcInstFun do_ql inst_final tc_head fun_sigma rn_args
; case do_ql of
NoQL -> do { traceTc "tcApp:NoQL" (ppr rn_fun $$ ppr app_res_rho)
@@ -420,6 +408,7 @@ tcApp rn_expr exp_res_ty
app_res_rho exp_res_ty
-- Step 4.2: typecheck the arguments
; tc_args <- tcValArgs NoQL inst_args
+
-- Step 4.3: wrap up
; finishApp tc_head tc_args app_res_rho res_wrap }
@@ -427,15 +416,18 @@ tcApp rn_expr exp_res_ty
-- Step 5.1: Take a quick look at the result type
; quickLookResultType app_res_rho exp_res_ty
+
-- Step 5.2: typecheck the arguments, and monomorphise
-- any un-unified instantiation variables
; tc_args <- tcValArgs DoQL inst_args
- -- Step 5.3: zonk to expose the polymophism hidden under
+
+ -- Step 5.3: zonk to expose the polymorphism hidden under
-- QuickLook instantiation variables in `app_res_rho`
; app_res_rho <- liftZonkM $ zonkTcType app_res_rho
+
-- Step 5.4: subsumption check against the expected type
; res_wrap <- checkResultTy rn_expr tc_head inst_args
- app_res_rho exp_res_ty
+ app_res_rho exp_res_ty
-- Step 5.5: wrap up
; finishApp tc_head tc_args app_res_rho res_wrap } }
@@ -470,32 +462,12 @@ checkResultTy :: HsExpr GhcRn
-> (HsExpr GhcTc, AppCtxt) -- Head
-> [HsExprArg p] -- Arguments, just error messages
-> TcRhoType -- Inferred type of the application; zonked to
- -- expose foralls, but maybe not deeply instantiated
+ -- expose foralls, but maybe not /deeply/ instantiated
-> ExpRhoType -- Expected type; this is deeply skolemised
-> TcM HsWrapper
checkResultTy rn_expr _fun _inst_args app_res_rho (Infer inf_res)
- = fillInferResultDS (exprCtOrigin rn_expr) app_res_rho inf_res
- -- See Note [Deeply instantiate in checkResultTy when inferring]
-
-{- Note [Deeply instantiate in checkResultTy when inferring]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-To accept the following program (T26225b) with -XDeepSubsumption, we need to
-deeply instantiate when inferring in checkResultTy:
-
- f :: Int -> (forall a. a->a)
- g :: Int -> Bool -> Bool
-
- test b =
- case b of
- True -> f
- False -> g
-
-If we don't deeply instantiate in the branches of the case expression, we will
-try to unify the type of 'f' with that of 'g', which fails. If we instead
-deeply instantiate 'f', we will fill the 'InferResult' with 'Int -> alpha -> alpha'
-which then successfully unifies with the type of 'g' when we come to fill the
-'InferResult' hole a second time for the second case branch.
--}
+ = fillInferResult (exprCtOrigin rn_expr) app_res_rho inf_res
+ -- fillInferResult does deep instantiation if DeepSubsumption is on
checkResultTy rn_expr (tc_fun, fun_ctxt) inst_args app_res_rho (Check res_ty)
-- Unify with expected type from the context
@@ -651,18 +623,16 @@ quickLookKeys = [dollarIdKey, leftSectionKey, rightSectionKey]
********************************************************************* -}
tcInstFun :: QLFlag
- -> Bool -- False <=> Instantiate only /inferred/ variables at the end
+ -> Bool -- False <=> Instantiate only /top-level, inferred/ variables;
-- so may return a sigma-type
- -- True <=> Instantiate all type variables at the end:
- -- return a rho-type
- -- The /only/ call site that passes in False is the one
- -- in tcInferSigma, which is used only to implement :type
- -- Otherwise we do eager instantiation; in Fig 5 of the paper
+ -- True <=> Instantiate /top-level, invisible/ type variables;
+ -- always return a rho-type (but not a deep-rho type)
+ -- Generally speaking we pass in True; in Fig 5 of the paper
-- |-inst returns a rho-type
-> (HsExpr GhcTc, AppCtxt)
-> TcSigmaType -> [HsExprArg 'TcpRn]
-> TcM ( [HsExprArg 'TcpInst]
- , TcSigmaType )
+ , TcSigmaType ) -- Does not instantiate trailing invisible foralls
-- This crucial function implements the |-inst judgement in Fig 4, plus the
-- modification in Fig 5, of the QL paper:
-- "A quick look at impredicativity" (ICFP'20).
@@ -704,13 +674,9 @@ tcInstFun do_ql inst_final (tc_fun, fun_ctxt) fun_sigma rn_args
_ -> False
inst_fun :: [HsExprArg 'TcpRn] -> ForAllTyFlag -> Bool
- -- True <=> instantiate a tyvar with this ForAllTyFlag
+ -- True <=> instantiate a tyvar that has this ForAllTyFlag
inst_fun [] | inst_final = isInvisibleForAllTyFlag
| otherwise = const False
- -- Using `const False` for `:type` avoids
- -- `forall {r1} (a :: TYPE r1) {r2} (b :: TYPE r2). a -> b`
- -- turning into `forall a {r2} (b :: TYPE r2). a -> b`.
- -- See #21088.
inst_fun (EValArg {} : _) = isInvisibleForAllTyFlag
inst_fun _ = isInferredForAllTyFlag
=====================================
compiler/GHC/Tc/Gen/Bind.hs
=====================================
@@ -1305,8 +1305,8 @@ tcMonoBinds is_rec sig_fn no_gen
do { mult <- newMultiplicityVar
; ((co_fn, matches'), rhs_ty')
- <- tcInferFRR (FRRBinder name) $ \ exp_ty ->
- -- tcInferFRR: the type of a let-binder must have
+ <- runInferRhoFRR (FRRBinder name) $ \ exp_ty ->
+ -- runInferRhoFRR: the type of a let-binder must have
-- a fixed runtime rep. See #23176
tcExtendBinderStack [TcIdBndr_ExpType name exp_ty NotTopLevel] $
-- We extend the error context even for a non-recursive
@@ -1333,8 +1333,8 @@ tcMonoBinds is_rec sig_fn no_gen
= addErrCtxt (PatMonoBindsCtxt pat grhss) $
do { mult <- tcMultAnnOnPatBind mult_ann
- ; (grhss', pat_ty) <- tcInferFRR FRRPatBind $ \ exp_ty ->
- -- tcInferFRR: the type of each let-binder must have
+ ; (grhss', pat_ty) <- runInferRhoFRR FRRPatBind $ \ exp_ty ->
+ -- runInferRhoFRR: the type of each let-binder must have
-- a fixed runtime rep. See #23176
tcGRHSsPat mult grhss exp_ty
@@ -1522,7 +1522,7 @@ tcLhs sig_fn no_gen (PatBind { pat_lhs = pat, pat_rhs = grhss, pat_mult = mult_a
-- See Note [Typechecking pattern bindings]
; ((pat', nosig_mbis), pat_ty)
<- addErrCtxt (PatMonoBindsCtxt pat grhss) $
- tcInferFRR FRRPatBind $ \ exp_ty ->
+ runInferSigmaFRR FRRPatBind $ \ exp_ty ->
tcLetPat inst_sig_fun no_gen pat (Scaled mult exp_ty) $
-- The above inferred type get an unrestricted multiplicity. It may be
-- worth it to try and find a finer-grained multiplicity here
=====================================
compiler/GHC/Tc/Gen/Expr.hs
=====================================
@@ -19,7 +19,7 @@ module GHC.Tc.Gen.Expr
( tcCheckPolyExpr, tcCheckPolyExprNC,
tcCheckMonoExpr, tcCheckMonoExprNC,
tcMonoExpr, tcMonoExprNC,
- tcInferRho, tcInferRhoNC,
+ tcInferExpr, tcInferSigma, tcInferRho, tcInferRhoNC,
tcPolyLExpr, tcPolyExpr, tcExpr, tcPolyLExprSig,
tcSyntaxOp, tcSyntaxOpGen, SyntaxOpType(..), synKnownType,
tcCheckId,
@@ -233,17 +233,24 @@ tcPolyExprCheck expr res_ty
* *
********************************************************************* -}
+tcInferSigma :: LHsExpr GhcRn -> TcM (LHsExpr GhcTc, TcSigmaType)
+tcInferSigma = tcInferExpr IIF_Sigma
+
tcInferRho, tcInferRhoNC :: LHsExpr GhcRn -> TcM (LHsExpr GhcTc, TcRhoType)
-- Infer a *rho*-type. The return type is always instantiated.
-tcInferRho (L loc expr)
- = setSrcSpanA loc $ -- Set location /first/; see GHC.Tc.Utils.Monad
+tcInferRho = tcInferExpr IIF_DeepRho
+tcInferRhoNC = tcInferExprNC IIF_DeepRho
+
+tcInferExpr, tcInferExprNC :: InferInstFlag -> LHsExpr GhcRn -> TcM (LHsExpr GhcTc, TcType)
+tcInferExpr iif (L loc expr)
+ = setSrcSpanA loc $ -- Set location /first/; see GHC.Tc.Utils.Monad
addExprCtxt expr $ -- Note [Error contexts in generated code]
- do { (expr', rho) <- tcInfer (tcExpr expr)
+ do { (expr', rho) <- runInfer iif IFRR_Any (tcExpr expr)
; return (L loc expr', rho) }
-tcInferRhoNC (L loc expr)
- = setSrcSpanA loc $
- do { (expr', rho) <- tcInfer (tcExpr expr)
+tcInferExprNC iif (L loc expr)
+ = setSrcSpanA loc $
+ do { (expr', rho) <- runInfer iif IFRR_Any (tcExpr expr)
; return (L loc expr', rho) }
---------------
@@ -878,7 +885,7 @@ tcInferTupArgs boxity args
; return (Missing (Scaled mult arg_ty), arg_ty) }
tc_infer_tup_arg i (Present x lexpr@(L l expr))
= do { (expr', arg_ty) <- case boxity of
- Unboxed -> tcInferFRR (FRRUnboxedTuple i) (tcPolyExpr expr)
+ Unboxed -> runInferRhoFRR (FRRUnboxedTuple i) (tcPolyExpr expr)
Boxed -> do { arg_ty <- newFlexiTyVarTy liftedTypeKind
; L _ expr' <- tcCheckPolyExpr lexpr arg_ty
; return (expr', arg_ty) }
=====================================
compiler/GHC/Tc/Gen/Expr.hs-boot
=====================================
@@ -1,8 +1,8 @@
module GHC.Tc.Gen.Expr where
import GHC.Hs ( HsExpr, LHsExpr, SyntaxExprRn
, SyntaxExprTc )
-import GHC.Tc.Utils.TcType ( TcRhoType, TcSigmaType, TcSigmaTypeFRR
- , SyntaxOpType
+import GHC.Tc.Utils.TcType ( TcType, TcRhoType, TcSigmaType, TcSigmaTypeFRR
+ , SyntaxOpType, InferInstFlag
, ExpType, ExpRhoType, ExpSigmaType )
import GHC.Tc.Types ( TcM )
import GHC.Tc.Types.BasicTypes( TcCompleteSig )
@@ -33,6 +33,8 @@ tcExpr :: HsExpr GhcRn -> ExpRhoType -> TcM (HsExpr GhcTc)
tcInferRho, tcInferRhoNC ::
LHsExpr GhcRn -> TcM (LHsExpr GhcTc, TcRhoType)
+tcInferExpr :: InferInstFlag -> LHsExpr GhcRn -> TcM (LHsExpr GhcTc, TcType)
+
tcSyntaxOp :: CtOrigin
-> SyntaxExprRn
-> [SyntaxOpType] -- ^ shape of syntax operator arguments
=====================================
compiler/GHC/Tc/Gen/Head.hs
=====================================
@@ -556,7 +556,7 @@ tcInferAppHead (fun,ctxt)
do { mb_tc_fun <- tcInferAppHead_maybe fun
; case mb_tc_fun of
Just (fun', fun_sigma) -> return (fun', fun_sigma)
- Nothing -> tcInfer (tcExpr fun) }
+ Nothing -> runInferRho (tcExpr fun) }
tcInferAppHead_maybe :: HsExpr GhcRn
-> TcM (Maybe (HsExpr GhcTc, TcSigmaType))
=====================================
compiler/GHC/Tc/Gen/HsType.hs
=====================================
@@ -1063,9 +1063,9 @@ tc_infer_lhs_type mode (L span ty)
-- | Infer the kind of a type and desugar. This is the "up" type-checker,
-- as described in Note [Bidirectional type checking]
tc_infer_hs_type :: TcTyMode -> HsType GhcRn -> TcM (TcType, TcKind)
-
tc_infer_hs_type mode rn_ty
- = tcInfer $ \exp_kind -> tcHsType mode rn_ty exp_kind
+ = runInferKind $ \exp_kind ->
+ tcHsType mode rn_ty exp_kind
{-
Note [Typechecking HsCoreTys]
@@ -1985,7 +1985,7 @@ checkExpKind rn_ty ty ki (Check ki') =
checkExpKind _rn_ty ty ki (Infer cell) = do
-- NB: do not instantiate.
-- See Note [Do not always instantiate eagerly in types]
- co <- fillInferResult ki cell
+ co <- fillInferResultNoInst ki cell
pure (ty `mkCastTy` co)
---------------------------
=====================================
compiler/GHC/Tc/Gen/Match.hs
=====================================
@@ -1034,7 +1034,7 @@ tcDoStmt ctxt (RecStmt { recS_stmts = L l stmts, recS_later_ids = later_names
; tcExtendIdEnv tup_ids $ do
{ ((stmts', (ret_op', tup_rets)), stmts_ty)
- <- tcInfer $ \ exp_ty ->
+ <- runInferRho $ \ exp_ty ->
tcStmtsAndThen ctxt tcDoStmt stmts exp_ty $ \ inner_res_ty ->
do { tup_rets <- zipWithM tcCheckId tup_names
(map mkCheckExpType tup_elt_tys)
@@ -1046,7 +1046,7 @@ tcDoStmt ctxt (RecStmt { recS_stmts = L l stmts, recS_later_ids = later_names
; return (ret_op', tup_rets) }
; ((_, mfix_op'), mfix_res_ty)
- <- tcInfer $ \ exp_ty ->
+ <- runInferRho $ \ exp_ty ->
tcSyntaxOp DoOrigin mfix_op
[synKnownType (mkVisFunTyMany tup_ty stmts_ty)] exp_ty $
\ _ _ -> return ()
@@ -1172,7 +1172,7 @@ tcApplicativeStmts
tcApplicativeStmts ctxt pairs rhs_ty thing_inside
= do { body_ty <- newFlexiTyVarTy liftedTypeKind
; let arity = length pairs
- ; ts <- replicateM (arity-1) $ newInferExpType
+ ; ts <- replicateM (arity-1) $ newInferExpType IIF_DeepRho
; exp_tys <- replicateM arity $ newFlexiTyVarTy liftedTypeKind
; pat_tys <- replicateM arity $ newFlexiTyVarTy liftedTypeKind
; let fun_ty = mkVisFunTysMany pat_tys body_ty
=====================================
compiler/GHC/Tc/Gen/Pat.hs
=====================================
@@ -26,7 +26,7 @@ where
import GHC.Prelude
-import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcSyntaxOp, tcSyntaxOpGen, tcInferRho )
+import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcSyntaxOp, tcSyntaxOpGen, tcInferExpr )
import GHC.Hs
import GHC.Hs.Syn.Type
@@ -220,7 +220,7 @@ tcInferPat :: FixedRuntimeRepContext
-> TcM a
-> TcM ((LPat GhcTc, a), TcSigmaTypeFRR)
tcInferPat frr_orig ctxt pat thing_inside
- = tcInferFRR frr_orig $ \ exp_ty ->
+ = runInferSigmaFRR frr_orig $ \ exp_ty ->
tc_lpat (unrestricted exp_ty) penv pat thing_inside
where
penv = PE { pe_lazy = False, pe_ctxt = LamPat ctxt, pe_orig = PatOrigin }
@@ -694,15 +694,17 @@ tc_pat pat_ty penv ps_pat thing_inside = case ps_pat of
-- restriction need to be put in place, if any, for linear view
-- patterns to desugar to type-correct Core.
- ; (expr',expr_ty) <- tcInferRho expr
- -- Note [View patterns and polymorphism]
+ ; (expr', expr_rho) <- tcInferExpr IIF_ShallowRho expr
+ -- IIF_ShallowRho: do not perform deep instantiation, regardless of
+ -- DeepSubsumption (Note [View patterns and polymorphism])
+ -- But we must do top-instantiation to expose the arrow to matchActualFunTy
-- Expression must be a function
; let herald = ExpectedFunTyViewPat $ unLoc expr
; (expr_wrap1, Scaled _mult inf_arg_ty, inf_res_sigma)
- <- matchActualFunTy herald (Just . HsExprRnThing $ unLoc expr) (1,expr_ty) expr_ty
+ <- matchActualFunTy herald (Just . HsExprRnThing $ unLoc expr) (1,expr_rho) expr_rho
-- See Note [View patterns and polymorphism]
- -- expr_wrap1 :: expr_ty "->" (inf_arg_ty -> inf_res_sigma)
+ -- expr_wrap1 :: expr_rho "->" (inf_arg_ty -> inf_res_sigma)
-- Check that overall pattern is more polymorphic than arg type
; expr_wrap2 <- tc_sub_type penv (scaledThing pat_ty) inf_arg_ty
@@ -715,18 +717,18 @@ tc_pat pat_ty penv ps_pat thing_inside = case ps_pat of
; pat_ty <- readExpType h_pat_ty
; let expr_wrap2' = mkWpFun expr_wrap2 idHsWrapper
(Scaled w pat_ty) inf_res_sigma
- -- expr_wrap2' :: (inf_arg_ty -> inf_res_sigma) "->"
- -- (pat_ty -> inf_res_sigma)
- -- NB: pat_ty comes from matchActualFunTy, so it has a
- -- fixed RuntimeRep, as needed to call mkWpFun.
- ; let
+ -- expr_wrap2' :: (inf_arg_ty -> inf_res_sigma) "->"
+ -- (pat_ty -> inf_res_sigma)
+ -- NB: pat_ty comes from matchActualFunTy, so it has a
+ -- fixed RuntimeRep, as needed to call mkWpFun.
+
expr_wrap = expr_wrap2' <.> expr_wrap1
; return $ (ViewPat pat_ty (mkLHsWrap expr_wrap expr') pat', res) }
{- Note [View patterns and polymorphism]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider this exotic example:
+Consider this exotic example (test T26331a):
pair :: forall a. Bool -> a -> forall b. b -> (a,b)
f :: Int -> blah
@@ -735,11 +737,15 @@ Consider this exotic example:
The expression (pair True) should have type
pair True :: Int -> forall b. b -> (Int,b)
so that it is ready to consume the incoming Int. It should be an
-arrow type (t1 -> t2); hence using (tcInferRho expr).
+arrow type (t1 -> t2); and we must not instantiate that `forall b`,
+/even with DeepSubsumption/. Hence using `IIF_ShallowRho`; this is the only
+place where `IIF_ShallowRho` is used.
Then, when taking that arrow apart we want to get a *sigma* type
(forall b. b->(Int,b)), because that's what we want to bind 'x' to.
Fortunately that's what matchActualFunTy returns anyway.
+
+Another example is #26331.
-}
-- Type signatures in patterns
@@ -768,8 +774,7 @@ Fortunately that's what matchActualFunTy returns anyway.
penv pats thing_inside
; pat_ty <- readExpType (scaledThing pat_ty)
; return (mkHsWrapPat coi
- (ListPat elt_ty pats') pat_ty, res)
-}
+ (ListPat elt_ty pats') pat_ty, res) }
TuplePat _ pats boxity -> do
{ let arity = length pats
=====================================
compiler/GHC/Tc/Module.hs
=====================================
@@ -62,7 +62,6 @@ import GHC.Tc.Gen.Match
import GHC.Tc.Utils.Unify( checkConstraints, tcSubTypeSigma )
import GHC.Tc.Zonk.Type
import GHC.Tc.Gen.Expr
-import GHC.Tc.Gen.App( tcInferSigma )
import GHC.Tc.Utils.Monad
import GHC.Tc.Gen.Export
import GHC.Tc.Types.Evidence
@@ -2628,10 +2627,11 @@ tcRnExpr hsc_env mode rdr_expr
failIfErrsM ;
-- Typecheck the expression
- ((tclvl, res_ty), lie)
+ ((tclvl, (_tc_expr, res_ty)), lie)
<- captureTopConstraints $
pushTcLevelM $
- tcInferSigma inst rn_expr ;
+ (if inst then tcInferRho rn_expr
+ else tcInferSigma rn_expr);
-- Generalise
uniq <- newUnique ;
=====================================
compiler/GHC/Tc/Types/Evidence.hs
=====================================
@@ -206,9 +206,15 @@ instance Monoid HsWrapper where
(<.>) :: HsWrapper -> HsWrapper -> HsWrapper
WpHole <.> c = c
c <.> WpHole = c
-WpCast c1 <.> WpCast c2 = WpCast (c1 `mkTransCo` c2)
+WpCast c1 <.> WpCast c2 = WpCast (c2 `mkTransCo` c1)
-- If we can represent the HsWrapper as a cast, try to do so: this may avoid
-- unnecessary eta-expansion (see 'mkWpFun').
+ --
+ -- NB: <.> behaves like function composition:
+ --
+ -- WpCast c1 <.> WpCast c2 :: coercionLKind c2 ~> coercionRKind c1
+ --
+ -- This is thus the same as WpCast (c2 ; c1) and not WpCast (c1 ; c2).
c1 <.> c2 = c1 `WpCompose` c2
-- | Smart constructor to create a 'WpFun' 'HsWrapper', which avoids introducing
=====================================
compiler/GHC/Tc/Utils/TcMType.hs
=====================================
@@ -65,7 +65,7 @@ module GHC.Tc.Utils.TcMType (
-- Expected types
ExpType(..), ExpSigmaType, ExpRhoType,
mkCheckExpType, newInferExpType, newInferExpTypeFRR,
- tcInfer, tcInferFRR,
+ runInfer, runInferRho, runInferSigma, runInferKind, runInferRhoFRR, runInferSigmaFRR,
readExpType, readExpType_maybe, readScaledExpType,
expTypeToType, scaledExpTypeToType,
checkingExpType_maybe, checkingExpType,
@@ -438,30 +438,29 @@ See test case T21325.
-- actual data definition is in GHC.Tc.Utils.TcType
-newInferExpType :: TcM ExpType
-newInferExpType = new_inferExpType Nothing
+newInferExpType :: InferInstFlag -> TcM ExpType
+newInferExpType iif = new_inferExpType iif IFRR_Any
-newInferExpTypeFRR :: FixedRuntimeRepContext -> TcM ExpTypeFRR
-newInferExpTypeFRR frr_orig
+newInferExpTypeFRR :: InferInstFlag -> FixedRuntimeRepContext -> TcM ExpTypeFRR
+newInferExpTypeFRR iif frr_orig
= do { th_lvl <- getThLevel
- ; if
- -- See [Wrinkle: Typed Template Haskell]
- -- in Note [hasFixedRuntimeRep] in GHC.Tc.Utils.Concrete.
- | TypedBrack _ <- th_lvl
- -> new_inferExpType Nothing
+ ; let mb_frr = case th_lvl of
+ TypedBrack {} -> IFRR_Any
+ _ -> IFRR_Check frr_orig
+ -- mb_frr: see [Wrinkle: Typed Template Haskell]
+ -- in Note [hasFixedRuntimeRep] in GHC.Tc.Utils.Concrete.
- | otherwise
- -> new_inferExpType (Just frr_orig) }
+ ; new_inferExpType iif mb_frr }
-new_inferExpType :: Maybe FixedRuntimeRepContext -> TcM ExpType
-new_inferExpType mb_frr_orig
+new_inferExpType :: InferInstFlag -> InferFRRFlag -> TcM ExpType
+new_inferExpType iif ifrr
= do { u <- newUnique
; tclvl <- getTcLevel
; traceTc "newInferExpType" (ppr u <+> ppr tclvl)
; ref <- newMutVar Nothing
; return (Infer (IR { ir_uniq = u, ir_lvl = tclvl
- , ir_ref = ref
- , ir_frr = mb_frr_orig })) }
+ , ir_inst = iif, ir_frr = ifrr
+ , ir_ref = ref })) }
-- | Extract a type out of an ExpType, if one exists. But one should always
-- exist. Unless you're quite sure you know what you're doing.
@@ -515,12 +514,12 @@ inferResultToType (IR { ir_uniq = u, ir_lvl = tc_lvl
where
-- See Note [TcLevel of ExpType]
new_meta = case mb_frr of
- Nothing -> do { rr <- newMetaTyVarTyAtLevel tc_lvl runtimeRepTy
+ IFRR_Any -> do { rr <- newMetaTyVarTyAtLevel tc_lvl runtimeRepTy
; newMetaTyVarTyAtLevel tc_lvl (mkTYPEapp rr) }
- Just frr -> mdo { rr <- newConcreteTyVarTyAtLevel conc_orig tc_lvl runtimeRepTy
- ; tau <- newMetaTyVarTyAtLevel tc_lvl (mkTYPEapp rr)
- ; let conc_orig = ConcreteFRR $ FixedRuntimeRepOrigin tau frr
- ; return tau }
+ IFRR_Check frr -> mdo { rr <- newConcreteTyVarTyAtLevel conc_orig tc_lvl runtimeRepTy
+ ; tau <- newMetaTyVarTyAtLevel tc_lvl (mkTYPEapp rr)
+ ; let conc_orig = ConcreteFRR $ FixedRuntimeRepOrigin tau frr
+ ; return tau }
{- Note [inferResultToType]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -537,20 +536,31 @@ Note [fillInferResult] in GHC.Tc.Utils.Unify.
-- | Infer a type using a fresh ExpType
-- See also Note [ExpType] in "GHC.Tc.Utils.TcMType"
--
--- Use 'tcInferFRR' if you require the type to have a fixed
+-- Use 'runInferFRR' if you require the type to have a fixed
-- runtime representation.
-tcInfer :: (ExpSigmaType -> TcM a) -> TcM (a, TcSigmaType)
-tcInfer = tc_infer Nothing
+runInferSigma :: (ExpSigmaType -> TcM a) -> TcM (a, TcSigmaType)
+runInferSigma = runInfer IIF_Sigma IFRR_Any
--- | Like 'tcInfer', except it ensures that the resulting type
+runInferRho :: (ExpRhoType -> TcM a) -> TcM (a, TcRhoType)
+runInferRho = runInfer IIF_DeepRho IFRR_Any
+
+runInferKind :: (ExpSigmaType -> TcM a) -> TcM (a, TcSigmaType)
+-- Used for kind-checking types, where we never want deep instantiation,
+-- nor FRR checks
+runInferKind = runInfer IIF_Sigma IFRR_Any
+
+-- | Like 'runInferRho', except it ensures that the resulting type
-- has a syntactically fixed RuntimeRep as per Note [Fixed RuntimeRep] in
-- GHC.Tc.Utils.Concrete.
-tcInferFRR :: FixedRuntimeRepContext -> (ExpSigmaTypeFRR -> TcM a) -> TcM (a, TcSigmaTypeFRR)
-tcInferFRR frr_orig = tc_infer (Just frr_orig)
+runInferRhoFRR :: FixedRuntimeRepContext -> (ExpRhoTypeFRR -> TcM a) -> TcM (a, TcRhoTypeFRR)
+runInferRhoFRR frr_orig = runInfer IIF_DeepRho (IFRR_Check frr_orig)
+
+runInferSigmaFRR :: FixedRuntimeRepContext -> (ExpSigmaTypeFRR -> TcM a) -> TcM (a, TcSigmaTypeFRR)
+runInferSigmaFRR frr_orig = runInfer IIF_Sigma (IFRR_Check frr_orig)
-tc_infer :: Maybe FixedRuntimeRepContext -> (ExpSigmaType -> TcM a) -> TcM (a, TcSigmaType)
-tc_infer mb_frr tc_check
- = do { res_ty <- new_inferExpType mb_frr
+runInfer :: InferInstFlag -> InferFRRFlag -> (ExpSigmaType -> TcM a) -> TcM (a, TcSigmaType)
+runInfer iif mb_frr tc_check
+ = do { res_ty <- new_inferExpType iif mb_frr
; result <- tc_check res_ty
; res_ty <- readExpType res_ty
; return (result, res_ty) }
=====================================
compiler/GHC/Tc/Utils/TcType.hs
=====================================
@@ -24,14 +24,14 @@ module GHC.Tc.Utils.TcType (
--------------------------------
-- Types
TcType, TcSigmaType, TcTypeFRR, TcSigmaTypeFRR,
- TcRhoType, TcTauType, TcPredType, TcThetaType,
+ TcRhoType, TcRhoTypeFRR, TcTauType, TcPredType, TcThetaType,
TcTyVar, TcTyVarSet, TcDTyVarSet, TcTyCoVarSet, TcDTyCoVarSet,
TcKind, TcCoVar, TcTyCoVar, TcTyVarBinder, TcInvisTVBinder, TcReqTVBinder,
TcTyCon, MonoTcTyCon, PolyTcTyCon, TcTyConBinder, KnotTied,
- ExpType(..), ExpKind, InferResult(..),
+ ExpType(..), ExpKind, InferResult(..), InferInstFlag(..), InferFRRFlag(..),
ExpTypeFRR, ExpSigmaType, ExpSigmaTypeFRR,
- ExpRhoType,
+ ExpRhoType, ExpRhoTypeFRR,
mkCheckExpType,
checkingExpType_maybe, checkingExpType,
@@ -380,6 +380,7 @@ type TcSigmaType = TcType
-- See Note [Return arguments with a fixed RuntimeRep.
type TcSigmaTypeFRR = TcSigmaType
-- TODO: consider making this a newtype.
+type TcRhoTypeFRR = TcRhoType
type TcRhoType = TcType -- Note [TcRhoType]
type TcTauType = TcType
@@ -408,9 +409,13 @@ data InferResult
, ir_lvl :: TcLevel
-- ^ See Note [TcLevel of ExpType] in GHC.Tc.Utils.TcMType
- , ir_frr :: Maybe FixedRuntimeRepContext
+ , ir_frr :: InferFRRFlag
-- ^ See Note [FixedRuntimeRep context in ExpType] in GHC.Tc.Utils.TcMType
+ , ir_inst :: InferInstFlag
+ -- ^ True <=> when DeepSubsumption is on, deeply instantiate before filling,
+ -- See Note [Instantiation of InferResult] in GHC.Tc.Utils.Unify
+
, ir_ref :: IORef (Maybe TcType) }
-- ^ The type that fills in this hole should be a @Type@,
-- that is, its kind should be @TYPE rr@ for some @rr :: RuntimeRep@.
@@ -419,26 +424,48 @@ data InferResult
-- @rr@ must be concrete, in the sense of Note [Concrete types]
-- in GHC.Tc.Utils.Concrete.
-type ExpSigmaType = ExpType
+data InferFRRFlag
+ = IFRR_Check -- Check that the result type has a fixed runtime rep
+ FixedRuntimeRepContext -- Typically used for function arguments and lambdas
+
+ | IFRR_Any -- No need to check for fixed runtime-rep
+
+data InferInstFlag -- Specifies whether the inference should return an uninstantiated
+ -- SigmaType, or a (possibly deeply) instantiated RhoType
+ -- See Note [Instantiation of InferResult] in GHC.Tc.Utils.Unify
+
+ = IIF_Sigma -- Trying to infer a SigmaType
+ -- Don't instantiate at all, regardless of DeepSubsumption
+ -- Typically used when inferring the type of a pattern
+
+ | IIF_ShallowRho -- Trying to infer a shallow RhoType (no foralls or => at the top)
+ -- Top-instantiate (only, regardless of DeepSubsumption) before filling the hole
+ -- Typically used when inferring the type of an expression
+
+ | IIF_DeepRho -- Trying to infer a possibly-deep RhoType (depending on DeepSubsumption)
+ -- If DeepSubsumption is off, same as IIF_ShallowRho
+ -- If DeepSubsumption is on, instantiate deeply before filling the hole
+
+type ExpSigmaType = ExpType
+type ExpRhoType = ExpType
+ -- Invariant: in ExpRhoType, if -XDeepSubsumption is on,
+ -- and we are in checking mode (i.e. the ExpRhoType is (Check rho)),
+ -- then the `rho` is deeply skolemised
-- | An 'ExpType' which has a fixed RuntimeRep.
--
-- For a 'Check' 'ExpType', the stored 'TcType' must have
-- a fixed RuntimeRep. For an 'Infer' 'ExpType', the 'ir_frr'
--- field must be of the form @Just frr_orig@.
-type ExpTypeFRR = ExpType
+-- field must be of the form @IFRR_Check frr_orig@.
+type ExpTypeFRR = ExpType
-- | Like 'TcSigmaTypeFRR', but for an expected type.
--
-- See 'ExpTypeFRR'.
type ExpSigmaTypeFRR = ExpTypeFRR
+type ExpRhoTypeFRR = ExpTypeFRR
-- TODO: consider making this a newtype.
-type ExpRhoType = ExpType
- -- Invariant: if -XDeepSubsumption is on,
- -- and we are checking (i.e. the ExpRhoType is (Check rho)),
- -- then the `rho` is deeply skolemised
-
-- | Like 'ExpType', but on kind level
type ExpKind = ExpType
@@ -447,12 +474,17 @@ instance Outputable ExpType where
ppr (Infer ir) = ppr ir
instance Outputable InferResult where
- ppr (IR { ir_uniq = u, ir_lvl = lvl, ir_frr = mb_frr })
- = text "Infer" <> mb_frr_text <> braces (ppr u <> comma <> ppr lvl)
+ ppr (IR { ir_uniq = u, ir_lvl = lvl, ir_frr = mb_frr, ir_inst = inst })
+ = text "Infer" <> parens (pp_inst <> pp_frr)
+ <> braces (ppr u <> comma <> ppr lvl)
where
- mb_frr_text = case mb_frr of
- Just _ -> text "FRR"
- Nothing -> empty
+ pp_inst = case inst of
+ IIF_Sigma -> text "Sigma"
+ IIF_ShallowRho -> text "ShallowRho"
+ IIF_DeepRho -> text "DeepRho"
+ pp_frr = case mb_frr of
+ IFRR_Check {} -> text ",FRR"
+ IFRR_Any -> empty
-- | Make an 'ExpType' suitable for checking.
mkCheckExpType :: TcType -> ExpType
=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -27,7 +27,7 @@ module GHC.Tc.Utils.Unify (
-- Skolemisation
DeepSubsumptionFlag(..), getDeepSubsumptionFlag, isRhoTyDS,
tcSkolemise, tcSkolemiseCompleteSig, tcSkolemiseExpectedType,
- deeplyInstantiate,
+ dsInstantiate,
-- Various unifications
unifyType, unifyKind, unifyInvisibleType,
@@ -40,7 +40,6 @@ module GHC.Tc.Utils.Unify (
--------------------------------
-- Holes
- tcInfer,
matchExpectedListTy,
matchExpectedTyConApp,
matchExpectedAppTy,
@@ -60,7 +59,7 @@ module GHC.Tc.Utils.Unify (
simpleUnifyCheck, UnifyCheckCaller(..), SimpleUnifyResult(..),
- fillInferResult, fillInferResultDS
+ fillInferResult, fillInferResultNoInst
) where
import GHC.Prelude
@@ -801,13 +800,13 @@ matchExpectedFunTys :: forall a.
-- If exp_ty is Infer {}, then [ExpPatType] and ExpRhoType results are all Infer{}
matchExpectedFunTys herald _ctxt arity (Infer inf_res) thing_inside
= do { arg_tys <- mapM (new_infer_arg_ty herald) [1 .. arity]
- ; res_ty <- newInferExpType
+ ; res_ty <- newInferExpType (ir_inst inf_res)
; result <- thing_inside (map ExpFunPatTy arg_tys) res_ty
; arg_tys <- mapM (\(Scaled m t) -> Scaled m <$> readExpType t) arg_tys
; res_ty <- readExpType res_ty
-- NB: mkScaledFunTys arg_tys res_ty does not contain any foralls
-- (even nested ones), so no need to instantiate.
- ; co <- fillInferResult (mkScaledFunTys arg_tys res_ty) inf_res
+ ; co <- fillInferResultNoInst (mkScaledFunTys arg_tys res_ty) inf_res
; return (mkWpCastN co, result) }
matchExpectedFunTys herald ctx arity (Check top_ty) thing_inside
@@ -914,10 +913,10 @@ matchExpectedFunTys herald ctx arity (Check top_ty) thing_inside
; co <- unifyType Nothing (mkScaledFunTys more_arg_tys res_ty) fun_ty
; return (mkWpCastN co, result) }
-new_infer_arg_ty :: ExpectedFunTyOrigin -> Int -> TcM (Scaled ExpSigmaTypeFRR)
+new_infer_arg_ty :: ExpectedFunTyOrigin -> Int -> TcM (Scaled ExpRhoTypeFRR)
new_infer_arg_ty herald arg_pos -- position for error messages only
= do { mult <- newFlexiTyVarTy multiplicityTy
- ; inf_hole <- newInferExpTypeFRR (FRRExpectedFunTy herald arg_pos)
+ ; inf_hole <- newInferExpTypeFRR IIF_DeepRho (FRRExpectedFunTy herald arg_pos)
; return (mkScaled mult inf_hole) }
new_check_arg_ty :: ExpectedFunTyOrigin -> Int -> TcM (Scaled TcType)
@@ -1075,18 +1074,6 @@ matchExpectedAppTy orig_ty
*
********************************************************************** -}
-{- Note [inferResultToType]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~
-expTypeToType and inferResultType convert an InferResult to a monotype.
-It must be a monotype because if the InferResult isn't already filled in,
-we fill it in with a unification variable (hence monotype). So to preserve
-order-independence we check for mono-type-ness even if it *is* filled in
-already.
-
-See also Note [TcLevel of ExpType] in GHC.Tc.Utils.TcType, and
-Note [fillInferResult].
--}
-
-- | Fill an 'InferResult' with the given type.
--
-- If @co = fillInferResult t1 infer_res@, then @co :: t1 ~# t2@,
@@ -1098,14 +1085,14 @@ Note [fillInferResult].
-- The stored type @t2@ is at the same level as given by the
-- 'ir_lvl' field.
-- - FRR invariant.
--- Whenever the 'ir_frr' field is not @Nothing@, @t2@ is guaranteed
+-- Whenever the 'ir_frr' field is `IFRR_Check`, @t2@ is guaranteed
-- to have a syntactically fixed RuntimeRep, in the sense of
-- Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete.
-fillInferResult :: TcType -> InferResult -> TcM TcCoercionN
-fillInferResult act_res_ty (IR { ir_uniq = u
- , ir_lvl = res_lvl
- , ir_frr = mb_frr
- , ir_ref = ref })
+fillInferResultNoInst :: TcType -> InferResult -> TcM TcCoercionN
+fillInferResultNoInst act_res_ty (IR { ir_uniq = u
+ , ir_lvl = res_lvl
+ , ir_frr = mb_frr
+ , ir_ref = ref })
= do { mb_exp_res_ty <- readTcRef ref
; case mb_exp_res_ty of
Just exp_res_ty
@@ -1126,7 +1113,7 @@ fillInferResult act_res_ty (IR { ir_uniq = u
ppr u <> colon <+> ppr act_res_ty <+> char '~' <+> ppr exp_res_ty
; cur_lvl <- getTcLevel
; unless (cur_lvl `sameDepthAs` res_lvl) $
- ensureMonoType act_res_ty
+ ensureMonoType act_res_ty -- See (FIR1)
; unifyType Nothing act_res_ty exp_res_ty }
Nothing
-> do { traceTc "Filling inferred ExpType" $
@@ -1140,16 +1127,28 @@ fillInferResult act_res_ty (IR { ir_uniq = u
-- fixed RuntimeRep (if necessary, i.e. 'mb_frr' is not 'Nothing').
; (frr_co, act_res_ty) <-
case mb_frr of
- Nothing -> return (mkNomReflCo act_res_ty, act_res_ty)
- Just frr_orig -> hasFixedRuntimeRep frr_orig act_res_ty
+ IFRR_Any -> return (mkNomReflCo act_res_ty, act_res_ty)
+ IFRR_Check frr_orig -> hasFixedRuntimeRep frr_orig act_res_ty
-- Compose the two coercions.
; let final_co = prom_co `mkTransCo` frr_co
; writeTcRef ref (Just act_res_ty)
- ; return final_co }
- }
+ ; return final_co } }
+
+fillInferResult :: CtOrigin -> TcType -> InferResult -> TcM HsWrapper
+-- See Note [Instantiation of InferResult]
+fillInferResult ct_orig res_ty ires@(IR { ir_inst = iif })
+ = case iif of
+ IIF_Sigma -> do { co <- fillInferResultNoInst res_ty ires
+ ; return (mkWpCastN co) }
+ IIF_ShallowRho -> do { (wrap, res_ty') <- topInstantiate ct_orig res_ty
+ ; co <- fillInferResultNoInst res_ty' ires
+ ; return (mkWpCastN co <.> wrap) }
+ IIF_DeepRho -> do { (wrap, res_ty') <- dsInstantiate ct_orig res_ty
+ ; co <- fillInferResultNoInst res_ty' ires
+ ; return (mkWpCastN co <.> wrap) }
{- Note [fillInferResult]
~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1210,39 +1209,96 @@ For (2), we simply look to see if the hole is filled already.
- if it is filled, we simply unify with the type that is
already there
-There is one wrinkle. Suppose we have
- case e of
- T1 -> e1 :: (forall a. a->a) -> Int
- G2 -> e2
-where T1 is not GADT or existential, but G2 is a GADT. Then suppose the
-T1 alternative fills the hole with (forall a. a->a) -> Int, which is fine.
-But now the G2 alternative must not *just* unify with that else we'd risk
-allowing through (e2 :: (forall a. a->a) -> Int). If we'd checked G2 first
-we'd have filled the hole with a unification variable, which enforces a
-monotype.
-
-So if we check G2 second, we still want to emit a constraint that restricts
-the RHS to be a monotype. This is done by ensureMonoType, and it works
-by simply generating a constraint (alpha ~ ty), where alpha is a fresh
+(FIR1) There is one wrinkle. Suppose we have
+ case e of
+ T1 -> e1 :: (forall a. a->a) -> Int
+ G2 -> e2
+ where T1 is not GADT or existential, but G2 is a GADT. Then suppose the
+ T1 alternative fills the hole with (forall a. a->a) -> Int, which is fine.
+ But now the G2 alternative must not *just* unify with that else we'd risk
+ allowing through (e2 :: (forall a. a->a) -> Int). If we'd checked G2 first
+ we'd have filled the hole with a unification variable, which enforces a
+ monotype.
+
+ So if we check G2 second, we still want to emit a constraint that restricts
+ the RHS to be a monotype. This is done by ensureMonoType, and it works
+ by simply generating a constraint (alpha ~ ty), where alpha is a fresh
unification variable. We discard the evidence.
--}
+Note [Instantiation of InferResult]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When typechecking expressions (not types, not patterns), we always almost
+always instantiate before filling in `InferResult`, so that the result is a
+TcRhoType. This behaviour is controlled by the `ir_inst :: InferInstFlag`
+field of `InferResult`.
--- | A version of 'fillInferResult' that also performs deep instantiation
--- when deep subsumption is enabled.
---
--- See also Note [Instantiation of InferResult].
-fillInferResultDS :: CtOrigin -> TcRhoType -> InferResult -> TcM HsWrapper
-fillInferResultDS ct_orig rho inf_res
- = do { massertPpr (isRhoTy rho) $
- vcat [ text "fillInferResultDS: input type is not a rho-type"
- , text "ty:" <+> ppr rho ]
- ; ds_flag <- getDeepSubsumptionFlag
- ; case ds_flag of
- Shallow -> mkWpCastN <$> fillInferResult rho inf_res
- Deep -> do { (inst_wrap, rho') <- deeplyInstantiate ct_orig rho
- ; co <- fillInferResult rho' inf_res
- ; return (mkWpCastN co <.> inst_wrap) } }
+If we do instantiate (ir_inst = IIF_DeepRho), and DeepSubsumption is enabled,
+we instantiate deeply. See `tcInferResult`.
+
+Usually this field is `IIF_DeepRho` meaning "return a (possibly deep) rho-type".
+Why is this the common case? See #17173 for discussion. Here are some examples
+of why:
+
+1. Consider
+ f x = (*)
+ We want to instantiate the type of (*) before returning, else we
+ will infer the type
+ f :: forall {a}. a -> forall b. Num b => b -> b -> b
+ This is surely confusing for users.
+
+ And worse, the monomorphism restriction won't work properly. The MR is
+ dealt with in simplifyInfer, and simplifyInfer has no way of
+ instantiating. This could perhaps be worked around, but it may be
+ hard to know even when instantiation should happen.
+
+2. Another reason. Consider
+ f :: (?x :: Int) => a -> a
+ g y = let ?x = 3::Int in f
+ Here want to instantiate f's type so that the ?x::Int constraint
+ gets discharged by the enclosing implicit-parameter binding.
+
+3. Suppose one defines plus = (+). If we instantiate lazily, we will
+ infer plus :: forall a. Num a => a -> a -> a. However, the monomorphism
+ restriction compels us to infer
+ plus :: Integer -> Integer -> Integer
+ (or similar monotype). Indeed, the only way to know whether to apply
+ the monomorphism restriction at all is to instantiate
+
+HOWEVER, not always! Here are places where we want `IIF_Sigma` meaning
+"return a sigma-type":
+
+* IIF_Sigma: In GHC.Tc.Module.tcRnExpr, which implements GHCi's :type
+ command, we want to return a completely uninstantiated type.
+ See Note [Implementing :type] in GHC.Tc.Module.
+
+* IIF_Sigma: In types we can't lambda-abstract, so we must be careful not to instantiate
+ at all. See calls to `runInferHsType`
+
+* IIF_Sigma: in patterns we don't want to instantiate at all. See the use of
+ `runInferSigmaFRR` in GHC.Tc.Gen.Pat
+
+* IIF_ShallowRho: in the expression part of a view pattern, we must top-instantiate
+ but /not/ deeply instantiate (#26331). See Note [View patterns and polymorphism]
+ in GHC.Tc.Gen.Pat. This the only place we use IIF_ShallowRho.
+
+Why do we want to deeply instantiate, ever? Why isn't top-instantiation enough?
+Answer: to accept the following program (T26225b) with -XDeepSubsumption, we
+need to deeply instantiate when inferring in checkResultTy:
+
+ f :: Int -> (forall a. a->a)
+ g :: Int -> Bool -> Bool
+
+ test b =
+ case b of
+ True -> f
+ False -> g
+
+If we don't deeply instantiate in the branches of the case expression, we will
+try to unify the type of 'f' with that of 'g', which fails. If we instead
+deeply instantiate 'f', we will fill the 'InferResult' with 'Int -> alpha -> alpha'
+which then successfully unifies with the type of 'g' when we come to fill the
+'InferResult' hole a second time for the second case branch.
+-}
{-
************************************************************************
@@ -1337,7 +1393,7 @@ tcSubTypeMono rn_expr act_ty exp_ty
, text "act_ty:" <+> ppr act_ty
, text "rn_expr:" <+> ppr rn_expr]) $
case exp_ty of
- Infer inf_res -> fillInferResult act_ty inf_res
+ Infer inf_res -> fillInferResultNoInst act_ty inf_res
Check exp_ty -> unifyType (Just $ HsExprRnThing rn_expr) act_ty exp_ty
------------------------
@@ -1351,7 +1407,7 @@ tcSubTypePat inst_orig ctxt (Check ty_actual) ty_expected
= tc_sub_type unifyTypeET inst_orig ctxt ty_actual ty_expected
tcSubTypePat _ _ (Infer inf_res) ty_expected
- = do { co <- fillInferResult ty_expected inf_res
+ = do { co <- fillInferResultNoInst ty_expected inf_res
-- In patterns we do not instantatiate
; return (mkWpCastN (mkSymCo co)) }
@@ -1377,7 +1433,7 @@ tcSubTypeDS rn_expr act_rho exp_rho
-- | Checks that the 'actual' type is more polymorphic than the 'expected' type.
tcSubType :: CtOrigin -- ^ Used when instantiating
-> UserTypeCtxt -- ^ Used when skolemising
- -> Maybe TypedThing -- ^ The expression that has type 'actual' (if known)
+ -> Maybe TypedThing -- ^ The expression that has type 'actual' (if known)
-> TcSigmaType -- ^ Actual type
-> ExpRhoType -- ^ Expected type
-> TcM HsWrapper
@@ -1386,10 +1442,7 @@ tcSubType inst_orig ctxt m_thing ty_actual res_ty
Check ty_expected -> tc_sub_type (unifyType m_thing) inst_orig ctxt
ty_actual ty_expected
- Infer inf_res -> do { (wrap, rho) <- topInstantiate inst_orig ty_actual
- -- See Note [Instantiation of InferResult]
- ; inst <- fillInferResultDS inst_orig rho inf_res
- ; return (inst <.> wrap) }
+ Infer inf_res -> fillInferResult inst_orig ty_actual inf_res
---------------
tcSubTypeSigma :: CtOrigin -- where did the actual type arise / why are we
@@ -1428,47 +1481,6 @@ addSubTypeCtxt ty_actual ty_expected thing_inside
; return (tidy_env, SubTypeCtxt ty_expected ty_actual) }
-{- Note [Instantiation of InferResult]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-When typechecking expressions (not types, not patterns), we always instantiate
-before filling in InferResult, so that the result is a TcRhoType.
-See #17173 for discussion.
-
-For example:
-
-1. Consider
- f x = (*)
- We want to instantiate the type of (*) before returning, else we
- will infer the type
- f :: forall {a}. a -> forall b. Num b => b -> b -> b
- This is surely confusing for users.
-
- And worse, the monomorphism restriction won't work properly. The MR is
- dealt with in simplifyInfer, and simplifyInfer has no way of
- instantiating. This could perhaps be worked around, but it may be
- hard to know even when instantiation should happen.
-
-2. Another reason. Consider
- f :: (?x :: Int) => a -> a
- g y = let ?x = 3::Int in f
- Here want to instantiate f's type so that the ?x::Int constraint
- gets discharged by the enclosing implicit-parameter binding.
-
-3. Suppose one defines plus = (+). If we instantiate lazily, we will
- infer plus :: forall a. Num a => a -> a -> a. However, the monomorphism
- restriction compels us to infer
- plus :: Integer -> Integer -> Integer
- (or similar monotype). Indeed, the only way to know whether to apply
- the monomorphism restriction at all is to instantiate
-
-There is one place where we don't want to instantiate eagerly,
-namely in GHC.Tc.Module.tcRnExpr, which implements GHCi's :type
-command. See Note [Implementing :type] in GHC.Tc.Module.
-
-This also means that, if DeepSubsumption is enabled, we should also instantiate
-deeply; we do this by using fillInferResultDS.
--}
-
---------------
tc_sub_type :: (TcType -> TcType -> TcM TcCoercionN) -- How to unify
-> CtOrigin -- Used when instantiating
@@ -2133,7 +2145,17 @@ deeplySkolemise skol_info ty
= return (idHsWrapper, [], [], substTy subst ty)
-- substTy is a quick no-op on an empty substitution
+dsInstantiate :: CtOrigin -> TcType -> TcM (HsWrapper, Type)
+-- Do topInstantiate or deeplyInstantiate, depending on -XDeepSubsumption
+dsInstantiate orig ty
+ = do { ds_flag <- getDeepSubsumptionFlag
+ ; case ds_flag of
+ Shallow -> topInstantiate orig ty
+ Deep -> deeplyInstantiate orig ty }
+
deeplyInstantiate :: CtOrigin -> TcType -> TcM (HsWrapper, Type)
+-- Instantiate invisible foralls, even ones nested
+-- (to the right) under arrows
deeplyInstantiate orig ty
= go init_subst ty
where
@@ -3342,8 +3364,9 @@ mapCheck f xs
-- | Options describing how to deal with a type equality
-- in the eager unifier. See 'checkTyEqRhs'
data TyEqFlags m a
- -- | LHS is a type family application; we are not unifying.
- = TEFTyFam
+ = -- | TFTyFam: LHS is a type family application
+ -- Invariant: we are not unifying; see `notUnifying_TEFTask`
+ TEFTyFam
{ tefTyFam_occursCheck :: CheckTyEqProblem
-- ^ The 'CheckTyEqProblem' to report for occurs-check failures
-- (soluble or insoluble)
@@ -3352,7 +3375,8 @@ data TyEqFlags m a
, tef_fam_app :: TyEqFamApp m a
-- ^ How to deal with type family applications
}
- -- | LHS is a 'TyVar'.
+
+ -- | TEFTyVar: LHS is a 'TyVar'.
| TEFTyVar
-- NB: this constructor does not actually store a 'TyVar', in order to
-- support being called from 'makeTypeConcrete' (which works as if we
=====================================
testsuite/tests/patsyn/should_compile/T26331.hs
=====================================
@@ -0,0 +1,47 @@
+{-# LANGUAGE DeepSubsumption #-}
+
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE TypeAbstractions #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+
+module T26331 where
+
+import Data.Kind (Constraint, Type)
+
+type Apply :: (k1 ~> k2) -> k1 -> k2
+type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
+
+type (~>) :: Type -> Type -> Type
+type a ~> b = TyFun a b -> Type
+infixr 0 ~>
+
+data TyFun :: Type -> Type -> Type
+
+type Sing :: k -> Type
+type family Sing @k :: k -> Type
+
+type SingFunction2 :: (a1 ~> a2 ~> b) -> Type
+type SingFunction2 (f :: a1 ~> a2 ~> b) =
+ forall t1 t2. Sing t1 -> Sing t2 -> Sing (f `Apply` t1 `Apply` t2)
+
+unSingFun2 :: forall f. Sing f -> SingFunction2 f
+-- unSingFun2 :: forall f. Sing f -> forall t1 t2. blah
+unSingFun2 sf x = error "urk"
+
+singFun2 :: forall f. SingFunction2 f -> Sing f
+singFun2 f = error "urk"
+
+-------- This is the tricky bit -------
+pattern SLambda2 :: forall f. SingFunction2 f -> Sing f
+pattern SLambda2 x <- (unSingFun2 -> x) -- We want to push down (SingFunction2 f)
+ -- /uninstantiated/ into the pattern `x`
+ where
+ SLambda2 lam2 = singFun2 lam2
+
=====================================
testsuite/tests/patsyn/should_compile/T26331a.hs
=====================================
@@ -0,0 +1,11 @@
+{-# LANGUAGE DeepSubsumption #-}
+{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE RankNTypes #-}
+
+module T26331a where
+
+pair :: forall a. Bool -> a -> forall b. b -> (a,b)
+pair = error "urk"
+
+f :: Int -> ((Int,Bool),(Int,Char))
+f (pair True -> x) = (x True, x 'c') -- (x :: forall b. b -> (Int,b))
=====================================
testsuite/tests/patsyn/should_compile/all.T
=====================================
@@ -85,3 +85,5 @@ test('T21531', [ grep_errmsg(r'INLINE') ], compile, ['-ddump-ds'])
test('T22521', normal, compile, [''])
test('T23038', normal, compile_fail, [''])
test('T22328', normal, compile, [''])
+test('T26331', normal, compile, [''])
+test('T26331a', normal, compile, [''])
=====================================
testsuite/tests/typecheck/should_compile/T26346.hs
=====================================
@@ -0,0 +1,103 @@
+{-# LANGUAGE GHC2024 #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+module T26346 (warble) where
+
+import Data.Kind (Type)
+import Data.Type.Equality ((:~:)(..))
+
+type Nat :: Type
+data Nat = Z | S Nat
+
+type SNat :: Nat -> Type
+data SNat n where
+ SZ :: SNat Z
+ SS :: SNat n -> SNat (S n)
+
+type NatPlus :: Nat -> Nat -> Nat
+type family NatPlus a b where
+ NatPlus Z b = b
+ NatPlus (S a) b = S (NatPlus a b)
+
+sNatPlus ::
+ forall (a :: Nat) (b :: Nat).
+ SNat a ->
+ SNat b ->
+ SNat (NatPlus a b)
+sNatPlus SZ b = b
+sNatPlus (SS a) b = SS (sNatPlus a b)
+
+data Bin
+ = Zero
+ | Even Bin
+ | Odd Bin
+
+type SBin :: Bin -> Type
+data SBin b where
+ SZero :: SBin Zero
+ SEven :: SBin n -> SBin (Even n)
+ SOdd :: SBin n -> SBin (Odd n)
+
+type Incr :: Bin -> Bin
+type family Incr b where
+ Incr Zero = Odd Zero -- 0 + 1 = (2*0) + 1
+ Incr (Even n) = Odd n -- 2n + 1
+ Incr (Odd n) = Even (Incr n) -- (2n + 1) + 1 = 2*(n + 1)
+
+type BinToNat :: Bin -> Nat
+type family BinToNat b where
+ BinToNat Zero = Z
+ BinToNat (Even n) = NatPlus (BinToNat n) (BinToNat n)
+ BinToNat (Odd n) = S (NatPlus (BinToNat n) (BinToNat n))
+
+sBinToNat ::
+ forall (b :: Bin).
+ SBin b ->
+ SNat (BinToNat b)
+sBinToNat SZero = SZ
+sBinToNat (SEven n) = sNatPlus (sBinToNat n) (sBinToNat n)
+sBinToNat (SOdd n) = SS (sNatPlus (sBinToNat n) (sBinToNat n))
+
+warble ::
+ forall (b :: Bin).
+ SBin b ->
+ BinToNat (Incr b) :~: S (BinToNat b)
+warble SZero = Refl
+warble (SEven {}) = Refl
+warble (SOdd sb) | Refl <- warble sb
+ , Refl <- plusComm sbn (SS sbn)
+ = Refl
+ where
+ sbn = sBinToNat sb
+
+ plus0R ::
+ forall (n :: Nat).
+ SNat n ->
+ NatPlus n Z :~: n
+ plus0R SZ = Refl
+ plus0R (SS sn)
+ | Refl <- plus0R sn
+ = Refl
+
+ plusSnR ::
+ forall (n :: Nat) (m :: Nat).
+ SNat n ->
+ SNat m ->
+ NatPlus n (S m) :~: S (NatPlus n m)
+ plusSnR SZ _ = Refl
+ plusSnR (SS sn) sm
+ | Refl <- plusSnR sn sm
+ = Refl
+
+ plusComm ::
+ forall (n :: Nat) (m :: Nat).
+ SNat n ->
+ SNat m ->
+ NatPlus n m :~: NatPlus m n
+ plusComm SZ sm
+ | Refl <- plus0R sm
+ = Refl
+ plusComm (SS sn) sm
+ | Refl <- plusComm sn sm
+ , Refl <- plusSnR sm sn
+ = Refl
=====================================
testsuite/tests/typecheck/should_compile/T26350.hs
=====================================
@@ -0,0 +1,18 @@
+{-# LANGUAGE DeepSubsumption #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+
+{-# OPTIONS_GHC -dcore-lint #-}
+
+module T26350 where
+
+import Control.Arrow (first)
+
+infix 6 .-.
+
+class AffineSpace p where
+ type Diff p
+ (.-.) :: p -> p -> Diff p
+
+affineCombo :: (AffineSpace p, v ~ Diff p) => p -> (p,v) -> (v,v)
+affineCombo z l = first (.-. z) l
=====================================
testsuite/tests/typecheck/should_compile/T26358.hs
=====================================
@@ -0,0 +1,48 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module T26358 where
+import Data.Kind
+import Data.Proxy
+
+{- Two failing tests, described in GHC.Core.Unify
+ Note [Shortcomings of the apartness test]
+
+Explanation for TF2
+* We try to reduce
+ (TF2 (F (G Float)) (F Int) (G Float))
+* We can only do so if those arguments are apart from the first
+ equation of TF2, namely (Bool,Char,Int).
+* So we try to unify
+ [F (G Float), F Int, G Float] ~ [Bool, Char, Int]
+* They really are apart, but we can't quite spot that yet;
+ hence #26358
+
+TF1 is similar.
+-}
+
+
+type TF1 :: Type -> Type -> Type -> Type
+type family TF1 a b c where
+ TF1 Bool Char a = Word
+ TF1 a b c = (a,b,c)
+
+type F :: Type -> Type
+type family F a where
+
+foo :: Proxy a
+ -> Proxy (TF1 (F a) (F Int) Int)
+ -> Proxy (F a, F Int, Int)
+foo _ px = px
+
+type TF2 :: Type -> Type -> Type -> Type
+type family TF2 a b c where
+ TF2 Bool Char Int = Word
+ TF2 a b c = (a,b,c)
+
+type G :: Type -> Type
+type family G a where
+
+bar :: Proxy (TF2 (F (G Float)) (F Int) (G Float))
+ -> Proxy (F (G Float), F Int, G Float)
+bar px = px
+
=====================================
testsuite/tests/typecheck/should_compile/all.T
=====================================
@@ -862,6 +862,7 @@ test('DeepSubsumption06', normal, compile, ['-XHaskell98'])
test('DeepSubsumption07', normal, compile, ['-XHaskell2010'])
test('DeepSubsumption08', normal, compile, [''])
test('DeepSubsumption09', normal, compile, [''])
+test('T26350', normal, compile, [''])
test('T26225', normal, compile, [''])
test('T26225b', normal, compile, [''])
test('T21765', normal, compile, [''])
@@ -945,3 +946,5 @@ test('T25992', normal, compile, [''])
test('T14010', normal, compile, [''])
test('T26256a', normal, compile, [''])
test('T25992a', normal, compile, [''])
+test('T26346', normal, compile, [''])
+test('T26358', expect_broken(26358), compile, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/299b483c9e86a26467ab3e460c1371…
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/299b483c9e86a26467ab3e460c1371…
You're receiving this email because of your account on gitlab.haskell.org.
1
0
[Git][ghc/ghc][wip/fendor/stack-annotation-with-backtraces] 12 commits: Revert "STM: don't create a transaction in the rhs of catchRetry# (#26028)"
by Hannes Siebenhandl (＠fendor) 29 Aug '25
by Hannes Siebenhandl (＠fendor) 29 Aug '25
29 Aug '25
Hannes Siebenhandl pushed to branch wip/fendor/stack-annotation-with-backtraces at Glasgow Haskell Compiler / GHC
Commits:
5b5d9d47 by Ben Gamari at 2025-08-25T14:29:35-04:00
Revert "STM: don't create a transaction in the rhs of catchRetry# (#26028)"
This reverts commit 0a5836891ca29836a24c306d2a364c2e4b5377fd
- - - - -
10f06163 by Cheng Shao at 2025-08-25T14:30:16-04:00
wasm: ensure setKeepCAFs() is called in ghci
This patch is a critical bugfix for #26106, see comment and linked
issue for details.
- - - - -
bedc1004 by Cheng Shao at 2025-08-26T09:31:18-04:00
compiler: use zero cost coerce in hoopl setElems/mapToList
This patch is a follow-up of !14680 and changes setElems/mapToList in
GHC/Cmm/Dataflow/Label to use coerce instead of mapping mkHooplLabel
over the keys.
- - - - -
13250d97 by Ryan Scott at 2025-08-26T09:31:59-04:00
Reject infix promoted data constructors without DataKinds
In the rename, make sure to apply the same `DataKinds` checks for both
`HsTyVar` (for prefix promoted data constructors) and `HsOpTy` (for infix
promoted data constructors) alike.
Fixes #26318.
- - - - -
37655c46 by Teo Camarasu at 2025-08-26T15:24:51-04:00
tests: disable T22859 under LLVM
This test was failing under the LLVM backend since the allocations
differ from the NCG.
Resolves #26282
- - - - -
2cbba9d6 by Teo Camarasu at 2025-08-26T15:25:33-04:00
base-exports: update version numbers
As the version of the compiler has been bumped, a lot of the embedded
version numbers will need to be updated if we ever run this test with
`--test-accept` so let's just update them now, and keep future diffs
clean.
- - - - -
f9f2ffcf by Alexandre Esteves at 2025-08-27T07:19:14-04:00
Import new name for 'utimbuf' on windows to fix #26337
Fixes an `-Wincompatible-pointer-types` instance that turns into an error on
recent toolchains and surfaced as such on nixpkgs when doing linux->ucrt cross.
This long-standing warning has been present at least since 9.4:
```
C:\GitLabRunner\builds\0\1709189\tmp\ghc16652_0\ghc_4.c:26:115: error:
warning: incompatible pointer types passing 'struct utimbuf *' to parameter of type 'struct _utimbuf *' [-Wincompatible-pointer-types]
|
26 | HsInt32 ghczuwrapperZC9ZCbaseZCSystemziPosixziInternalsZCzuutime(char* a1, struct utimbuf* a2) {return _utime(a1, a2);}
| ^
HsInt32 ghczuwrapperZC9ZCbaseZCSystemziPosixziInternalsZCzuutime(char* a1, struct utimbuf* a2) {return _utime(a1, a2);}
^~
C:\GitLabRunner\builds\0\1709189\_build\stage0\lib\..\..\mingw\x86_64-w64-mingw32\include\sys\utime.h:109:72: error:
note: passing argument to parameter '_Utimbuf' here
|
109 | __CRT_INLINE int __cdecl _utime(const char *_Filename,struct _utimbuf *_Utimbuf) {
| ^
__CRT_INLINE int __cdecl _utime(const char *_Filename,struct _utimbuf *_Utimbuf) {
```
- - - - -
ae89f000 by Hassan Al-Awwadi at 2025-08-27T07:19:56-04:00
Adds the fucnction addDependentDirectory to Q, resolving issue #26148.
This function adds a new directory to the list of things a module depends upon. That means that when the contents of the directory change, the recompilation checker will notice this and the module will be recompiled. Documentation has also been added for addDependentFunction and addDependentDirectory in the user guide.
- - - - -
1a361d8b by fendor at 2025-08-28T13:48:09+02:00
Move stack decoding logic from ghc-heap to ghc-internal
The stack decoding logic in `ghc-heap` is more sophisticated than the one
currently employed in `CloneStack`. We want to use the stack decoding
implementation from `ghc-heap` in `base`.
We cannot simply depend on `ghc-heap` in `base` due do bootstrapping
issues.
Thus, we move the code that is necessary to implement stack decoding to
`ghc-internal`. This is the right location, as we don't want to add a
new API to `base`.
Moving the stack decoding logic and re-exposing it in ghc-heap is
insufficient, though, as we have a dependency cycle between.
* ghc-heap depends on stage1:ghc-internal
* stage0:ghc depends on stage0:ghc-heap
To fix this, we remove ghc-heap from the set of `stage0` dependencies.
This is not entirely straight-forward, as a couple of boot dependencies,
such as `ghci` depend on `ghc-heap`.
Luckily, the boot compiler of GHC is now >=9.10, so we can migrate `ghci`
to use `ghc-internal` instead of `ghc-heap`, which already exports the
relevant modules.
However, we cannot 100% remove ghc's dependency on `ghc-heap`, since
when we compile `stage0:ghc`, `stage1:ghc-internal` is not yet
available.
Thus, when we compile with the boot-compiler, we still depend on an
older version of `ghc-heap`, and only use the modules from `ghc-internal`,
if the `ghc-internal` version is recent enough.
-------------------------
Metric Increase:
T24602_perf_size
T25046_perf_size_gzip
T25046_perf_size_unicode
T25046_perf_size_unicode_gzip
size_hello_artifact
size_hello_artifact_gzip
size_hello_unicode
size_hello_unicode_gzip
-------------------------
These metric increases are unfortunate, they are most likely caused by
the larger (literally in terms of lines of code) stack decoder implementation
that are now linked into hello-word binaries.
On linux, it is almost a 10% increase, which is considerable.
- - - - -
15c35e87 by fendor at 2025-08-28T13:48:10+02:00
Implement `decode` in terms of `decodeStackWithIpe`
Uses the more efficient stack decoder implementation.
- - - - -
be4cbbf4 by fendor at 2025-08-28T13:48:10+02:00
Remove stg_decodeStackzh
- - - - -
742e9e04 by fendor at 2025-08-29T09:00:48+02:00
Expose Stack Annotation frames in IPE backtraces by default
When decoding the Haskell-native call stack and displaying the IPE information
for the stack frames, we print the `StackAnnotation` of the `AnnFrame` by default.
This means, when an exception is thrown, any intermediate stack annotations will
be displayed in the `IPE Backtrace`.
Example backtrace:
```
Exception: ghc-internal:GHC.Internal.Exception.ErrorCall:
Oh no!
IPE backtrace:
annotateCallStackIO, called at app/Main.hs:48:10 in backtrace-0.1.0.0-inplace-server:Main
annotateCallStackIO, called at app/Main.hs:46:13 in backtrace-0.1.0.0-inplace-server:Main
Main.handler (app/Main.hs:(46,1)-(49,30))
Main.liftIO (src/Servant/Server/Internal/Handler.hs:30:36-42)
Servant.Server.Internal.Delayed.runHandler' (src/Servant/Server/Internal/Handler.hs:27:31-41)
Control.Monad.Trans.Resource.runResourceT (./Control/Monad/Trans/Resource.hs:(192,14)-(197,18))
Network.Wai.Handler.Warp.HTTP1.processRequest (./Network/Wai/Handler/Warp/HTTP1.hs:195:20-22)
Network.Wai.Handler.Warp.HTTP1.processRequest (./Network/Wai/Handler/Warp/HTTP1.hs:(195,5)-(203,31))
Network.Wai.Handler.Warp.HTTP1.http1server.loop (./Network/Wai/Handler/Warp/HTTP1.hs:(141,9)-(157,42))
HasCallStack backtrace:
error, called at app/Main.hs:48:32 in backtrace-0.1.0.0-inplace-server:Main
```
The first two entries have been added by `annotateCallStackIO`, defined in `annotateCallStackIO`.
- - - - -
93 changed files:
- compiler/GHC/ByteCode/Types.hs
- compiler/GHC/Cmm/Dataflow/Label.hs
- compiler/GHC/HsToCore/Usage.hs
- compiler/GHC/Iface/Make.hs
- compiler/GHC/Iface/Recomp.hs
- compiler/GHC/Iface/Recomp/Types.hs
- compiler/GHC/Rename/HsType.hs
- compiler/GHC/Runtime/Heap/Inspect.hs
- compiler/GHC/Tc/Gen/Splice.hs
- compiler/GHC/Tc/Types.hs
- compiler/GHC/Tc/Utils/Monad.hs
- compiler/GHC/Unit/Finder.hs
- compiler/GHC/Unit/Finder/Types.hs
- compiler/GHC/Unit/Module/Deps.hs
- compiler/ghc.cabal.in
- docs/users_guide/9.16.1-notes.rst
- docs/users_guide/separate_compilation.rst
- hadrian/src/Rules/ToolArgs.hs
- hadrian/src/Settings/Default.hs
- libraries/base/src/GHC/Stack/CloneStack.hs
- libraries/ghc-experimental/src/GHC/Stack/Annotation/Experimental.hs
- libraries/ghc-heap/GHC/Exts/Heap/ClosureTypes.hs
- libraries/ghc-heap/GHC/Exts/Heap/Closures.hs
- + libraries/ghc-heap/GHC/Exts/Heap/Constants.hs
- + libraries/ghc-heap/GHC/Exts/Heap/InfoTable.hs
- + libraries/ghc-heap/GHC/Exts/Heap/InfoTable/Types.hs
- + libraries/ghc-heap/GHC/Exts/Heap/InfoTableProf.hs
- libraries/ghc-heap/GHC/Exts/Heap/ProfInfo/Types.hs
- + libraries/ghc-heap/GHC/Exts/Stack/Constants.hs
- libraries/ghc-heap/GHC/Exts/Stack/Decode.hs
- libraries/ghc-heap/ghc-heap.cabal.in
- − libraries/ghc-heap/tests/stack-annotation/ann_frame004.stdout
- libraries/ghc-heap/cbits/HeapPrim.cmm → libraries/ghc-internal/cbits/HeapPrim.cmm
- libraries/ghc-heap/cbits/Stack.cmm → libraries/ghc-internal/cbits/Stack.cmm
- libraries/ghc-internal/cbits/StackCloningDecoding.cmm
- libraries/ghc-heap/cbits/Stack_c.c → libraries/ghc-internal/cbits/Stack_c.c
- libraries/ghc-internal/ghc-internal.cabal.in
- libraries/ghc-internal/jsbits/base.js
- libraries/ghc-internal/src/GHC/Internal/Exception/Backtrace.hs
- + libraries/ghc-internal/src/GHC/Internal/Heap/Closures.hs
- libraries/ghc-heap/GHC/Exts/Heap/Constants.hsc → libraries/ghc-internal/src/GHC/Internal/Heap/Constants.hsc
- libraries/ghc-heap/GHC/Exts/Heap/InfoTable.hsc → libraries/ghc-internal/src/GHC/Internal/Heap/InfoTable.hsc
- libraries/ghc-heap/GHC/Exts/Heap/InfoTable/Types.hsc → libraries/ghc-internal/src/GHC/Internal/Heap/InfoTable/Types.hsc
- libraries/ghc-heap/GHC/Exts/Heap/InfoTableProf.hsc → libraries/ghc-internal/src/GHC/Internal/Heap/InfoTableProf.hsc
- + libraries/ghc-internal/src/GHC/Internal/Heap/ProfInfo/Types.hs
- + libraries/ghc-internal/src/GHC/Internal/Stack/Annotation.hs
- libraries/ghc-internal/src/GHC/Internal/Stack/CloneStack.hs
- libraries/ghc-heap/GHC/Exts/Stack/Constants.hsc → libraries/ghc-internal/src/GHC/Internal/Stack/Constants.hsc
- + libraries/ghc-internal/src/GHC/Internal/Stack/Decode.hs
- libraries/ghc-internal/src/GHC/Internal/System/Posix/Internals.hs
- libraries/ghc-internal/src/GHC/Internal/TH/Syntax.hs
- libraries/ghc-heap/tests/stack-annotation/Makefile → libraries/ghc-internal/tests/stack-annotation/Makefile
- libraries/ghc-heap/tests/stack-annotation/TestUtils.hs → libraries/ghc-internal/tests/stack-annotation/TestUtils.hs
- libraries/ghc-heap/tests/stack-annotation/all.T → libraries/ghc-internal/tests/stack-annotation/all.T
- libraries/ghc-heap/tests/stack-annotation/ann_frame001.hs → libraries/ghc-internal/tests/stack-annotation/ann_frame001.hs
- libraries/ghc-heap/tests/stack-annotation/ann_frame001.stdout → libraries/ghc-internal/tests/stack-annotation/ann_frame001.stdout
- libraries/ghc-heap/tests/stack-annotation/ann_frame002.hs → libraries/ghc-internal/tests/stack-annotation/ann_frame002.hs
- libraries/ghc-heap/tests/stack-annotation/ann_frame002.stdout → libraries/ghc-internal/tests/stack-annotation/ann_frame002.stdout
- libraries/ghc-heap/tests/stack-annotation/ann_frame003.hs → libraries/ghc-internal/tests/stack-annotation/ann_frame003.hs
- libraries/ghc-heap/tests/stack-annotation/ann_frame003.stdout → libraries/ghc-internal/tests/stack-annotation/ann_frame003.stdout
- libraries/ghc-heap/tests/stack-annotation/ann_frame004.hs → libraries/ghc-internal/tests/stack-annotation/ann_frame004.hs
- + libraries/ghc-internal/tests/stack-annotation/ann_frame004.stdout
- libraries/ghci/GHCi/Message.hs
- libraries/ghci/GHCi/TH.hs
- libraries/ghci/ghci.cabal.in
- libraries/template-haskell/Language/Haskell/TH/Syntax.hs
- rts/CloneStack.c
- rts/CloneStack.h
- rts/PrimOps.cmm
- rts/RaiseAsync.c
- rts/RtsSymbols.c
- rts/STM.c
- testsuite/.gitignore
- testsuite/tests/interface-stability/base-exports.stdout
- testsuite/tests/interface-stability/base-exports.stdout-javascript-unknown-ghcjs
- testsuite/tests/interface-stability/base-exports.stdout-mingw32
- testsuite/tests/interface-stability/base-exports.stdout-ws-32
- testsuite/tests/interface-stability/ghc-experimental-exports.stdout
- testsuite/tests/interface-stability/ghc-experimental-exports.stdout-mingw32
- testsuite/tests/interface-stability/template-haskell-exports.stdout
- − testsuite/tests/lib/stm/T26028.hs
- − testsuite/tests/lib/stm/T26028.stdout
- − testsuite/tests/lib/stm/all.T
- testsuite/tests/rts/all.T
- testsuite/tests/th/Makefile
- + testsuite/tests/th/TH_Depends_Dir.hs
- + testsuite/tests/th/TH_Depends_Dir.stdout
- + testsuite/tests/th/TH_Depends_Dir_External.hs
- testsuite/tests/th/all.T
- + testsuite/tests/typecheck/should_fail/T26318.hs
- + testsuite/tests/typecheck/should_fail/T26318.stderr
- testsuite/tests/typecheck/should_fail/all.T
- utils/jsffi/dyld.mjs
The diff was not included because it is too large.
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/36314d049da3f39f0196877be1c20f…
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/36314d049da3f39f0196877be1c20f…
You're receiving this email because of your account on gitlab.haskell.org.
1
0
[Git][ghc/ghc][wip/marge_bot_batch_merge_job] 3 commits: Fix orientation in HsWrapper composition (<.>)
by Marge Bot (＠marge-bot) 29 Aug '25
by Marge Bot (＠marge-bot) 29 Aug '25
29 Aug '25
Marge Bot pushed to branch wip/marge_bot_batch_merge_job at Glasgow Haskell Compiler / GHC
Commits:
8adfc222 by sheaf at 2025-08-28T19:47:17-04:00
Fix orientation in HsWrapper composition (<.>)
This commit fixes the order in which WpCast HsWrappers are composed,
fixing a bug introduced in commit 56b32c5a2d5d7cad89a12f4d74dc940e086069d1.
Fixes #26350
- - - - -
b9f585ab by Oleg Grenrus at 2025-08-29T03:00:22-04:00
Generalise thNameToGhcName by adding HasHscEnv
There were multiple single monad-specific `getHscEnv` across codebase.
HasHscEnv is modelled on HasDynFlags.
My first idea was to simply add thNameToGhcNameHsc and
thNameToGhcNameTc, but those would been exactly the same
as thNameToGhcName already.
Also add an usage example to thNameToGhcName and mention that it's
recommended way of looking up names in GHC plugins
- - - - -
52ba0a3d by fendor at 2025-08-29T03:00:23-04:00
configure: Bump minimal bootstrap GHC version to 9.10
- - - - -
12 changed files:
- .gitlab-ci.yml
- compiler/GHC/Core/Opt/Monad.hs
- compiler/GHC/Driver/Env.hs
- compiler/GHC/Driver/Env/Types.hs
- compiler/GHC/Driver/Main.hs
- compiler/GHC/Plugins.hs
- compiler/GHC/StgToByteCode.hs
- compiler/GHC/Tc/Gen/App.hs
- compiler/GHC/Tc/Types/Evidence.hs
- configure.ac
- + testsuite/tests/typecheck/should_compile/T26350.hs
- testsuite/tests/typecheck/should_compile/all.T
Changes:
=====================================
.gitlab-ci.yml
=====================================
@@ -104,6 +104,7 @@ workflow:
# which versions of GHC to allow bootstrap with
.bootstrap_matrix : &bootstrap_matrix
matrix:
+ # If you update this version, be sure to also update 'MinBootGhcVersion' in configure.ac
- GHC_VERSION: 9.10.1
DOCKER_IMAGE: "registry.gitlab.haskell.org/ghc/ci-images/x86_64-linux-deb12-ghc9_10:$DOCKE…"
- GHC_VERSION: 9.12.2
=====================================
compiler/GHC/Core/Opt/Monad.hs
=====================================
@@ -16,7 +16,7 @@ module GHC.Core.Opt.Monad (
mapDynFlagsCoreM, dropSimplCount,
-- ** Reading from the monad
- getHscEnv, getModule,
+ getModule,
initRuleEnv, getExternalRuleBase,
getDynFlags, getPackageFamInstEnv,
getInteractiveContext,
@@ -243,8 +243,8 @@ liftIOWithCount what = liftIO what >>= (\(count, x) -> addSimplCount count >> re
************************************************************************
-}
-getHscEnv :: CoreM HscEnv
-getHscEnv = read cr_hsc_env
+instance HasHscEnv CoreM where
+ getHscEnv = read cr_hsc_env
getHomeRuleBase :: CoreM RuleBase
getHomeRuleBase = read cr_rule_base
=====================================
compiler/GHC/Driver/Env.hs
=====================================
@@ -2,6 +2,7 @@
module GHC.Driver.Env
( Hsc(..)
, HscEnv (..)
+ , HasHscEnv (..)
, hsc_mod_graph
, setModuleGraph
, hscUpdateFlags
@@ -49,7 +50,7 @@ import GHC.Driver.Errors ( printOrThrowDiagnostics )
import GHC.Driver.Errors.Types ( GhcMessage )
import GHC.Driver.Config.Logger (initLogFlags)
import GHC.Driver.Config.Diagnostic (initDiagOpts, initPrintConfig)
-import GHC.Driver.Env.Types ( Hsc(..), HscEnv(..) )
+import GHC.Driver.Env.Types ( Hsc(..), HscEnv(..), HasHscEnv (..) )
import GHC.Runtime.Context
import GHC.Runtime.Interpreter.Types (Interp)
=====================================
compiler/GHC/Driver/Env/Types.hs
=====================================
@@ -3,6 +3,7 @@
module GHC.Driver.Env.Types
( Hsc(..)
, HscEnv(..)
+ , HasHscEnv(..)
) where
import GHC.Driver.Errors.Types ( GhcMessage )
@@ -34,6 +35,9 @@ newtype Hsc a = Hsc (HscEnv -> Messages GhcMessage -> IO (a, Messages GhcMessage
deriving (Functor, Applicative, Monad, MonadIO)
via ReaderT HscEnv (StateT (Messages GhcMessage) IO)
+instance HasHscEnv Hsc where
+ getHscEnv = Hsc $ \e w -> return (e, w)
+
instance HasDynFlags Hsc where
getDynFlags = Hsc $ \e w -> return (hsc_dflags e, w)
@@ -109,3 +113,5 @@ data HscEnv
-- ^ LLVM configuration cache.
}
+class HasHscEnv m where
+ getHscEnv :: m HscEnv
=====================================
compiler/GHC/Driver/Main.hs
=====================================
@@ -368,9 +368,6 @@ clearDiagnostics = Hsc $ \_ _ -> return ((), emptyMessages)
logDiagnostics :: Messages GhcMessage -> Hsc ()
logDiagnostics w = Hsc $ \_ w0 -> return ((), w0 `unionMessages` w)
-getHscEnv :: Hsc HscEnv
-getHscEnv = Hsc $ \e w -> return (e, w)
-
handleWarnings :: Hsc ()
handleWarnings = do
diag_opts <- initDiagOpts <$> getDynFlags
=====================================
compiler/GHC/Plugins.hs
=====================================
@@ -143,7 +143,7 @@ import Data.Maybe
import GHC.Iface.Env ( lookupNameCache )
import GHC.Prelude
-import GHC.Utils.Monad ( mapMaybeM )
+import GHC.Utils.Monad ( MonadIO, mapMaybeM )
import GHC.ThToHs ( thRdrNameGuesses )
import GHC.Tc.Utils.Env ( lookupGlobal )
import GHC.Types.Name.Cache ( NameCache )
@@ -178,7 +178,22 @@ instance MonadThings CoreM where
-- exactly. Qualified or unqualified TH names will be dynamically bound
-- to names in the module being compiled, if possible. Exact TH names
-- will be bound to the name they represent, exactly.
-thNameToGhcName :: TH.Name -> CoreM (Maybe Name)
+--
+-- 'thNameToGhcName' can be used in 'CoreM', 'Hsc' and 'TcM' monads.
+--
+-- 'thNameToGhcName' is recommended way to lookup 'Name's in GHC plugins.
+--
+-- @
+-- {-# LANGUAGE TemplateHaskellQuotes #-}
+--
+-- getNames :: Hsc (Maybe Name, Maybe Name)
+-- getNames = do
+-- class_Eq <- thNameToGhcName ''Eq
+-- fun_eq <- thNameToGhcName '(==)
+-- return (classEq, fun_eq)
+-- @
+--
+thNameToGhcName :: (MonadIO m, HasHscEnv m) => TH.Name -> m (Maybe Name)
thNameToGhcName th_name = do
hsc_env <- getHscEnv
liftIO $ thNameToGhcNameIO (hsc_NC hsc_env) th_name
=====================================
compiler/GHC/StgToByteCode.hs
=====================================
@@ -2641,8 +2641,8 @@ runBc hsc_env this_mod mbs (BcM m)
instance HasDynFlags BcM where
getDynFlags = hsc_dflags <$> getHscEnv
-getHscEnv :: BcM HscEnv
-getHscEnv = BcM $ \env st -> return (bcm_hsc_env env, st)
+instance HasHscEnv BcM where
+ getHscEnv = BcM $ \env st -> return (bcm_hsc_env env, st)
getProfile :: BcM Profile
getProfile = targetProfile <$> getDynFlags
=====================================
compiler/GHC/Tc/Gen/App.hs
=====================================
@@ -430,7 +430,7 @@ tcApp rn_expr exp_res_ty
-- Step 5.2: typecheck the arguments, and monomorphise
-- any un-unified instantiation variables
; tc_args <- tcValArgs DoQL inst_args
- -- Step 5.3: zonk to expose the polymophism hidden under
+ -- Step 5.3: zonk to expose the polymorphism hidden under
-- QuickLook instantiation variables in `app_res_rho`
; app_res_rho <- liftZonkM $ zonkTcType app_res_rho
-- Step 5.4: subsumption check against the expected type
=====================================
compiler/GHC/Tc/Types/Evidence.hs
=====================================
@@ -206,9 +206,15 @@ instance Monoid HsWrapper where
(<.>) :: HsWrapper -> HsWrapper -> HsWrapper
WpHole <.> c = c
c <.> WpHole = c
-WpCast c1 <.> WpCast c2 = WpCast (c1 `mkTransCo` c2)
+WpCast c1 <.> WpCast c2 = WpCast (c2 `mkTransCo` c1)
-- If we can represent the HsWrapper as a cast, try to do so: this may avoid
-- unnecessary eta-expansion (see 'mkWpFun').
+ --
+ -- NB: <.> behaves like function composition:
+ --
+ -- WpCast c1 <.> WpCast c2 :: coercionLKind c2 ~> coercionRKind c1
+ --
+ -- This is thus the same as WpCast (c2 ; c1) and not WpCast (c1 ; c2).
c1 <.> c2 = c1 `WpCompose` c2
-- | Smart constructor to create a 'WpFun' 'HsWrapper', which avoids introducing
=====================================
configure.ac
=====================================
@@ -219,7 +219,7 @@ if test "$WithGhc" = ""
then
AC_MSG_ERROR([GHC is required.])
fi
-MinBootGhcVersion="9.8"
+MinBootGhcVersion="9.10"
FP_COMPARE_VERSIONS([$GhcVersion],[-lt],[$MinBootGhcVersion],
[AC_MSG_ERROR([GHC version $MinBootGhcVersion or later is required to compile GHC.])])
=====================================
testsuite/tests/typecheck/should_compile/T26350.hs
=====================================
@@ -0,0 +1,18 @@
+{-# LANGUAGE DeepSubsumption #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+
+{-# OPTIONS_GHC -dcore-lint #-}
+
+module T26350 where
+
+import Control.Arrow (first)
+
+infix 6 .-.
+
+class AffineSpace p where
+ type Diff p
+ (.-.) :: p -> p -> Diff p
+
+affineCombo :: (AffineSpace p, v ~ Diff p) => p -> (p,v) -> (v,v)
+affineCombo z l = first (.-. z) l
=====================================
testsuite/tests/typecheck/should_compile/all.T
=====================================
@@ -862,6 +862,7 @@ test('DeepSubsumption06', normal, compile, ['-XHaskell98'])
test('DeepSubsumption07', normal, compile, ['-XHaskell2010'])
test('DeepSubsumption08', normal, compile, [''])
test('DeepSubsumption09', normal, compile, [''])
+test('T26350', normal, compile, [''])
test('T26225', normal, compile, [''])
test('T26225b', normal, compile, [''])
test('T21765', normal, compile, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/dbbb3c391d47e9ff04ec4bb858f709…
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/dbbb3c391d47e9ff04ec4bb858f709…
You're receiving this email because of your account on gitlab.haskell.org.
1
0
[Git][ghc/ghc][master] Fix orientation in HsWrapper composition (<.>)
by Marge Bot (＠marge-bot) 28 Aug '25
by Marge Bot (＠marge-bot) 28 Aug '25
28 Aug '25
Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC
Commits:
8adfc222 by sheaf at 2025-08-28T19:47:17-04:00
Fix orientation in HsWrapper composition (<.>)
This commit fixes the order in which WpCast HsWrappers are composed,
fixing a bug introduced in commit 56b32c5a2d5d7cad89a12f4d74dc940e086069d1.
Fixes #26350
- - - - -
4 changed files:
- compiler/GHC/Tc/Gen/App.hs
- compiler/GHC/Tc/Types/Evidence.hs
- + testsuite/tests/typecheck/should_compile/T26350.hs
- testsuite/tests/typecheck/should_compile/all.T
Changes:
=====================================
compiler/GHC/Tc/Gen/App.hs
=====================================
@@ -430,7 +430,7 @@ tcApp rn_expr exp_res_ty
-- Step 5.2: typecheck the arguments, and monomorphise
-- any un-unified instantiation variables
; tc_args <- tcValArgs DoQL inst_args
- -- Step 5.3: zonk to expose the polymophism hidden under
+ -- Step 5.3: zonk to expose the polymorphism hidden under
-- QuickLook instantiation variables in `app_res_rho`
; app_res_rho <- liftZonkM $ zonkTcType app_res_rho
-- Step 5.4: subsumption check against the expected type
=====================================
compiler/GHC/Tc/Types/Evidence.hs
=====================================
@@ -206,9 +206,15 @@ instance Monoid HsWrapper where
(<.>) :: HsWrapper -> HsWrapper -> HsWrapper
WpHole <.> c = c
c <.> WpHole = c
-WpCast c1 <.> WpCast c2 = WpCast (c1 `mkTransCo` c2)
+WpCast c1 <.> WpCast c2 = WpCast (c2 `mkTransCo` c1)
-- If we can represent the HsWrapper as a cast, try to do so: this may avoid
-- unnecessary eta-expansion (see 'mkWpFun').
+ --
+ -- NB: <.> behaves like function composition:
+ --
+ -- WpCast c1 <.> WpCast c2 :: coercionLKind c2 ~> coercionRKind c1
+ --
+ -- This is thus the same as WpCast (c2 ; c1) and not WpCast (c1 ; c2).
c1 <.> c2 = c1 `WpCompose` c2
-- | Smart constructor to create a 'WpFun' 'HsWrapper', which avoids introducing
=====================================
testsuite/tests/typecheck/should_compile/T26350.hs
=====================================
@@ -0,0 +1,18 @@
+{-# LANGUAGE DeepSubsumption #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+
+{-# OPTIONS_GHC -dcore-lint #-}
+
+module T26350 where
+
+import Control.Arrow (first)
+
+infix 6 .-.
+
+class AffineSpace p where
+ type Diff p
+ (.-.) :: p -> p -> Diff p
+
+affineCombo :: (AffineSpace p, v ~ Diff p) => p -> (p,v) -> (v,v)
+affineCombo z l = first (.-. z) l
=====================================
testsuite/tests/typecheck/should_compile/all.T
=====================================
@@ -862,6 +862,7 @@ test('DeepSubsumption06', normal, compile, ['-XHaskell98'])
test('DeepSubsumption07', normal, compile, ['-XHaskell2010'])
test('DeepSubsumption08', normal, compile, [''])
test('DeepSubsumption09', normal, compile, [''])
+test('T26350', normal, compile, [''])
test('T26225', normal, compile, [''])
test('T26225b', normal, compile, [''])
test('T21765', normal, compile, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/8adfc22242b068417acc43cc682b79f…
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/8adfc22242b068417acc43cc682b79f…
You're receiving this email because of your account on gitlab.haskell.org.
1
0
Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC
Commits:
00478944 by Simon Peyton Jones at 2025-08-27T16:48:30+01:00
Comments only
- - - - -
a7884589 by Simon Peyton Jones at 2025-08-28T11:08:23+01:00
Type-family occurs check in unification
The occurs check in `GHC.Core.Unify.uVarOrFam` was inadequate in dealing
with type families.
Better now. See Note [The occurs check in the Core unifier].
As I did this I realised that the whole apartness thing is trickier than I
thought: see the new Note [Shortcomings of the apartness test]
- - - - -
6 changed files:
- compiler/GHC/Core/TyCo/Compare.hs
- compiler/GHC/Core/Unify.hs
- compiler/GHC/Tc/Utils/Unify.hs
- + testsuite/tests/typecheck/should_compile/T26346.hs
- + testsuite/tests/typecheck/should_compile/T26358.hs
- testsuite/tests/typecheck/should_compile/all.T
Changes:
=====================================
compiler/GHC/Core/TyCo/Compare.hs
=====================================
@@ -229,6 +229,8 @@ tcEqTyConApps tc1 args1 tc2 args2
= tc1 == tc2 && tcEqTyConAppArgs args1 args2
tcEqTyConAppArgs :: [Type] -> [Type] -> Bool
+-- Args do not have to have equal length;
+-- we discard the excess of the longer one
tcEqTyConAppArgs args1 args2
= and (zipWith tcEqTypeNoKindCheck args1 args2)
-- No kind check necessary: if both arguments are well typed, then
=====================================
compiler/GHC/Core/Unify.hs
=====================================
@@ -245,16 +245,21 @@ give up on), but for /substitutivity/. If we have (F x x), we can see that (F x
can reduce to Double. So, it had better be the case that (F blah blah) can
reduce to Double, no matter what (blah) is!
-To achieve this, `go_fam` in `uVarOrFam` does this;
+To achieve this, `go` in `uVarOrFam` does this;
+
+* We maintain /two/ substitutions, not just one:
+ * um_tv_env: the regular substitution, mapping TyVar :-> Type
+ * um_fam_env: maps (TyCon,[Type]) :-> Type, where the LHS is a type-fam application
+ In effect, these constitute one substitution mapping
+ CanEqLHS :-> Types
* When we attempt to unify (G Float) ~ Int, we return MaybeApart..
- but we /also/ extend a "family substitution" [G Float :-> Int],
- in `um_fam_env`, alongside the regular [tyvar :-> type] substitution in
- `um_tv_env`. See the `BindMe` case of `go_fam` in `uVarOrFam`.
+ but we /also/ add a "family substitution" [G Float :-> Int],
+ to `um_fam_env`. See the `BindMe` case of `go` in `uVarOrFam`.
* When we later encounter (G Float) ~ Bool, we apply the family substitution,
very much as we apply the conventional [tyvar :-> type] substitution
- when we encounter a type variable. See the `lookupFamEnv` in `go_fam` in
+ when we encounter a type variable. See the `lookupFamEnv` in `go` in
`uVarOrFam`.
So (G Float ~ Bool) becomes (Int ~ Bool) which is SurelyApart. Bingo.
@@ -329,7 +334,7 @@ Wrinkles
alternative path. So `noMatchableGivenDicts` must return False;
so `mightMatchLater` must return False; so when um_bind_fam_fun returns
`DontBindMe`, the unifier must return `SurelyApart`, not `MaybeApart`. See
- `go_fam` in `uVarOrFam`
+ `go` in `uVarOrFam`
(ATF6) When /matching/ can we ever have a type-family application on the LHS, in
the template? You might think not, because type-class-instance and
@@ -426,6 +431,9 @@ Wrinkles
(ATF12) There is a horrid exception for the injectivity check. See (UR1) in
in Note [Specification of unification].
+(ATF13) We have to be careful about the occurs check.
+ See Note [The occurs check in the Core unifier]
+
SIDE NOTE. The paper "Closed type families with overlapping equations"
http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/axioms-e…
tries to achieve the same effect with a standard yes/no unifier, by "flattening"
@@ -449,6 +457,49 @@ and all is lost. But with the current algorithm we have that
a a ~ (Var A) (Var B)
is SurelyApart, so the first equation definitely doesn't match and we can try the
second, which does. END OF SIDE NOTE.
+
+Note [Shortcomings of the apartness test]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Note [Apartness and type families] is very clever.
+
+But it still has shortcomings (#26358). Consider unifying
+ [F a, F Int, Int] ~ [Bool, Char, a]
+Working left to right you might think we would build the mapping
+ F a :-> Bool
+ F Int :-> Char
+Now we discover that `a` unifies with `Int`. So really these two lists are Apart
+because F Int can't be both Bool and Char.
+
+Just the same applies when adding a type-family binding to um_fam_env:
+ [F (G Float), F Int, G Float] ~ [Bool, Char, Iont]
+Again these are Apart, because (G Float = Int),
+and (F Int) can't be both Bool and Char
+
+But achieving this is very tricky! Perhaps whenever we unify a type variable,
+or a type family, we should run it over the domain and (maybe range) of the
+type-family mapping too? Sigh.
+
+For now we make no such attempt.
+* The um_fam_env has only /un-substituted/ types.
+* We look up only /un-substituted/ types in um_fam_env
+
+This may make us say MaybeApart when we could say SurelyApart, but it has no
+effect on the correctness of unification: if we return Unifiable, it really is
+Unifiable.
+
+This is all quite subtle. suppose we have:
+ um_tv_env: c :-> b
+ um_fam_env F b :-> a
+and we are trying to add a :-> F c. We will call lookupFamEnv on (F, [c]), which will
+fail because b and c are not equal. So we go ahead and add a :-> F c as a new tyvar eq,
+getting:
+ um_tv_env: a :-> F c, c :-> b
+ um_fam_env F b :-> a
+
+Does that loop, like this:
+ a --> F c --> F b --> a?
+No, because we do not substitute (F c) to (F b) and then look up in um_fam_env;
+we look up only un-substituted types.
-}
{- *********************************************************************
@@ -1767,6 +1818,11 @@ uVarOrFam :: UMEnv -> CanEqLHS -> InType -> OutCoercion -> UM ()
-- Why saturated? See (ATF4) in Note [Apartness and type families]
uVarOrFam env ty1 ty2 kco
= do { substs <- getSubstEnvs
+-- ; pprTrace "uVarOrFam" (vcat
+-- [ text "ty1" <+> ppr ty1
+-- , text "ty2" <+> ppr ty2
+-- , text "tv_env" <+> ppr (um_tv_env substs)
+-- , text "fam_env" <+> ppr (um_fam_env substs) ]) $
; go NotSwapped substs ty1 ty2 kco }
where
-- `go` takes two bites at the cherry; if the first one fails
@@ -1776,16 +1832,12 @@ uVarOrFam env ty1 ty2 kco
-- E.g. a ~ F p q
-- Starts with: go a (F p q)
-- if `a` not bindable, swap to: go (F p q) a
- go swapped substs (TyVarLHS tv1) ty2 kco
- = go_tv swapped substs tv1 ty2 kco
-
- go swapped substs (TyFamLHS tc tys) ty2 kco
- = go_fam swapped substs tc tys ty2 kco
-----------------------------
- -- go_tv: LHS is a type variable
+ -- LHS is a type variable
-- The sequence of tests is very similar to go_tv
- go_tv swapped substs tv1 ty2 kco
+ go :: SwapFlag -> UMState -> CanEqLHS -> InType -> OutCoercion -> UM ()
+ go swapped substs lhs@(TyVarLHS tv1) ty2 kco
| Just ty1' <- lookupVarEnv (um_tv_env substs) tv1'
= -- We already have a substitution for tv1
if | um_unif env -> unify_ty env ty1' ty2 kco
@@ -1837,9 +1889,8 @@ uVarOrFam env ty1 ty2 kco
where
tv1' = umRnOccL env tv1
ty2_fvs = tyCoVarsOfType ty2
- rhs_fvs = ty2_fvs `unionVarSet` tyCoVarsOfCo kco
rhs = ty2 `mkCastTy` mkSymCo kco
- tv1_is_bindable | not (tv1' `elemVarSet` um_foralls env)
+ tv1_is_bindable | not (tv1' `elemVarSet` foralld_tvs)
-- tv1' is not forall-bound, but tv1 can still differ
-- from tv1; see Note [Cloning the template binders]
-- in GHC.Core.Rules. So give tv1' to um_bind_tv_fun.
@@ -1848,16 +1899,16 @@ uVarOrFam env ty1 ty2 kco
| otherwise
= False
- occurs_check = um_unif env &&
- occursCheck (um_tv_env substs) tv1 rhs_fvs
+ foralld_tvs = um_foralls env
+ occurs_check = um_unif env && uOccursCheck substs foralld_tvs lhs rhs
-- Occurs check, only when unifying
-- see Note [Infinitary substitutions]
- -- Make sure you include `kco` in rhs_tvs #14846
+ -- Make sure you include `kco` in rhs #14846
-----------------------------
- -- go_fam: LHS is a saturated type-family application
+ -- LHS is a saturated type-family application
-- Invariant: ty2 is not a TyVarTy
- go_fam swapped substs tc1 tys1 ty2 kco
+ go swapped substs lhs@(TyFamLHS tc1 tys1) ty2 kco
-- If we are under a forall, just give up and return MaybeApart
-- see (ATF3) in Note [Apartness and type families]
| not (isEmptyVarSet (um_foralls env))
@@ -1878,14 +1929,17 @@ uVarOrFam env ty1 ty2 kco
-- Check for equality F tys1 ~ F tys2
| Just (tc2, tys2) <- isSatFamApp ty2
, tc1 == tc2
- = go_fam_fam tc1 tys1 tys2 kco
+ = go_fam_fam substs tc1 tys1 tys2 kco
-- Now check if we can bind the (F tys) to the RHS
-- This can happen even when matching: see (ATF7)
| BindMe <- um_bind_fam_fun env tc1 tys1 rhs
- = -- ToDo: do we need an occurs check here?
- do { extendFamEnv tc1 tys1 rhs
- ; maybeApart MARTypeFamily }
+ = if uOccursCheck substs emptyVarSet lhs rhs
+ then maybeApart MARInfinite
+ else do { extendFamEnv tc1 tys1 rhs
+ -- We don't substitute tys1 before extending
+ -- See Note [Shortcomings of the apartness test]
+ ; maybeApart MARTypeFamily }
-- Swap in case of (F a b) ~ (G c d e)
-- Maybe um_bind_fam_fun is False of (F a b) but true of (G c d e)
@@ -1905,7 +1959,8 @@ uVarOrFam env ty1 ty2 kco
-----------------------------
-- go_fam_fam: LHS and RHS are both saturated type-family applications,
-- for the same type-family F
- go_fam_fam tc tys1 tys2 kco
+ -- Precondition: um_foralls is empty
+ go_fam_fam substs tc tys1 tys2 kco
-- Decompose (F tys1 ~ F tys2): (ATF9)
-- Use injectivity information of F: (ATF10)
-- But first bind the type-fam if poss: (ATF11)
@@ -1925,13 +1980,13 @@ uVarOrFam env ty1 ty2 kco
bind_fam_if_poss
| not (um_unif env) -- Not when matching (ATF11-1)
= return ()
- | tcEqTyConAppArgs tys1 tys2 -- Detect (F tys ~ F tys);
- = return () -- otherwise we'd build an infinite substitution
| BindMe <- um_bind_fam_fun env tc tys1 rhs1
- = extendFamEnv tc tys1 rhs1
- | um_unif env
- , BindMe <- um_bind_fam_fun env tc tys2 rhs2
- = extendFamEnv tc tys2 rhs2
+ = unless (uOccursCheck substs emptyVarSet (TyFamLHS tc tys1) rhs1) $
+ extendFamEnv tc tys1 rhs1
+ -- At this point um_unif=True, so we can unify either way
+ | BindMe <- um_bind_fam_fun env tc tys2 rhs2
+ = unless (uOccursCheck substs emptyVarSet (TyFamLHS tc tys2) rhs2) $
+ extendFamEnv tc tys2 rhs2
| otherwise
= return ()
@@ -1939,17 +1994,92 @@ uVarOrFam env ty1 ty2 kco
rhs2 = mkTyConApp tc tys1 `mkCastTy` kco
-occursCheck :: TvSubstEnv -> TyVar -> TyCoVarSet -> Bool
-occursCheck env tv1 tvs
- = anyVarSet bad tvs
+uOccursCheck :: UMState
+ -> TyVarSet -- Bound by enclosing foralls; see (OCU1)
+ -> CanEqLHS -> Type -- Can we unify (lhs := ty)?
+ -> Bool
+-- See Note [The occurs check in the Core unifier] and (ATF13)
+uOccursCheck (UMState { um_tv_env = tv_env, um_fam_env = fam_env }) bvs lhs ty
+ = go bvs ty
where
- bad tv | Just ty <- lookupVarEnv env tv
- = anyVarSet bad (tyCoVarsOfType ty)
- | otherwise
- = tv == tv1
-
-{- Note [Unifying coercion-foralls]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+ go :: TyCoVarSet -- Bound by enclosing foralls; see (OCU1)
+ -> Type -> Bool
+ go bvs ty | Just ty' <- coreView ty = go bvs ty'
+ go bvs (TyVarTy tv) | Just ty' <- lookupVarEnv tv_env tv
+ = go bvs ty'
+ | TyVarLHS tv' <- lhs, tv==tv'
+ = True
+ | otherwise
+ = go bvs (tyVarKind tv)
+ go bvs (AppTy ty1 ty2) = go bvs ty1 || go bvs ty2
+ go _ (LitTy {}) = False
+ go bvs (FunTy _ w arg res) = go bvs w || go bvs arg || go bvs res
+ go bvs (TyConApp tc tys) = go_tc bvs tc tys
+
+ go bvs (ForAllTy (Bndr tv _) ty)
+ = go bvs (tyVarKind tv) ||
+ (case lhs of
+ TyVarLHS tv' | tv==tv' -> False -- Shadowing
+ | otherwise -> go (bvs `extendVarSet` tv) ty
+ TyFamLHS {} -> False) -- Lookups don't happen under a forall
+
+ go bvs (CastTy ty _co) = go bvs ty -- ToDo: should we worry about `co`?
+ go _ (CoercionTy _co) = False -- ToDo: should we worry about `co`?
+
+ go_tc bvs tc tys
+ | isEmptyVarSet bvs -- Never look up in um_fam_env under a forall (ATF3)
+ , isTypeFamilyTyCon tc
+ , Just ty' <- lookupFamEnv fam_env tc (take arity tys)
+ -- NB: we look up /un-substituted/ types;
+ -- See Note [Shortcomings of the apartness test]
+ = go bvs ty' || any (go bvs) (drop arity tys)
+
+ | TyFamLHS tc' tys' <- lhs
+ , tc == tc'
+ , tys `lengthAtLeast` arity -- Saturated, or over-saturated
+ , tcEqTyConAppArgs tys tys'
+ = True
+
+ | otherwise
+ = any (go bvs) tys
+ where
+ arity = tyConArity tc
+
+{- Note [The occurs check in the Core unifier]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The unifier applies both substitutions (um_tv_env and um_fam_env) as it goes,
+so we'll get an infinite loop if we have, for example
+ um_tv_env: a :-> F b -- (1)
+ um_fam_env F b :-> a -- (2)
+
+So (uOccursCheck substs lhs ty) returns True iff extending `substs` with `lhs :-> ty`
+could lead to a loop. That is, could there by a type `s` such that
+ applySubsts( (substs + lhs:->ty), s ) is infinite
+
+It's vital that we do both at once: we might have (1) already and add (2);
+or we might have (2) already and add (1).
+
+A very similar task is done by GHC.Tc.Utils.Unify.checkTyEqRhs.
+
+(OCU1) We keep track of the forall-bound variables because the um_fam_env is inactive
+ under a forall; indeed it is /unsound/ to consult it because we may have a binding
+ (F a :-> Int), and then unify (forall a. ...(F a)...) with something. We don't
+ want to map that (F a) to Int!
+
+(OCU2) Performance. Consider unifying
+ [a, b] ~ [big-ty, (a,a,a)]
+ We'll unify a:=big-ty. Then we'll attempt b:=(a,a,a), but must do an occurs check.
+ So we'll walk over big-ty, looking for `b`. And then again, and again, once for
+ each occurrence of `a`. A similar thing happens for
+ [a, (b,b,b)] ~ [big-ty, (a,a,a)]
+ albeit a bit less obviously.
+
+ Potentially we could use a cache to record checks we have already done;
+ but I have not attempted that yet. Precisely similar remarks would apply
+ to GHC.Tc.Utils.Unify.checkTyEqRhs
+
+Note [Unifying coercion-foralls]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we try to unify (forall cv. t1) ~ (forall cv. t2).
See Note [ForAllTy] in GHC.Core.TyCo.Rep.
=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -3342,8 +3342,9 @@ mapCheck f xs
-- | Options describing how to deal with a type equality
-- in the eager unifier. See 'checkTyEqRhs'
data TyEqFlags m a
- -- | LHS is a type family application; we are not unifying.
- = TEFTyFam
+ = -- | TFTyFam: LHS is a type family application
+ -- Invariant: we are not unifying; see `notUnifying_TEFTask`
+ TEFTyFam
{ tefTyFam_occursCheck :: CheckTyEqProblem
-- ^ The 'CheckTyEqProblem' to report for occurs-check failures
-- (soluble or insoluble)
@@ -3352,7 +3353,8 @@ data TyEqFlags m a
, tef_fam_app :: TyEqFamApp m a
-- ^ How to deal with type family applications
}
- -- | LHS is a 'TyVar'.
+
+ -- | TEFTyVar: LHS is a 'TyVar'.
| TEFTyVar
-- NB: this constructor does not actually store a 'TyVar', in order to
-- support being called from 'makeTypeConcrete' (which works as if we
=====================================
testsuite/tests/typecheck/should_compile/T26346.hs
=====================================
@@ -0,0 +1,103 @@
+{-# LANGUAGE GHC2024 #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+module T26346 (warble) where
+
+import Data.Kind (Type)
+import Data.Type.Equality ((:~:)(..))
+
+type Nat :: Type
+data Nat = Z | S Nat
+
+type SNat :: Nat -> Type
+data SNat n where
+ SZ :: SNat Z
+ SS :: SNat n -> SNat (S n)
+
+type NatPlus :: Nat -> Nat -> Nat
+type family NatPlus a b where
+ NatPlus Z b = b
+ NatPlus (S a) b = S (NatPlus a b)
+
+sNatPlus ::
+ forall (a :: Nat) (b :: Nat).
+ SNat a ->
+ SNat b ->
+ SNat (NatPlus a b)
+sNatPlus SZ b = b
+sNatPlus (SS a) b = SS (sNatPlus a b)
+
+data Bin
+ = Zero
+ | Even Bin
+ | Odd Bin
+
+type SBin :: Bin -> Type
+data SBin b where
+ SZero :: SBin Zero
+ SEven :: SBin n -> SBin (Even n)
+ SOdd :: SBin n -> SBin (Odd n)
+
+type Incr :: Bin -> Bin
+type family Incr b where
+ Incr Zero = Odd Zero -- 0 + 1 = (2*0) + 1
+ Incr (Even n) = Odd n -- 2n + 1
+ Incr (Odd n) = Even (Incr n) -- (2n + 1) + 1 = 2*(n + 1)
+
+type BinToNat :: Bin -> Nat
+type family BinToNat b where
+ BinToNat Zero = Z
+ BinToNat (Even n) = NatPlus (BinToNat n) (BinToNat n)
+ BinToNat (Odd n) = S (NatPlus (BinToNat n) (BinToNat n))
+
+sBinToNat ::
+ forall (b :: Bin).
+ SBin b ->
+ SNat (BinToNat b)
+sBinToNat SZero = SZ
+sBinToNat (SEven n) = sNatPlus (sBinToNat n) (sBinToNat n)
+sBinToNat (SOdd n) = SS (sNatPlus (sBinToNat n) (sBinToNat n))
+
+warble ::
+ forall (b :: Bin).
+ SBin b ->
+ BinToNat (Incr b) :~: S (BinToNat b)
+warble SZero = Refl
+warble (SEven {}) = Refl
+warble (SOdd sb) | Refl <- warble sb
+ , Refl <- plusComm sbn (SS sbn)
+ = Refl
+ where
+ sbn = sBinToNat sb
+
+ plus0R ::
+ forall (n :: Nat).
+ SNat n ->
+ NatPlus n Z :~: n
+ plus0R SZ = Refl
+ plus0R (SS sn)
+ | Refl <- plus0R sn
+ = Refl
+
+ plusSnR ::
+ forall (n :: Nat) (m :: Nat).
+ SNat n ->
+ SNat m ->
+ NatPlus n (S m) :~: S (NatPlus n m)
+ plusSnR SZ _ = Refl
+ plusSnR (SS sn) sm
+ | Refl <- plusSnR sn sm
+ = Refl
+
+ plusComm ::
+ forall (n :: Nat) (m :: Nat).
+ SNat n ->
+ SNat m ->
+ NatPlus n m :~: NatPlus m n
+ plusComm SZ sm
+ | Refl <- plus0R sm
+ = Refl
+ plusComm (SS sn) sm
+ | Refl <- plusComm sn sm
+ , Refl <- plusSnR sm sn
+ = Refl
=====================================
testsuite/tests/typecheck/should_compile/T26358.hs
=====================================
@@ -0,0 +1,48 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module T26358 where
+import Data.Kind
+import Data.Proxy
+
+{- Two failing tests, described in GHC.Core.Unify
+ Note [Shortcomings of the apartness test]
+
+Explanation for TF2
+* We try to reduce
+ (TF2 (F (G Float)) (F Int) (G Float))
+* We can only do so if those arguments are apart from the first
+ equation of TF2, namely (Bool,Char,Int).
+* So we try to unify
+ [F (G Float), F Int, G Float] ~ [Bool, Char, Int]
+* They really are apart, but we can't quite spot that yet;
+ hence #26358
+
+TF1 is similar.
+-}
+
+
+type TF1 :: Type -> Type -> Type -> Type
+type family TF1 a b c where
+ TF1 Bool Char a = Word
+ TF1 a b c = (a,b,c)
+
+type F :: Type -> Type
+type family F a where
+
+foo :: Proxy a
+ -> Proxy (TF1 (F a) (F Int) Int)
+ -> Proxy (F a, F Int, Int)
+foo _ px = px
+
+type TF2 :: Type -> Type -> Type -> Type
+type family TF2 a b c where
+ TF2 Bool Char Int = Word
+ TF2 a b c = (a,b,c)
+
+type G :: Type -> Type
+type family G a where
+
+bar :: Proxy (TF2 (F (G Float)) (F Int) (G Float))
+ -> Proxy (F (G Float), F Int, G Float)
+bar px = px
+
=====================================
testsuite/tests/typecheck/should_compile/all.T
=====================================
@@ -945,3 +945,5 @@ test('T25992', normal, compile, [''])
test('T14010', normal, compile, [''])
test('T26256a', normal, compile, [''])
test('T25992a', normal, compile, [''])
+test('T26346', normal, compile, [''])
+test('T26358', expect_broken(26358), compile, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/ae89f0006cb0221e54a6bcecfb1542…
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/ae89f0006cb0221e54a6bcecfb1542…
You're receiving this email because of your account on gitlab.haskell.org.
1
0
[Git][ghc/ghc][wip/marge_bot_batch_merge_job] 3 commits: Comments only
by Marge Bot (＠marge-bot) 28 Aug '25
by Marge Bot (＠marge-bot) 28 Aug '25
28 Aug '25
Marge Bot pushed to branch wip/marge_bot_batch_merge_job at Glasgow Haskell Compiler / GHC
Commits:
00478944 by Simon Peyton Jones at 2025-08-27T16:48:30+01:00
Comments only
- - - - -
a7884589 by Simon Peyton Jones at 2025-08-28T11:08:23+01:00
Type-family occurs check in unification
The occurs check in `GHC.Core.Unify.uVarOrFam` was inadequate in dealing
with type families.
Better now. See Note [The occurs check in the Core unifier].
As I did this I realised that the whole apartness thing is trickier than I
thought: see the new Note [Shortcomings of the apartness test]
- - - - -
dbbb3c39 by sheaf at 2025-08-28T13:56:02-04:00
Fix orientation in HsWrapper composition (<.>)
This commit fixes the order in which WpCast HsWrappers are composed,
fixing a bug introduced in commit 56b32c5a2d5d7cad89a12f4d74dc940e086069d1.
Fixes #26350
- - - - -
9 changed files:
- compiler/GHC/Core/TyCo/Compare.hs
- compiler/GHC/Core/Unify.hs
- compiler/GHC/Tc/Gen/App.hs
- compiler/GHC/Tc/Types/Evidence.hs
- compiler/GHC/Tc/Utils/Unify.hs
- + testsuite/tests/typecheck/should_compile/T26346.hs
- + testsuite/tests/typecheck/should_compile/T26350.hs
- + testsuite/tests/typecheck/should_compile/T26358.hs
- testsuite/tests/typecheck/should_compile/all.T
Changes:
=====================================
compiler/GHC/Core/TyCo/Compare.hs
=====================================
@@ -229,6 +229,8 @@ tcEqTyConApps tc1 args1 tc2 args2
= tc1 == tc2 && tcEqTyConAppArgs args1 args2
tcEqTyConAppArgs :: [Type] -> [Type] -> Bool
+-- Args do not have to have equal length;
+-- we discard the excess of the longer one
tcEqTyConAppArgs args1 args2
= and (zipWith tcEqTypeNoKindCheck args1 args2)
-- No kind check necessary: if both arguments are well typed, then
=====================================
compiler/GHC/Core/Unify.hs
=====================================
@@ -245,16 +245,21 @@ give up on), but for /substitutivity/. If we have (F x x), we can see that (F x
can reduce to Double. So, it had better be the case that (F blah blah) can
reduce to Double, no matter what (blah) is!
-To achieve this, `go_fam` in `uVarOrFam` does this;
+To achieve this, `go` in `uVarOrFam` does this;
+
+* We maintain /two/ substitutions, not just one:
+ * um_tv_env: the regular substitution, mapping TyVar :-> Type
+ * um_fam_env: maps (TyCon,[Type]) :-> Type, where the LHS is a type-fam application
+ In effect, these constitute one substitution mapping
+ CanEqLHS :-> Types
* When we attempt to unify (G Float) ~ Int, we return MaybeApart..
- but we /also/ extend a "family substitution" [G Float :-> Int],
- in `um_fam_env`, alongside the regular [tyvar :-> type] substitution in
- `um_tv_env`. See the `BindMe` case of `go_fam` in `uVarOrFam`.
+ but we /also/ add a "family substitution" [G Float :-> Int],
+ to `um_fam_env`. See the `BindMe` case of `go` in `uVarOrFam`.
* When we later encounter (G Float) ~ Bool, we apply the family substitution,
very much as we apply the conventional [tyvar :-> type] substitution
- when we encounter a type variable. See the `lookupFamEnv` in `go_fam` in
+ when we encounter a type variable. See the `lookupFamEnv` in `go` in
`uVarOrFam`.
So (G Float ~ Bool) becomes (Int ~ Bool) which is SurelyApart. Bingo.
@@ -329,7 +334,7 @@ Wrinkles
alternative path. So `noMatchableGivenDicts` must return False;
so `mightMatchLater` must return False; so when um_bind_fam_fun returns
`DontBindMe`, the unifier must return `SurelyApart`, not `MaybeApart`. See
- `go_fam` in `uVarOrFam`
+ `go` in `uVarOrFam`
(ATF6) When /matching/ can we ever have a type-family application on the LHS, in
the template? You might think not, because type-class-instance and
@@ -426,6 +431,9 @@ Wrinkles
(ATF12) There is a horrid exception for the injectivity check. See (UR1) in
in Note [Specification of unification].
+(ATF13) We have to be careful about the occurs check.
+ See Note [The occurs check in the Core unifier]
+
SIDE NOTE. The paper "Closed type families with overlapping equations"
http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/axioms-e…
tries to achieve the same effect with a standard yes/no unifier, by "flattening"
@@ -449,6 +457,49 @@ and all is lost. But with the current algorithm we have that
a a ~ (Var A) (Var B)
is SurelyApart, so the first equation definitely doesn't match and we can try the
second, which does. END OF SIDE NOTE.
+
+Note [Shortcomings of the apartness test]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Note [Apartness and type families] is very clever.
+
+But it still has shortcomings (#26358). Consider unifying
+ [F a, F Int, Int] ~ [Bool, Char, a]
+Working left to right you might think we would build the mapping
+ F a :-> Bool
+ F Int :-> Char
+Now we discover that `a` unifies with `Int`. So really these two lists are Apart
+because F Int can't be both Bool and Char.
+
+Just the same applies when adding a type-family binding to um_fam_env:
+ [F (G Float), F Int, G Float] ~ [Bool, Char, Iont]
+Again these are Apart, because (G Float = Int),
+and (F Int) can't be both Bool and Char
+
+But achieving this is very tricky! Perhaps whenever we unify a type variable,
+or a type family, we should run it over the domain and (maybe range) of the
+type-family mapping too? Sigh.
+
+For now we make no such attempt.
+* The um_fam_env has only /un-substituted/ types.
+* We look up only /un-substituted/ types in um_fam_env
+
+This may make us say MaybeApart when we could say SurelyApart, but it has no
+effect on the correctness of unification: if we return Unifiable, it really is
+Unifiable.
+
+This is all quite subtle. suppose we have:
+ um_tv_env: c :-> b
+ um_fam_env F b :-> a
+and we are trying to add a :-> F c. We will call lookupFamEnv on (F, [c]), which will
+fail because b and c are not equal. So we go ahead and add a :-> F c as a new tyvar eq,
+getting:
+ um_tv_env: a :-> F c, c :-> b
+ um_fam_env F b :-> a
+
+Does that loop, like this:
+ a --> F c --> F b --> a?
+No, because we do not substitute (F c) to (F b) and then look up in um_fam_env;
+we look up only un-substituted types.
-}
{- *********************************************************************
@@ -1767,6 +1818,11 @@ uVarOrFam :: UMEnv -> CanEqLHS -> InType -> OutCoercion -> UM ()
-- Why saturated? See (ATF4) in Note [Apartness and type families]
uVarOrFam env ty1 ty2 kco
= do { substs <- getSubstEnvs
+-- ; pprTrace "uVarOrFam" (vcat
+-- [ text "ty1" <+> ppr ty1
+-- , text "ty2" <+> ppr ty2
+-- , text "tv_env" <+> ppr (um_tv_env substs)
+-- , text "fam_env" <+> ppr (um_fam_env substs) ]) $
; go NotSwapped substs ty1 ty2 kco }
where
-- `go` takes two bites at the cherry; if the first one fails
@@ -1776,16 +1832,12 @@ uVarOrFam env ty1 ty2 kco
-- E.g. a ~ F p q
-- Starts with: go a (F p q)
-- if `a` not bindable, swap to: go (F p q) a
- go swapped substs (TyVarLHS tv1) ty2 kco
- = go_tv swapped substs tv1 ty2 kco
-
- go swapped substs (TyFamLHS tc tys) ty2 kco
- = go_fam swapped substs tc tys ty2 kco
-----------------------------
- -- go_tv: LHS is a type variable
+ -- LHS is a type variable
-- The sequence of tests is very similar to go_tv
- go_tv swapped substs tv1 ty2 kco
+ go :: SwapFlag -> UMState -> CanEqLHS -> InType -> OutCoercion -> UM ()
+ go swapped substs lhs@(TyVarLHS tv1) ty2 kco
| Just ty1' <- lookupVarEnv (um_tv_env substs) tv1'
= -- We already have a substitution for tv1
if | um_unif env -> unify_ty env ty1' ty2 kco
@@ -1837,9 +1889,8 @@ uVarOrFam env ty1 ty2 kco
where
tv1' = umRnOccL env tv1
ty2_fvs = tyCoVarsOfType ty2
- rhs_fvs = ty2_fvs `unionVarSet` tyCoVarsOfCo kco
rhs = ty2 `mkCastTy` mkSymCo kco
- tv1_is_bindable | not (tv1' `elemVarSet` um_foralls env)
+ tv1_is_bindable | not (tv1' `elemVarSet` foralld_tvs)
-- tv1' is not forall-bound, but tv1 can still differ
-- from tv1; see Note [Cloning the template binders]
-- in GHC.Core.Rules. So give tv1' to um_bind_tv_fun.
@@ -1848,16 +1899,16 @@ uVarOrFam env ty1 ty2 kco
| otherwise
= False
- occurs_check = um_unif env &&
- occursCheck (um_tv_env substs) tv1 rhs_fvs
+ foralld_tvs = um_foralls env
+ occurs_check = um_unif env && uOccursCheck substs foralld_tvs lhs rhs
-- Occurs check, only when unifying
-- see Note [Infinitary substitutions]
- -- Make sure you include `kco` in rhs_tvs #14846
+ -- Make sure you include `kco` in rhs #14846
-----------------------------
- -- go_fam: LHS is a saturated type-family application
+ -- LHS is a saturated type-family application
-- Invariant: ty2 is not a TyVarTy
- go_fam swapped substs tc1 tys1 ty2 kco
+ go swapped substs lhs@(TyFamLHS tc1 tys1) ty2 kco
-- If we are under a forall, just give up and return MaybeApart
-- see (ATF3) in Note [Apartness and type families]
| not (isEmptyVarSet (um_foralls env))
@@ -1878,14 +1929,17 @@ uVarOrFam env ty1 ty2 kco
-- Check for equality F tys1 ~ F tys2
| Just (tc2, tys2) <- isSatFamApp ty2
, tc1 == tc2
- = go_fam_fam tc1 tys1 tys2 kco
+ = go_fam_fam substs tc1 tys1 tys2 kco
-- Now check if we can bind the (F tys) to the RHS
-- This can happen even when matching: see (ATF7)
| BindMe <- um_bind_fam_fun env tc1 tys1 rhs
- = -- ToDo: do we need an occurs check here?
- do { extendFamEnv tc1 tys1 rhs
- ; maybeApart MARTypeFamily }
+ = if uOccursCheck substs emptyVarSet lhs rhs
+ then maybeApart MARInfinite
+ else do { extendFamEnv tc1 tys1 rhs
+ -- We don't substitute tys1 before extending
+ -- See Note [Shortcomings of the apartness test]
+ ; maybeApart MARTypeFamily }
-- Swap in case of (F a b) ~ (G c d e)
-- Maybe um_bind_fam_fun is False of (F a b) but true of (G c d e)
@@ -1905,7 +1959,8 @@ uVarOrFam env ty1 ty2 kco
-----------------------------
-- go_fam_fam: LHS and RHS are both saturated type-family applications,
-- for the same type-family F
- go_fam_fam tc tys1 tys2 kco
+ -- Precondition: um_foralls is empty
+ go_fam_fam substs tc tys1 tys2 kco
-- Decompose (F tys1 ~ F tys2): (ATF9)
-- Use injectivity information of F: (ATF10)
-- But first bind the type-fam if poss: (ATF11)
@@ -1925,13 +1980,13 @@ uVarOrFam env ty1 ty2 kco
bind_fam_if_poss
| not (um_unif env) -- Not when matching (ATF11-1)
= return ()
- | tcEqTyConAppArgs tys1 tys2 -- Detect (F tys ~ F tys);
- = return () -- otherwise we'd build an infinite substitution
| BindMe <- um_bind_fam_fun env tc tys1 rhs1
- = extendFamEnv tc tys1 rhs1
- | um_unif env
- , BindMe <- um_bind_fam_fun env tc tys2 rhs2
- = extendFamEnv tc tys2 rhs2
+ = unless (uOccursCheck substs emptyVarSet (TyFamLHS tc tys1) rhs1) $
+ extendFamEnv tc tys1 rhs1
+ -- At this point um_unif=True, so we can unify either way
+ | BindMe <- um_bind_fam_fun env tc tys2 rhs2
+ = unless (uOccursCheck substs emptyVarSet (TyFamLHS tc tys2) rhs2) $
+ extendFamEnv tc tys2 rhs2
| otherwise
= return ()
@@ -1939,17 +1994,92 @@ uVarOrFam env ty1 ty2 kco
rhs2 = mkTyConApp tc tys1 `mkCastTy` kco
-occursCheck :: TvSubstEnv -> TyVar -> TyCoVarSet -> Bool
-occursCheck env tv1 tvs
- = anyVarSet bad tvs
+uOccursCheck :: UMState
+ -> TyVarSet -- Bound by enclosing foralls; see (OCU1)
+ -> CanEqLHS -> Type -- Can we unify (lhs := ty)?
+ -> Bool
+-- See Note [The occurs check in the Core unifier] and (ATF13)
+uOccursCheck (UMState { um_tv_env = tv_env, um_fam_env = fam_env }) bvs lhs ty
+ = go bvs ty
where
- bad tv | Just ty <- lookupVarEnv env tv
- = anyVarSet bad (tyCoVarsOfType ty)
- | otherwise
- = tv == tv1
-
-{- Note [Unifying coercion-foralls]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+ go :: TyCoVarSet -- Bound by enclosing foralls; see (OCU1)
+ -> Type -> Bool
+ go bvs ty | Just ty' <- coreView ty = go bvs ty'
+ go bvs (TyVarTy tv) | Just ty' <- lookupVarEnv tv_env tv
+ = go bvs ty'
+ | TyVarLHS tv' <- lhs, tv==tv'
+ = True
+ | otherwise
+ = go bvs (tyVarKind tv)
+ go bvs (AppTy ty1 ty2) = go bvs ty1 || go bvs ty2
+ go _ (LitTy {}) = False
+ go bvs (FunTy _ w arg res) = go bvs w || go bvs arg || go bvs res
+ go bvs (TyConApp tc tys) = go_tc bvs tc tys
+
+ go bvs (ForAllTy (Bndr tv _) ty)
+ = go bvs (tyVarKind tv) ||
+ (case lhs of
+ TyVarLHS tv' | tv==tv' -> False -- Shadowing
+ | otherwise -> go (bvs `extendVarSet` tv) ty
+ TyFamLHS {} -> False) -- Lookups don't happen under a forall
+
+ go bvs (CastTy ty _co) = go bvs ty -- ToDo: should we worry about `co`?
+ go _ (CoercionTy _co) = False -- ToDo: should we worry about `co`?
+
+ go_tc bvs tc tys
+ | isEmptyVarSet bvs -- Never look up in um_fam_env under a forall (ATF3)
+ , isTypeFamilyTyCon tc
+ , Just ty' <- lookupFamEnv fam_env tc (take arity tys)
+ -- NB: we look up /un-substituted/ types;
+ -- See Note [Shortcomings of the apartness test]
+ = go bvs ty' || any (go bvs) (drop arity tys)
+
+ | TyFamLHS tc' tys' <- lhs
+ , tc == tc'
+ , tys `lengthAtLeast` arity -- Saturated, or over-saturated
+ , tcEqTyConAppArgs tys tys'
+ = True
+
+ | otherwise
+ = any (go bvs) tys
+ where
+ arity = tyConArity tc
+
+{- Note [The occurs check in the Core unifier]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The unifier applies both substitutions (um_tv_env and um_fam_env) as it goes,
+so we'll get an infinite loop if we have, for example
+ um_tv_env: a :-> F b -- (1)
+ um_fam_env F b :-> a -- (2)
+
+So (uOccursCheck substs lhs ty) returns True iff extending `substs` with `lhs :-> ty`
+could lead to a loop. That is, could there by a type `s` such that
+ applySubsts( (substs + lhs:->ty), s ) is infinite
+
+It's vital that we do both at once: we might have (1) already and add (2);
+or we might have (2) already and add (1).
+
+A very similar task is done by GHC.Tc.Utils.Unify.checkTyEqRhs.
+
+(OCU1) We keep track of the forall-bound variables because the um_fam_env is inactive
+ under a forall; indeed it is /unsound/ to consult it because we may have a binding
+ (F a :-> Int), and then unify (forall a. ...(F a)...) with something. We don't
+ want to map that (F a) to Int!
+
+(OCU2) Performance. Consider unifying
+ [a, b] ~ [big-ty, (a,a,a)]
+ We'll unify a:=big-ty. Then we'll attempt b:=(a,a,a), but must do an occurs check.
+ So we'll walk over big-ty, looking for `b`. And then again, and again, once for
+ each occurrence of `a`. A similar thing happens for
+ [a, (b,b,b)] ~ [big-ty, (a,a,a)]
+ albeit a bit less obviously.
+
+ Potentially we could use a cache to record checks we have already done;
+ but I have not attempted that yet. Precisely similar remarks would apply
+ to GHC.Tc.Utils.Unify.checkTyEqRhs
+
+Note [Unifying coercion-foralls]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we try to unify (forall cv. t1) ~ (forall cv. t2).
See Note [ForAllTy] in GHC.Core.TyCo.Rep.
=====================================
compiler/GHC/Tc/Gen/App.hs
=====================================
@@ -430,7 +430,7 @@ tcApp rn_expr exp_res_ty
-- Step 5.2: typecheck the arguments, and monomorphise
-- any un-unified instantiation variables
; tc_args <- tcValArgs DoQL inst_args
- -- Step 5.3: zonk to expose the polymophism hidden under
+ -- Step 5.3: zonk to expose the polymorphism hidden under
-- QuickLook instantiation variables in `app_res_rho`
; app_res_rho <- liftZonkM $ zonkTcType app_res_rho
-- Step 5.4: subsumption check against the expected type
=====================================
compiler/GHC/Tc/Types/Evidence.hs
=====================================
@@ -206,9 +206,15 @@ instance Monoid HsWrapper where
(<.>) :: HsWrapper -> HsWrapper -> HsWrapper
WpHole <.> c = c
c <.> WpHole = c
-WpCast c1 <.> WpCast c2 = WpCast (c1 `mkTransCo` c2)
+WpCast c1 <.> WpCast c2 = WpCast (c2 `mkTransCo` c1)
-- If we can represent the HsWrapper as a cast, try to do so: this may avoid
-- unnecessary eta-expansion (see 'mkWpFun').
+ --
+ -- NB: <.> behaves like function composition:
+ --
+ -- WpCast c1 <.> WpCast c2 :: coercionLKind c2 ~> coercionRKind c1
+ --
+ -- This is thus the same as WpCast (c2 ; c1) and not WpCast (c1 ; c2).
c1 <.> c2 = c1 `WpCompose` c2
-- | Smart constructor to create a 'WpFun' 'HsWrapper', which avoids introducing
=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -3342,8 +3342,9 @@ mapCheck f xs
-- | Options describing how to deal with a type equality
-- in the eager unifier. See 'checkTyEqRhs'
data TyEqFlags m a
- -- | LHS is a type family application; we are not unifying.
- = TEFTyFam
+ = -- | TFTyFam: LHS is a type family application
+ -- Invariant: we are not unifying; see `notUnifying_TEFTask`
+ TEFTyFam
{ tefTyFam_occursCheck :: CheckTyEqProblem
-- ^ The 'CheckTyEqProblem' to report for occurs-check failures
-- (soluble or insoluble)
@@ -3352,7 +3353,8 @@ data TyEqFlags m a
, tef_fam_app :: TyEqFamApp m a
-- ^ How to deal with type family applications
}
- -- | LHS is a 'TyVar'.
+
+ -- | TEFTyVar: LHS is a 'TyVar'.
| TEFTyVar
-- NB: this constructor does not actually store a 'TyVar', in order to
-- support being called from 'makeTypeConcrete' (which works as if we
=====================================
testsuite/tests/typecheck/should_compile/T26346.hs
=====================================
@@ -0,0 +1,103 @@
+{-# LANGUAGE GHC2024 #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+module T26346 (warble) where
+
+import Data.Kind (Type)
+import Data.Type.Equality ((:~:)(..))
+
+type Nat :: Type
+data Nat = Z | S Nat
+
+type SNat :: Nat -> Type
+data SNat n where
+ SZ :: SNat Z
+ SS :: SNat n -> SNat (S n)
+
+type NatPlus :: Nat -> Nat -> Nat
+type family NatPlus a b where
+ NatPlus Z b = b
+ NatPlus (S a) b = S (NatPlus a b)
+
+sNatPlus ::
+ forall (a :: Nat) (b :: Nat).
+ SNat a ->
+ SNat b ->
+ SNat (NatPlus a b)
+sNatPlus SZ b = b
+sNatPlus (SS a) b = SS (sNatPlus a b)
+
+data Bin
+ = Zero
+ | Even Bin
+ | Odd Bin
+
+type SBin :: Bin -> Type
+data SBin b where
+ SZero :: SBin Zero
+ SEven :: SBin n -> SBin (Even n)
+ SOdd :: SBin n -> SBin (Odd n)
+
+type Incr :: Bin -> Bin
+type family Incr b where
+ Incr Zero = Odd Zero -- 0 + 1 = (2*0) + 1
+ Incr (Even n) = Odd n -- 2n + 1
+ Incr (Odd n) = Even (Incr n) -- (2n + 1) + 1 = 2*(n + 1)
+
+type BinToNat :: Bin -> Nat
+type family BinToNat b where
+ BinToNat Zero = Z
+ BinToNat (Even n) = NatPlus (BinToNat n) (BinToNat n)
+ BinToNat (Odd n) = S (NatPlus (BinToNat n) (BinToNat n))
+
+sBinToNat ::
+ forall (b :: Bin).
+ SBin b ->
+ SNat (BinToNat b)
+sBinToNat SZero = SZ
+sBinToNat (SEven n) = sNatPlus (sBinToNat n) (sBinToNat n)
+sBinToNat (SOdd n) = SS (sNatPlus (sBinToNat n) (sBinToNat n))
+
+warble ::
+ forall (b :: Bin).
+ SBin b ->
+ BinToNat (Incr b) :~: S (BinToNat b)
+warble SZero = Refl
+warble (SEven {}) = Refl
+warble (SOdd sb) | Refl <- warble sb
+ , Refl <- plusComm sbn (SS sbn)
+ = Refl
+ where
+ sbn = sBinToNat sb
+
+ plus0R ::
+ forall (n :: Nat).
+ SNat n ->
+ NatPlus n Z :~: n
+ plus0R SZ = Refl
+ plus0R (SS sn)
+ | Refl <- plus0R sn
+ = Refl
+
+ plusSnR ::
+ forall (n :: Nat) (m :: Nat).
+ SNat n ->
+ SNat m ->
+ NatPlus n (S m) :~: S (NatPlus n m)
+ plusSnR SZ _ = Refl
+ plusSnR (SS sn) sm
+ | Refl <- plusSnR sn sm
+ = Refl
+
+ plusComm ::
+ forall (n :: Nat) (m :: Nat).
+ SNat n ->
+ SNat m ->
+ NatPlus n m :~: NatPlus m n
+ plusComm SZ sm
+ | Refl <- plus0R sm
+ = Refl
+ plusComm (SS sn) sm
+ | Refl <- plusComm sn sm
+ , Refl <- plusSnR sm sn
+ = Refl
=====================================
testsuite/tests/typecheck/should_compile/T26350.hs
=====================================
@@ -0,0 +1,18 @@
+{-# LANGUAGE DeepSubsumption #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+
+{-# OPTIONS_GHC -dcore-lint #-}
+
+module T26350 where
+
+import Control.Arrow (first)
+
+infix 6 .-.
+
+class AffineSpace p where
+ type Diff p
+ (.-.) :: p -> p -> Diff p
+
+affineCombo :: (AffineSpace p, v ~ Diff p) => p -> (p,v) -> (v,v)
+affineCombo z l = first (.-. z) l
=====================================
testsuite/tests/typecheck/should_compile/T26358.hs
=====================================
@@ -0,0 +1,48 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module T26358 where
+import Data.Kind
+import Data.Proxy
+
+{- Two failing tests, described in GHC.Core.Unify
+ Note [Shortcomings of the apartness test]
+
+Explanation for TF2
+* We try to reduce
+ (TF2 (F (G Float)) (F Int) (G Float))
+* We can only do so if those arguments are apart from the first
+ equation of TF2, namely (Bool,Char,Int).
+* So we try to unify
+ [F (G Float), F Int, G Float] ~ [Bool, Char, Int]
+* They really are apart, but we can't quite spot that yet;
+ hence #26358
+
+TF1 is similar.
+-}
+
+
+type TF1 :: Type -> Type -> Type -> Type
+type family TF1 a b c where
+ TF1 Bool Char a = Word
+ TF1 a b c = (a,b,c)
+
+type F :: Type -> Type
+type family F a where
+
+foo :: Proxy a
+ -> Proxy (TF1 (F a) (F Int) Int)
+ -> Proxy (F a, F Int, Int)
+foo _ px = px
+
+type TF2 :: Type -> Type -> Type -> Type
+type family TF2 a b c where
+ TF2 Bool Char Int = Word
+ TF2 a b c = (a,b,c)
+
+type G :: Type -> Type
+type family G a where
+
+bar :: Proxy (TF2 (F (G Float)) (F Int) (G Float))
+ -> Proxy (F (G Float), F Int, G Float)
+bar px = px
+
=====================================
testsuite/tests/typecheck/should_compile/all.T
=====================================
@@ -862,6 +862,7 @@ test('DeepSubsumption06', normal, compile, ['-XHaskell98'])
test('DeepSubsumption07', normal, compile, ['-XHaskell2010'])
test('DeepSubsumption08', normal, compile, [''])
test('DeepSubsumption09', normal, compile, [''])
+test('T26350', normal, compile, [''])
test('T26225', normal, compile, [''])
test('T26225b', normal, compile, [''])
test('T21765', normal, compile, [''])
@@ -945,3 +946,5 @@ test('T25992', normal, compile, [''])
test('T14010', normal, compile, [''])
test('T26256a', normal, compile, [''])
test('T25992a', normal, compile, [''])
+test('T26346', normal, compile, [''])
+test('T26358', expect_broken(26358), compile, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/7eecfb55e3aa96cb5ece110700ccf9…
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/7eecfb55e3aa96cb5ece110700ccf9…
You're receiving this email because of your account on gitlab.haskell.org.
1
0
[Git][ghc/ghc][wip/bytecode-library] Load bytecode objects into the linker when they are loaded.
by Matthew Pickering (＠mpickering) 28 Aug '25
by Matthew Pickering (＠mpickering) 28 Aug '25
28 Aug '25
Matthew Pickering pushed to branch wip/bytecode-library at Glasgow Haskell Compiler / GHC
Commits:
99b973a9 by Matthew Pickering at 2025-08-28T17:23:50+01:00
Load bytecode objects into the linker when they are loaded.
- - - - -
17 changed files:
- compiler/GHC/ByteCode/Serialize.hs
- compiler/GHC/Driver/ByteCode.hs
- compiler/GHC/Driver/CodeOutput.hs
- compiler/GHC/Driver/Main.hs
- compiler/GHC/Driver/Pipeline.hs
- compiler/GHC/Linker/Loader.hs
- compiler/GHC/Linker/Types.hs
- compiler/GHC/Runtime/Interpreter.hs
- compiler/GHC/Unit/Finder.hs
- libraries/ghci/GHCi/Message.hs
- testsuite/tests/cabal/Bytecode.hs
- testsuite/tests/cabal/Makefile
- testsuite/tests/cabal/all.T
- testsuite/tests/cabal/bytecode.pkg
- + testsuite/tests/cabal/bytecode.script
- testsuite/tests/cabal/pkg_bytecode.stderr
- testsuite/tests/cabal/pkg_bytecode.stdout
Changes:
=====================================
compiler/GHC/ByteCode/Serialize.hs
=====================================
@@ -9,6 +9,7 @@ module GHC.ByteCode.Serialize
, writeBytecodeLib
, readBytecodeLib
, mkBytecodeLib
+ , decodeOnDiskByteCodeObject
)
where
=====================================
compiler/GHC/Driver/ByteCode.hs
=====================================
@@ -6,7 +6,8 @@ import GHC.Prelude
import GHC.Driver.Session
import GHC.Driver.CodeOutput
import GHC.Driver.Env
-import GHC.Runtime.Interpreter
+import GHC.Runtime.Interpreter.Types
+ ( interpreterDynamic, interpreterProfiled )
import GHC.ByteCode.Types
import GHC.Linker.Types
@@ -23,9 +24,11 @@ import Data.Time
import GHC.Platform.Ways
import GHC.ByteCode.Serialize
+import System.OsPath
-- | Write foreign sources and foreign stubs to temporary files and compile them.
-outputAndCompileForeign :: HscEnv -> Module -> ModLocation -> [(ForeignSrcLang, FilePath)] -> ForeignStubs -> IO [FilePath]
+outputAndCompileForeign :: HscEnv -> Module -> Maybe OsPath -- ^ Source file location
+ -> [(ForeignSrcLang, FilePath)] -> ForeignStubs -> IO [FilePath]
outputAndCompileForeign hsc_env mod_name location foreign_files foreign_stubs = do
let dflags = hsc_dflags hsc_env
logger = hsc_logger hsc_env
@@ -58,13 +61,13 @@ compile_for_interpreter hsc_env use =
adapt_way want = if want (hscInterp hsc_env) then addWay else removeWay
-- | Write the foreign sources and foreign stubs of a bytecode object to temporary files and compile them.
-loadByteCodeObject :: HscEnv -> ModLocation -> ByteCodeObject
+loadByteCodeObject :: HscEnv -> Maybe OsPath -> ByteCodeObject
-> IO (CompiledByteCode, [FilePath])
loadByteCodeObject hsc_env location (ByteCodeObject mod cbc foreign_srcs foreign_stubs) = do
fos <- outputAndCompileForeign hsc_env mod location foreign_srcs foreign_stubs
return (cbc, fos)
-loadByteCodeObjectLinkable :: HscEnv -> UTCTime -> ModLocation -> ByteCodeObject -> IO Linkable
+loadByteCodeObjectLinkable :: HscEnv -> UTCTime -> Maybe OsPath -> ByteCodeObject -> IO Linkable
loadByteCodeObjectLinkable hsc_env linkable_time location bco = do
~(cbc, fos) <- loadByteCodeObject hsc_env location bco
return $! Linkable linkable_time (bco_module bco) (BCOs cbc :| [DotO fo ForeignObject | fo <- fos])
\ No newline at end of file
=====================================
compiler/GHC/Driver/CodeOutput.hs
=====================================
@@ -133,7 +133,7 @@ codeOutput logger tmpfs llvm_config dflags unit_state this_mod filenm location g
ViaCCodeOutput -> outputC logger dflags filenm dus1 final_stream pkg_deps
LlvmCodeOutput -> outputLlvm logger llvm_config dflags filenm dus1 final_stream
JSCodeOutput -> outputJS logger llvm_config dflags filenm final_stream
- ; stubs_exist <- outputForeignStubs logger tmpfs dflags unit_state this_mod location stubs
+ ; stubs_exist <- outputForeignStubs logger tmpfs dflags unit_state this_mod (ml_hs_file_ospath $ location) stubs
; return (filenm, stubs_exist, foreign_fps, a)
}
@@ -269,7 +269,7 @@ outputForeignStubs
-> DynFlags
-> UnitState
-> Module
- -> ModLocation
+ -> Maybe OsPath -- ^ Source file location
-> ForeignStubs
-> IO (Bool, -- Header file created
Maybe FilePath) -- C file created
=====================================
compiler/GHC/Driver/Main.hs
=====================================
@@ -1015,7 +1015,7 @@ checkByteCodeFromObject hsc_env mod_sum = do
-- that the one we have on disk would be suitable as well.
linkable <- unsafeInterleaveIO $ do
bco <- readBinByteCode hsc_env obj_fn
- loadByteCodeObjectLinkable hsc_env obj_date (ms_location mod_sum) bco
+ loadByteCodeObjectLinkable hsc_env obj_date (ml_hs_file_ospath $ ms_location mod_sum) bco
return $ UpToDateItem linkable
_ -> return $ outOfDateItemBecause MissingBytecode Nothing
@@ -2163,7 +2163,7 @@ hscInteractive hsc_env cgguts location = do
let tmpfs = hsc_tmpfs hsc_env
------------------ Create f-x-dynamic C-side stuff -----
(_istub_h_exists, istub_c_exists)
- <- outputForeignStubs logger tmpfs dflags (hsc_units hsc_env) (cgi_module cgguts) location (cgi_foreign cgguts)
+ <- outputForeignStubs logger tmpfs dflags (hsc_units hsc_env) (cgi_module cgguts) (ml_hs_file_ospath $ location) (cgi_foreign cgguts)
return (istub_c_exists, comp_bc)
@@ -2214,7 +2214,7 @@ generateByteCode :: HscEnv
-> IO (CompiledByteCode, [FilePath])
generateByteCode hsc_env cgguts mod_location = do
comp_bc' <- hscGenerateByteCode hsc_env cgguts mod_location
- fos <- outputAndCompileForeign hsc_env (cgi_module cgguts) mod_location (cgi_foreign_files cgguts) (cgi_foreign cgguts)
+ fos <- outputAndCompileForeign hsc_env (cgi_module cgguts) (ml_hs_file_ospath $ mod_location) (cgi_foreign_files cgguts) (cgi_foreign cgguts)
pure (comp_bc', fos)
-- | Generate a byte code object linkable and write it to a file if `-fwrite-bytecode` is enabled.
@@ -2234,7 +2234,7 @@ generateAndWriteByteCodeLinkable hsc_env cgguts mod_location = do
-- It's important the time of the linkable matches the time of the .gbc file for recompilation
-- checking.
bco_time <- maybe getCurrentTime pure =<< modificationTimeIfExists (ml_bytecode_file mod_location)
- loadByteCodeObjectLinkable hsc_env bco_time mod_location bco_object
+ loadByteCodeObjectLinkable hsc_env bco_time (ml_hs_file_ospath $ mod_location) bco_object
mkByteCodeObject :: HscEnv -> Module -> ModLocation -> CgInteractiveGuts -> IO ByteCodeObject
mkByteCodeObject hsc_env mod mod_location cgguts = do
@@ -2249,7 +2249,7 @@ generateFreshByteCodeLinkable :: HscEnv
generateFreshByteCodeLinkable hsc_env mod_name cgguts mod_location = do
bco_time <- getCurrentTime
bco_object <- mkByteCodeObject hsc_env (mkHomeModule (hsc_home_unit hsc_env) mod_name) mod_location cgguts
- loadByteCodeObjectLinkable hsc_env bco_time mod_location bco_object
+ loadByteCodeObjectLinkable hsc_env bco_time (ml_hs_file_ospath $ mod_location) bco_object
------------------------------
hscCompileCmmFile :: HscEnv -> FilePath -> FilePath -> FilePath -> IO (Maybe FilePath)
=====================================
compiler/GHC/Driver/Pipeline.hs
=====================================
@@ -423,6 +423,13 @@ link' hsc_env batch_attempt_linking mHscMessager hpt
return Succeeded
else do
+ -- TODO: This is very awkward.
+
+ -- 1. Ban using --make mode to create -bytecodelib, since then you would not need in-memory linkables
+ -- 2. Make Linkable and ByteCodeObject more similar, so that you can translate between them.
+ -- * Either store .o files in ByteCodeObject <-- MP thinks this way
+ -- * or Store ForeignStubs/ForeignSrcs in Linkable
+ -- 3. Store ByteCodeObject in Linkable directly
let hackyMPtodo l = [ ByteCodeObject (linkableModule l) cbc [] NoStubs | cbc <- linkableBCOs l ]
let linkObjectLinkable action =
=====================================
compiler/GHC/Linker/Loader.hs
=====================================
@@ -132,6 +132,7 @@ import qualified Data.IntMap.Strict as IM
import qualified Data.Map.Strict as M
import Foreign.Ptr (nullPtr)
import GHC.ByteCode.Serialize
+import GHC.Data.Maybe (expectJust)
-- Note [Linkers and loaders]
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -659,7 +660,7 @@ findBytecodeLinkableMaybe hsc_env mod locn = do
loadInterface (text "get_reachable_nodes" <+> parens (ppr mod))
mod ImportBySystem
bco <- readBinByteCode hsc_env bytecode_fn
- Just <$> loadByteCodeObjectLinkable hsc_env bytecode_time locn bco
+ Just <$> loadByteCodeObjectLinkable hsc_env bytecode_time (ml_hs_file_ospath $ locn) bco
get_reachable_nodes :: HscEnv -> [Module] -> IO ([Module], UniqDSet UnitId)
get_reachable_nodes hsc_env mods
@@ -1155,16 +1156,16 @@ loadPackages interp hsc_env new_pkgs = do
loadPackages' :: Interp -> HscEnv -> [UnitId] -> LoaderState -> IO LoaderState
loadPackages' interp hsc_env new_pks pls = do
- pkgs' <- link (pkgs_loaded pls) new_pks
- return $! pls { pkgs_loaded = pkgs'
- }
+ pls' <- link pls new_pks
+ return $! pls'
where
- link :: PkgsLoaded -> [UnitId] -> IO PkgsLoaded
+ link :: LoaderState -> [UnitId] -> IO LoaderState
link pkgs new_pkgs =
foldM link_one pkgs new_pkgs
+ link_one :: LoaderState -> UnitId -> IO LoaderState
link_one pkgs new_pkg
- | new_pkg `elemUDFM` pkgs -- Already linked
+ | new_pkg `elemUDFM` (pkgs_loaded pkgs) -- Already linked
= return pkgs
| Just pkg_cfg <- lookupUnitId (hsc_units hsc_env) new_pkg
@@ -1172,19 +1173,15 @@ loadPackages' interp hsc_env new_pks pls = do
-- Link dependents first
; pkgs' <- link pkgs deps
-- Now link the package itself
- ; (hs_cls, extra_cls, loaded_dlls) <- loadPackage interp hsc_env pkg_cfg
- ; let trans_deps = unionManyUniqDSets [ addOneToUniqDSet (loaded_pkg_trans_deps loaded_pkg_info) dep_pkg
- | dep_pkg <- deps
- , Just loaded_pkg_info <- pure (lookupUDFM pkgs' dep_pkg)
- ]
- ; return (addToUDFM pkgs' new_pkg (LoadedPkgInfo new_pkg hs_cls extra_cls loaded_dlls trans_deps)) }
+ ; loadPackage interp hsc_env pkg_cfg pkgs'
+ }
| otherwise
= throwGhcExceptionIO (CmdLineError ("unknown package: " ++ unpackFS (unitIdFS new_pkg)))
-loadPackage :: Interp -> HscEnv -> UnitInfo -> IO ([LibrarySpec], [LibrarySpec], [RemotePtr LoadedDLL])
-loadPackage interp hsc_env pkg
+loadPackage :: Interp -> HscEnv -> UnitInfo -> LoaderState -> IO LoaderState
+loadPackage interp hsc_env pkg pls
= do
let dflags = hsc_dflags hsc_env
let logger = hsc_logger hsc_env
@@ -1268,7 +1265,7 @@ loadPackage interp hsc_env pkg
-- step to resolve everything.
mapM_ (loadObj interp) objs
mapM_ (loadArchive interp) archs
- mapM_ (loadBytecodeLibrary interp) bytecodes
+ pls' <- foldM (loadBytecodeLibrary hsc_env interp) pls bytecodes
maybePutStr logger "linking ... "
ok <- resolveObjs interp
@@ -1282,11 +1279,35 @@ loadPackage interp hsc_env pkg
if succeeded ok
then do
maybePutStrLn logger "done."
- return (hs_classifieds, extra_classifieds, loaded_dlls)
+ let deps = unitDepends pkg
+ let new_pkg = unitId pkg
+ let trans_deps = unionManyUniqDSets [ addOneToUniqDSet (loaded_pkg_trans_deps loaded_pkg_info) dep_pkg
+ | dep_pkg <- deps
+ , Just loaded_pkg_info <- pure (lookupUDFM (pkgs_loaded pls') dep_pkg)
+ ]
+ let new_pkg_info = LoadedPkgInfo new_pkg hs_classifieds extra_classifieds loaded_dlls trans_deps
+ return pls' { pkgs_loaded = addToUDFM (pkgs_loaded pls') new_pkg new_pkg_info }
+ --return (addToUDFM pkgs' new_pkg new_pkg_info)
+ -- return (hs_classifieds, extra_classifieds, loaded_dlls)
else let errmsg = text "unable to load unit `"
<> pprUnitInfoForUser pkg <> text "'"
in throwGhcExceptionIO (InstallationError (showSDoc dflags errmsg))
+
+loadBytecodeLibrary :: HscEnv -> Interp -> LoaderState -> FilePath -> IO LoaderState
+loadBytecodeLibrary hsc_env interp pls path = do
+ path' <- canonicalizePath path -- Note [loadObj and relative paths]
+ -- TODO: see loadModuleLinkables in GHC/Linker/Loader.hs
+ -- 0. Get the modification time of the module
+ mod_time <- expectJust <$> modificationTimeIfExists path'
+ -- 1. Read the bytecode library
+ (BytecodeLib bcos) <- readBytecodeLib hsc_env path'
+ bcos' <- mapM (decodeOnDiskByteCodeObject hsc_env) bcos
+ linkables <- mapM (loadByteCodeObjectLinkable hsc_env mod_time Nothing) bcos'
+ (pls', _) <- loadModuleLinkables interp hsc_env pls linkables
+ return pls'
+
+
{-
Note [Crash early load_dyn and locateLib]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
=====================================
compiler/GHC/Linker/Types.hs
=====================================
@@ -155,7 +155,7 @@ data LoaderState = LoaderState
-- ^ And the currently-loaded compiled modules (home package)
, pkgs_loaded :: !PkgsLoaded
- -- ^ The currently-loaded packages; always object code
+ -- ^ The currently-loaded packages;
-- haskell libraries, system libraries, transitive dependencies
, temp_sos :: ![(FilePath, String)]
=====================================
compiler/GHC/Runtime/Interpreter.hs
=====================================
@@ -41,7 +41,6 @@ module GHC.Runtime.Interpreter
, loadDLL
, loadArchive
, loadObj
- , loadBytecodeLibrary
, unloadObj
, addLibrarySearchPath
, removeLibrarySearchPath
@@ -78,6 +77,9 @@ import GHCi.RemoteTypes
import GHCi.ResolvedBCO
import GHCi.BreakArray (BreakArray)
import GHC.ByteCode.Breakpoints
+import GHC.ByteCode.Serialize
+import GHC.Driver.Env
+import GHC.Driver.ByteCode
import GHC.ByteCode.Types
import GHC.Linker.Types
@@ -117,6 +119,7 @@ import qualified GHC.InfoProv as InfoProv
import GHC.Builtin.Names
import GHC.Types.Name
import qualified GHC.Unit.Home.Graph as HUG
+import GHC.Utils.Misc
-- Standard libraries
import GHC.Exts
@@ -573,10 +576,6 @@ loadArchive interp path = do
path' <- canonicalizePath path -- Note [loadObj and relative paths]
interpCmd interp (LoadArchive path')
-loadBytecodeLibrary :: Interp -> String -> IO ()
-loadBytecodeLibrary interp path = do
- path' <- canonicalizePath path -- Note [loadObj and relative paths]
- putStrLn $ "I would load bytecode library but I'm not implemented yet" ++ path'
loadObj :: Interp -> String -> IO ()
loadObj interp path = do
=====================================
compiler/GHC/Unit/Finder.hs
=====================================
@@ -781,16 +781,16 @@ mkBytecodePath fopts basename mod_basename = bytecode_basename <.> bytecodesuf
mkStubPaths
:: FinderOpts
-> ModuleName
- -> ModLocation
-> Maybe OsPath
-mkStubPaths fopts mod location = do
+ -> Maybe OsPath
+mkStubPaths fopts mod hs_file_location = do
stub_basename <- in_stub_dir <|> src_basename
pure (stub_basename `mappend` os "_stub" <.> os "h")
where
in_stub_dir = (</> mod_basename) <$> (finder_stubDir fopts)
mod_basename = unsafeEncodeUtf $ moduleNameSlashes mod
- src_basename = OsPath.dropExtension <$> ml_hs_file_ospath location
+ src_basename = OsPath.dropExtension <$> hs_file_location
-- -----------------------------------------------------------------------------
-- findLinkable isn't related to the other stuff in here,
=====================================
libraries/ghci/GHCi/Message.hs
=====================================
@@ -86,6 +86,7 @@ data Message a where
LookupClosure :: String -> Message (Maybe HValueRef)
LoadDLL :: String -> Message (Either String (RemotePtr LoadedDLL))
LoadArchive :: String -> Message () -- error?
+ LoadBytecode :: String -> Message ()
LoadObj :: String -> Message () -- error?
UnloadObj :: String -> Message () -- error?
AddLibrarySearchPath :: String -> Message (RemotePtr ())
@@ -593,6 +594,7 @@ getMessage = do
38 -> Msg <$> (ResumeSeq <$> get)
39 -> Msg <$> (LookupSymbolInDLL <$> get <*> get)
40 -> Msg <$> (WhereFrom <$> get)
+ 41 -> Msg <$> (LoadBytecode <$> get)
_ -> error $ "Unknown Message code " ++ (show b)
putMessage :: Message a -> Put
=====================================
testsuite/tests/cabal/Bytecode.hs
=====================================
@@ -1,3 +1,3 @@
module Bytecode where
-bytecode = "bytecode"
+bytecode = "bytecode from a package"
=====================================
testsuite/tests/cabal/Makefile
=====================================
@@ -300,9 +300,8 @@ PKGCONF08=bytecode.package.conf
LOCAL_GHC_PKG08 = '$(GHC_PKG)' --no-user-package-db -f $(PKGCONF08)
pkg_bytecode :
$(LOCAL_GHC_PKG08) init $(PKGCONF08)
- @echo "bytecode-library-dirs: \$${pkgroot}" >> bytecode.pkg
- @echo "import-dirs: \$${pkgroot}" >> bytecode.pkg
- @echo "library-dirs: \$${pkgroot}" >> bytecode.pkg
+ mkdir outdir
+ mv Bytecode.hs outdir/
+ cd outdir && $(TEST_HC) -bytecodelib -hisuf=dyn_hi -dynamic -o testpkg-1.2.3.4-XXX.bytecode Bytecode.hs -fbyte-code -fwrite-interface -fwrite-byte-code -this-unit-id=testpkg-1.2.3.4-XXX
$(LOCAL_GHC_PKG08) register --force bytecode.pkg
- $(TEST_HC) -bytecodelib -o testpkg-1.2.3.4-XXX.bytecode Bytecode.hs -fbyte-code -fwrite-interface -fwrite-byte-code
- $(TEST_HC) --interactive -package testpkg -package-db $(PKGCONF08)
+ cat bytecode.script | $(TEST_HC) --interactive -package testpkg -package-db $(PKGCONF08)
=====================================
testsuite/tests/cabal/all.T
=====================================
@@ -35,7 +35,7 @@ test('ghcpkg06', [extra_files(['test.pkg', 'testdup.pkg'])], makefile_test, [])
test('ghcpkg07', [extra_files(['test.pkg', 'test7a.pkg', 'test7b.pkg'])], makefile_test, [])
-test('pkg_bytecode', [extra_files(['bytecode.pkg', 'Bytecode.hs']), copy_files], makefile_test, [])
+test('pkg_bytecode', [extra_files(['bytecode.pkg', 'Bytecode.hs', "bytecode.script"]), copy_files], makefile_test, [])
# Test that we *can* compile a module that also belongs to a package
# (this was disallowed in GHC 6.4 and earlier)
=====================================
testsuite/tests/cabal/bytecode.pkg
=====================================
@@ -13,7 +13,8 @@ category: none
author: simonmar(a)microsoft.com
exposed: True
exposed-modules: Bytecode
-import-dirs:
-library-dirs:
+import-dirs: ${pkgroot}/outdir
+library-dirs: ${pkgroot}/outdir
include-dirs:
+bytecode-library-dirs: ${pkgroot}/outdir
hs-libraries: testpkg-1.2.3.4-XXX
=====================================
testsuite/tests/cabal/bytecode.script
=====================================
@@ -0,0 +1,2 @@
+import Bytecode
+bytecode
=====================================
testsuite/tests/cabal/pkg_bytecode.stderr
=====================================
@@ -1,6 +1,6 @@
-testpkg-1.2.3.4: cannot find any of ["Bytecode.hi","Bytecode.p_hi","Bytecode.dyn_hi","Bytecode.p_dyn_hi"] (ignoring)
testpkg-1.2.3.4: cannot find any of ["libtestpkg-1.2.3.4-XXX.a","libtestpkg-1.2.3.4-XXX_p.a","libtestpkg-1.2.3.4-XXX-ghc9.15.20250811.so","libtestpkg-1.2.3.4-XXX_p-ghc9.15.20250811.so","libtestpkg-1.2.3.4-XXX-ghc9.15.20250811.dylib","libtestpkg-1.2.3.4-XXX_p-ghc9.15.20250811.dylib","testpkg-1.2.3.4-XXX-ghc9.15.20250811.dll","testpkg-1.2.3.4-XXX_p-ghc9.15.20250811.dll"] on library path (ignoring)
-hs_classifieds [BytecodeLibrary ./testpkg-1.2.3.4-XXX.bytecode]
+hs_classifieds
+ [BytecodeLibrary ./outdir/testpkg-1.2.3.4-XXX.bytecode]
hs_classifieds
[DLLPath /home/matt/ghc-bytecode/_new/stage1/lib/../lib/x86_64-linux-ghc-9.15.20250811/libHSghc-internal-9.1500.0-inplace-ghc9.15.20250811.so]
hs_classifieds
=====================================
testsuite/tests/cabal/pkg_bytecode.stdout
=====================================
@@ -1,6 +1,6 @@
-Reading package info from "bytecode.pkg" ... done.
[1 of 2] Compiling Bytecode ( Bytecode.hs, interpreted )
[2 of 2] Linking testpkg-1.2.3.4-XXX.bytecode
+Reading package info from "bytecode.pkg" ... done.
GHCi, version 9.15.20250811: https://www.haskell.org/ghc/ :? for help
-I would load bytecode library but I'm not implemented yet/tmp/nix-shell-4063774-0/ghctest-8522p1jo/test spaces/testsuite/tests/cabal/pkg_bytecode.run/testpkg-1.2.3.4-XXX.bytecode
+ghci> ghci> "bytecode from a package"
ghci> Leaving GHCi.
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/99b973a9ada4b427b688fde4d2a4f1e…
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/99b973a9ada4b427b688fde4d2a4f1e…
You're receiving this email because of your account on gitlab.haskell.org.
1
0