[Git][ghc/ghc][wip/T24769] WIP on 24769; needs a note
Krzysztof Gogolewski (@monoidal)
gitlab at gitlab.haskell.org
Mon Jun 10 12:27:00 UTC 2024
Krzysztof Gogolewski pushed to branch wip/T24769 at Glasgow Haskell Compiler / GHC
Commits:
023aac51 by Krzysztof Gogolewski at 2024-06-10T14:25:56+02:00
WIP on 24769; needs a note
Co-authored-by: Richard Eisenberg <reisenberg at janestreet.com>
- - - - -
17 changed files:
- compiler/GHC/Tc/Gen/Bind.hs
- compiler/GHC/Tc/Solver.hs
- testsuite/tests/rep-poly/T23176.stderr
- + testsuite/tests/rep-poly/T23505.hs
- + testsuite/tests/rep-poly/T23505.stderr
- + testsuite/tests/rep-poly/T24769a.hs
- + testsuite/tests/rep-poly/T24769a.stderr
- + testsuite/tests/rep-poly/T24769b.hs
- + testsuite/tests/rep-poly/T24769b.stderr
- + testsuite/tests/rep-poly/T24769c.hs
- + testsuite/tests/rep-poly/T24769c.stderr
- + testsuite/tests/rep-poly/T24769c_aux.hs
- + testsuite/tests/rep-poly/T24769d.hs
- + testsuite/tests/rep-poly/T24769d.stderr
- + testsuite/tests/rep-poly/T24769e.script
- + testsuite/tests/rep-poly/T24769e.stdout
- testsuite/tests/rep-poly/all.T
Changes:
=====================================
compiler/GHC/Tc/Gen/Bind.hs
=====================================
@@ -52,7 +52,7 @@ import GHC.Tc.Gen.Pat
import GHC.Tc.Utils.TcMType
import GHC.Tc.Instance.Family( tcGetFamInstEnvs )
import GHC.Tc.Utils.TcType
-import GHC.Tc.Validity (checkValidType, checkEscapingKind)
+import GHC.Tc.Validity (checkValidType)
import GHC.Tc.Zonk.TcType
import GHC.Core.Reduction ( Reduction(..) )
import GHC.Core.Multiplicity
@@ -1013,9 +1013,7 @@ mkInferredPolyId residual insoluble qtvs inferred_theta poly_name mb_sig_inst mo
; unless insoluble $
addErrCtxtM (mk_inf_msg poly_name inferred_poly_ty) $
- do { checkEscapingKind inferred_poly_ty
- -- See Note [Inferred type with escaping kind]
- ; checkValidType (InfSigCtxt poly_name) inferred_poly_ty }
+ checkValidType (InfSigCtxt poly_name) inferred_poly_ty
-- See Note [Validity of inferred types]
-- unless insoluble: if we found an insoluble error in the
-- function definition, don't do this check; otherwise
@@ -1259,22 +1257,6 @@ Examples that might fail:
or multi-parameter type classes
- an inferred type that includes unboxed tuples
-Note [Inferred type with escaping kind]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Check for an inferred type with an escaping kind; e.g. #23051
- forall {k} {f :: k -> RuntimeRep} {g :: k} {a :: TYPE (f g)}. a
-where the kind of the body of the forall mentions `f` and `g` which
-are bound by the forall. No no no.
-
-This check, mkInferredPolyId, is really in the wrong place:
-`inferred_poly_ty` doesn't obey the PKTI and it would be better not to
-generalise it in the first place; see #20686. But for now it works.
-
-I considered adjusting the generalisation in GHC.Tc.Solver to directly check for
-escaping kind variables; instead, promoting or defaulting them. But that
-gets into the defaulting swamp and is a non-trivial and unforced
-change, so I have left it alone for now.
-
Note [Impedance matching]
~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
=====================================
compiler/GHC/Tc/Solver.hs
=====================================
@@ -1324,6 +1324,10 @@ simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds
psig_theta = [ pred | sig <- partial_sigs
, pred <- sig_inst_theta sig ]
+ ; zonked_kinds <- mapM (TcM.liftZonkM . TcM.zonkTcType . typeKind . snd) name_taus
+ ; _ <- promoteTyVarSet (tyCoVarsOfTypes zonked_kinds)
+ -- Promote free variables in the kind (#24769)
+
; dep_vars <- candidateQTyVarsOfTypes (psig_tv_tys ++ psig_theta ++ map snd name_taus)
; skol_info <- mkSkolemInfo (InferSkol name_taus)
@@ -1837,6 +1841,7 @@ decidePromotedTyVars :: InferMode
-- (c) Connected by an equality or fundep to
-- * a type variable at level < N, or
-- * A tyvar subject to (a), (b) or (c)
+-- (d) Free in kind (e.g. we can't generalize over r in 'forall (a :: TYPE r). a')
-- Having found all such level-N tyvars that we can't generalise,
-- promote them, to eliminate them from further consideration.
--
@@ -1867,6 +1872,8 @@ decidePromotedTyVars infer_mode name_taus psigs candidates
co_vars = coVarsOfTypes (psig_tys ++ taus ++ candidates)
co_var_tvs = closeOverKinds co_vars
+ escapingKindVars = mapUnionVarSet (\x -> tyCoVarsOfType (typeKind x)) taus
+
mono_tvs0 = filterVarSet (not . isQuantifiableTv tc_lvl) $
tyCoVarsOfTypes candidates
-- We need to grab all the non-quantifiable tyvars in the
@@ -1881,7 +1888,9 @@ decidePromotedTyVars infer_mode name_taus psigs candidates
-- are in the equality constraint with alpha. Actual test case:
-- typecheck/should_compile/tc213
- mono_tvs1 = mono_tvs0 `unionVarSet` co_var_tvs
+ mono_tvs0a = mono_tvs0 `unionVarSet` escapingKindVars
+
+ mono_tvs1 = mono_tvs0a `unionVarSet` co_var_tvs
-- mono_tvs1 is now the set of variables from an outer scope
-- (that's mono_tvs0) and the set of covars, closed over kinds.
@@ -1916,6 +1925,7 @@ decidePromotedTyVars infer_mode name_taus psigs candidates
mono_tvs = (mono_tvs2 `unionVarSet` constrained_tvs)
`delVarSetList` psig_qtvs
+ `unionVarSet` escapingKindVars
-- (`delVarSetList` psig_qtvs): if the user has explicitly
-- asked for quantification, then that request "wins"
-- over the MR.
=====================================
testsuite/tests/rep-poly/T23176.stderr
=====================================
@@ -1,30 +1,45 @@
+T23176.hs:5:1: error: [GHC-55287]
+ The binder ‘f’ does not have a fixed runtime representation.
+ Its type is:
+ w :: TYPE (r1 s1)
-T23176.hs:5:1: error: [GHC-52083]
- The binder ‘f’
- cannot be assigned a fixed runtime representation, not even by defaulting.
- Suggested fix: Add a type signature.
+T23176.hs:5:19: error: [GHC-94185]
+ • Can't quantify over ‘s’
+ bound by the partial type signature:
+ <expression> :: (_ :: TYPE (r s))
+ • In the expression: outOfScope :: (_ :: TYPE (r s))
+ In an equation for ‘f’: f = outOfScope :: (_ :: TYPE (r s))
-T23176.hs:5:1: error: [GHC-52083]
- The binder ‘f’
- cannot be assigned a fixed runtime representation, not even by defaulting.
- Suggested fix: Add a type signature.
+T23176.hs:5:19: error: [GHC-94185]
+ • Can't quantify over ‘r’
+ bound by the partial type signature:
+ <expression> :: (_ :: TYPE (r s))
+ • In the expression: outOfScope :: (_ :: TYPE (r s))
+ In an equation for ‘f’: f = outOfScope :: (_ :: TYPE (r s))
-T23176.hs:5:1: error: [GHC-52083]
- The binder ‘f’
- cannot be assigned a fixed runtime representation, not even by defaulting.
- Suggested fix: Add a type signature.
+T23176.hs:6:1: error: [GHC-55287]
+ The binder ‘g’ does not have a fixed runtime representation.
+ Its type is:
+ forall {w :: TYPE (r0 s0)}. w :: TYPE (r0 s0)
-T23176.hs:6:1: error: [GHC-52083]
- The pattern binding
- cannot be assigned a fixed runtime representation, not even by defaulting.
- Suggested fix: Add a type signature.
+T23176.hs:6:12: error: [GHC-55287]
+ • The pattern binding does not have a fixed runtime representation.
+ Its type is:
+ w :: TYPE (r0 s0)
+ • In the expression: outOfScope :: (_ :: TYPE (r s))
+ In a pattern binding: (g :: _) = outOfScope :: (_ :: TYPE (r s))
-T23176.hs:6:1: error: [GHC-52083]
- The pattern binding
- cannot be assigned a fixed runtime representation, not even by defaulting.
- Suggested fix: Add a type signature.
+T23176.hs:6:26: error: [GHC-94185]
+ • Can't quantify over ‘s’
+ bound by the partial type signature:
+ <expression> :: (_ :: TYPE (r s))
+ • In the expression: outOfScope :: (_ :: TYPE (r s))
+ In a pattern binding: (g :: _) = outOfScope :: (_ :: TYPE (r s))
+
+T23176.hs:6:26: error: [GHC-94185]
+ • Can't quantify over ‘r’
+ bound by the partial type signature:
+ <expression> :: (_ :: TYPE (r s))
+ • In the expression: outOfScope :: (_ :: TYPE (r s))
+ In a pattern binding: (g :: _) = outOfScope :: (_ :: TYPE (r s))
-T23176.hs:6:1: error: [GHC-52083]
- The pattern binding
- cannot be assigned a fixed runtime representation, not even by defaulting.
- Suggested fix: Add a type signature.
=====================================
testsuite/tests/rep-poly/T23505.hs
=====================================
@@ -0,0 +1,5 @@
+module M where
+
+import GHC.Exts
+
+f = f :: (_ :: TYPE r)
=====================================
testsuite/tests/rep-poly/T23505.stderr
=====================================
@@ -0,0 +1,23 @@
+T23505.hs:5:1: error: [GHC-55287]
+ The binder ‘f’ does not have a fixed runtime representation.
+ Its type is:
+ forall {t :: TYPE r0}. t :: TYPE r0
+
+T23505.hs:5:10: error: [GHC-94185]
+ • Can't quantify over ‘r’
+ bound by the partial type signature: <expression> :: (_ :: TYPE r)
+ • In the expression: f :: (_ :: TYPE r)
+ In an equation for ‘f’: f = f :: (_ :: TYPE r)
+
+T23505.hs:5:11: error: [GHC-88464]
+ • Found type wildcard ‘_’ standing for ‘t :: TYPE r0’
+ Where: ‘r0’ is an ambiguous type variable
+ ‘t’ is a rigid type variable bound by
+ the inferred type of f :: t
+ at T23505.hs:5:1-22
+ To use the inferred type, enable PartialTypeSignatures
+ • In an expression type signature: (_ :: TYPE r)
+ In the expression: f :: (_ :: TYPE r)
+ In an equation for ‘f’: f = f :: (_ :: TYPE r)
+ • Relevant bindings include f :: t (bound at T23505.hs:5:1)
+
=====================================
testsuite/tests/rep-poly/T24769a.hs
=====================================
@@ -0,0 +1,5 @@
+module T24769a where
+
+import GHC.Exts
+
+f = f :: (_ :: TYPE (r s))
=====================================
testsuite/tests/rep-poly/T24769a.stderr
=====================================
@@ -0,0 +1,33 @@
+T24769a.hs:5:1: error: [GHC-55287]
+ The binder ‘f’ does not have a fixed runtime representation.
+ Its type is:
+ forall {t :: TYPE (r0 s0)}. t :: TYPE (r0 s0)
+
+T24769a.hs:5:10: error: [GHC-94185]
+ • Can't quantify over ‘s’
+ bound by the partial type signature:
+ <expression> :: (_ :: TYPE (r s))
+ • In the expression: f :: (_ :: TYPE (r s))
+ In an equation for ‘f’: f = f :: (_ :: TYPE (r s))
+
+T24769a.hs:5:10: error: [GHC-94185]
+ • Can't quantify over ‘r’
+ bound by the partial type signature:
+ <expression> :: (_ :: TYPE (r s))
+ • In the expression: f :: (_ :: TYPE (r s))
+ In an equation for ‘f’: f = f :: (_ :: TYPE (r s))
+
+T24769a.hs:5:11: error: [GHC-88464]
+ • Found type wildcard ‘_’ standing for ‘t :: TYPE (r0 s0)’
+ Where: ‘r0’ is an ambiguous type variable
+ ‘k0’ is an ambiguous type variable
+ ‘s0’ is an ambiguous type variable
+ ‘t’ is a rigid type variable bound by
+ the inferred type of f :: t
+ at T24769a.hs:5:1-26
+ To use the inferred type, enable PartialTypeSignatures
+ • In an expression type signature: (_ :: TYPE (r s))
+ In the expression: f :: (_ :: TYPE (r s))
+ In an equation for ‘f’: f = f :: (_ :: TYPE (r s))
+ • Relevant bindings include f :: t (bound at T24769a.hs:5:1)
+
=====================================
testsuite/tests/rep-poly/T24769b.hs
=====================================
@@ -0,0 +1,6 @@
+module T24769b where
+
+import GHC.Exts
+
+f :: (_ :: TYPE r)
+f = f
=====================================
testsuite/tests/rep-poly/T24769b.stderr
=====================================
@@ -0,0 +1,4 @@
+T24769b.hs:6:1: error: [GHC-94185]
+ Can't quantify over ‘r’
+ bound by the partial type signature: f :: (_ :: TYPE r)
+
=====================================
testsuite/tests/rep-poly/T24769c.hs
=====================================
@@ -0,0 +1,5 @@
+{-# LANGUAGE TemplateHaskell, PartialTypeSignatures #-}
+module T24769c where
+
+import T24769c_aux
+h = $$g
=====================================
testsuite/tests/rep-poly/T24769c.stderr
=====================================
@@ -0,0 +1,20 @@
+[1 of 2] Compiling T24769c_aux ( T24769c_aux.hs, T24769c_aux.o )
+T24769c_aux.hs:8:13: warning: [GHC-88464] [-Wpartial-type-signatures (in -Wdefault)]
+ • Found type wildcard ‘_’ standing for ‘w :: TYPE (r s)’
+ Where: ‘r’, ‘s’, ‘w’ are rigid type variables bound by
+ the inferred type of g :: Code Q w
+ at T24769c_aux.hs:(9,1)-(11,22)
+ • In the second argument of ‘Code’, namely ‘_’
+ In the type signature: g :: Code Q _
+
+[2 of 2] Compiling T24769c ( T24769c.hs, T24769c.o )
+T24769c.hs:5:1: error: [GHC-52083]
+ The binder ‘h’
+ cannot be assigned a fixed runtime representation, not even by defaulting.
+ Suggested fix: Add a type signature.
+
+T24769c.hs:5:1: error: [GHC-52083]
+ The binder ‘h’
+ cannot be assigned a fixed runtime representation, not even by defaulting.
+ Suggested fix: Add a type signature.
+
=====================================
testsuite/tests/rep-poly/T24769c_aux.hs
=====================================
@@ -0,0 +1,11 @@
+{-# LANGUAGE TemplateHaskell, PartialTypeSignatures #-}
+module T24769c_aux where
+
+import Data.Kind
+import GHC.Exts
+import Language.Haskell.TH (Code, Q)
+
+g :: Code Q _
+g = [||let f :: forall (r :: Type -> RuntimeRep) s (a :: TYPE (r s)). () -> a
+ f = f
+ in f () ||]
=====================================
testsuite/tests/rep-poly/T24769d.hs
=====================================
@@ -0,0 +1,8 @@
+{-# LANGUAGE PartialTypeSignatures #-}
+module T24769d where
+
+import GHC.Exts
+import GHC.Stack
+
+f :: forall r (a :: TYPE r). (HasCallStack, _) => a
+f = undefined
=====================================
testsuite/tests/rep-poly/T24769d.stderr
=====================================
@@ -0,0 +1,5 @@
+T24769d.hs:8:1: error: [GHC-94185]
+ Can't quantify over ‘r’
+ bound by the partial type signature:
+ f :: forall r (a :: TYPE r). (HasCallStack, _) => a
+
=====================================
testsuite/tests/rep-poly/T24769e.script
=====================================
@@ -0,0 +1,3 @@
+:m GHC.Exts Data.Kind
+f :: forall (r :: Type -> RuntimeRep) s (a :: TYPE (r s)). () -> a; f = f
+:t f ()
=====================================
testsuite/tests/rep-poly/T24769e.stdout
=====================================
@@ -0,0 +1 @@
+f () :: forall {a :: TYPE (r0 s0)}. a
=====================================
testsuite/tests/rep-poly/all.T
=====================================
@@ -37,6 +37,7 @@ test('T23153', normal, compile_fail, [''])
test('T23154', normal, compile_fail, [''])
test('T23176', normal, compile_fail, ['-XPartialTypeSignatures -fdefer-out-of-scope-variables'])
test('T23903', normal, compile_fail, [''])
+test('T23505', normal, compile_fail, [''])
test('EtaExpandDataCon', normal, compile, ['-O'])
test('EtaExpandStupid1', normal, compile, ['-Wno-deprecated-flags'])
@@ -107,6 +108,11 @@ test('RepPolyWrappedVar', normal, compile_fail, [''])
test('RepPolyWrappedVar2', [js_skip], compile, [''])
test('UnliftedNewtypesCoerceFail', normal, compile_fail, [''])
test('UnliftedNewtypesLevityBinder', normal, compile_fail, [''])
+test('T24769a', normal, compile_fail, [''])
+test('T24769b', normal, compile_fail, [''])
+test('T24769c', [extra_files(['T24769c_aux.hs'])], multimod_compile_fail, ['T24769c', ''])
+test('T24769d', normal, compile_fail, [''])
+test('T24769e', normal, ghci_script, ['T24769e.script'])
###############################################################################
## The following tests require rewriting in RuntimeReps, ##
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/023aac51fcfa3be08da2e380ee765871d83a2fe8
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/023aac51fcfa3be08da2e380ee765871d83a2fe8
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20240610/0ed75092/attachment-0001.html>
More information about the ghc-commits
mailing list