[Git][ghc/ghc][wip/derived-refactor] Embrace oclose.
Richard Eisenberg
gitlab at gitlab.haskell.org
Tue Jul 28 04:09:31 UTC 2020
Richard Eisenberg pushed to branch wip/derived-refactor at Glasgow Haskell Compiler / GHC
Commits:
d57c9cdb by Richard Eisenberg at 2020-07-28T00:09:05-04:00
Embrace oclose.
- - - - -
19 changed files:
- compiler/GHC/Tc/Errors.hs
- compiler/GHC/Tc/Instance/FunDeps.hs
- compiler/GHC/Tc/Solver.hs
- compiler/GHC/Tc/Solver/Monad.hs
- − testsuite/tests/typecheck/should_compile/T18398.stderr
- testsuite/tests/typecheck/should_compile/T7220a.stderr
- testsuite/tests/typecheck/should_compile/all.T
- testsuite/tests/typecheck/should_fail/FD1.hs
- testsuite/tests/typecheck/should_fail/FD1.stderr
- testsuite/tests/typecheck/should_fail/FD2.stderr
- testsuite/tests/typecheck/should_fail/T10194.stderr
- testsuite/tests/typecheck/should_fail/T11514.stderr
- testsuite/tests/typecheck/should_fail/T12563.stderr
- testsuite/tests/typecheck/should_fail/T12589.stderr
- testsuite/tests/typecheck/should_compile/T18398.hs → testsuite/tests/typecheck/should_fail/T18398.hs
- + testsuite/tests/typecheck/should_fail/T18398.stderr
- testsuite/tests/typecheck/should_compile/T18406.hs → testsuite/tests/typecheck/should_fail/T18406.hs
- + testsuite/tests/typecheck/should_fail/T18406.stderr
- testsuite/tests/typecheck/should_fail/all.T
Changes:
=====================================
compiler/GHC/Tc/Errors.hs
=====================================
@@ -524,8 +524,14 @@ This only matters in instance declarations..
-}
-- | A predicate with its arising location; used to encapsulate a constraint
--- that will give rise to a warning.
+-- that will give rise to a diagnostic.
data ErrorItem
+-- We could perhaps use Ct here (and indeed used to do exactly that), but
+-- having a separate type gives to denote errors-in-formation gives us
+-- a nice place to do pre-processing, such as calculating ei_suppress.
+-- Perhaps some day, an ErrorItem could eventually evolve to contain
+-- the error text (or some representation of it), so we can then have all
+-- the errors together when deciding which to report.
= EI { ei_pred :: PredType -- report about this
-- The ei_pred field will never be an unboxed equality with
-- a (casted) tyvar on the right; this is guaranteed by the solver
@@ -666,9 +672,6 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_impl = implics
suppress item
| Wanted _ <- ei_flavour item
= is_ww_fundep_item item
-{- "RAE" || (not has_gadt_match_here &&
- is_given_eq item (classifyPredType (ei_pred item)))
--}
| otherwise
= False
@@ -747,7 +750,7 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_impl = implics
is_irred _ (IrredPred {}) = True
is_irred _ _ = False
- -- See situation (2) of Note [Suppress confusing errors]
+ -- See situation (1) of Note [Suppress confusing errors]
is_ww_fundep item _ = is_ww_fundep_item item
is_ww_fundep_item = isWantedWantedFunDepOrigin . errorItemOrigin
@@ -798,7 +801,7 @@ isTyFun_maybe ty = case tcSplitTyConApp_maybe ty of
Certain errors we might encounter are potentially confusing to users.
If there are any other errors to report, at all, we want to suppress these.
-Which errors:
+Which errors (only 1 case right now):
1) Errors which arise from the interaction of two Wanted fun-dep constraints.
Example:
@@ -828,14 +831,6 @@ Which errors:
both are givens, the error represents unreachable code. For
a Given/Wanted case, see #9612.
-2) Errors which arise from given functional dependencies. Functional
- dependencies have no evidence, and so they are always Wanted -- we have no
- evidence to supply to build a Given. So we can have a Wanted that arises
- from Givens. These can be surprising for users. However, we still must
- report (in contrast to Note [Given errors]): the (non-existent) evidence
- might have been used to rewrite another Wanted. If we fail to report, then
- we get an unfilled coercion hole. This happened in typecheck/should_fail/FD1.
-
Mechanism:
We use the `suppress` function within reportWanteds to filter out these two
=====================================
compiler/GHC/Tc/Instance/FunDeps.hs
=====================================
@@ -551,6 +551,13 @@ oclose preds fixed_tvs
| null tv_fds = fixed_tvs -- Fast escape hatch for common case.
| otherwise = fixVarSet extend fixed_tvs
where
+ non_ip_preds = filterOut isIPPred preds
+ -- implicit params don't really determine a type variable, and
+ -- skipping this causes implicit params to monomorphise too many
+ -- variables; see Note [Inheriting implicit parameters] in
+ -- GHC.Tc.Utils.TcType. Skipping causes typecheck/should_compile/tc219
+ -- to fail.
+
extend fixed_tvs = foldl' add fixed_tvs tv_fds
where
add fixed_tvs (ls,rs)
@@ -561,7 +568,7 @@ oclose preds fixed_tvs
tv_fds :: [(TyCoVarSet,TyCoVarSet)]
tv_fds = [ (tyCoVarsOfTypes ls, fvVarSet $ injectiveVarsOfTypes True rs)
-- See Note [Care with type functions]
- | pred <- preds
+ | pred <- non_ip_preds
, pred' <- pred : transSuperClasses pred
-- Look for fundeps in superclasses too
, (ls, rs) <- determined pred' ]
=====================================
compiler/GHC/Tc/Solver.hs
=====================================
@@ -1063,9 +1063,8 @@ decideMonoTyVars infer_mode name_taus psigs candidates
; tc_lvl <- TcM.getTcLevel
; let psig_tys = mkTyVarTys psig_qtvs ++ psig_theta
- all_tys = candidates ++ psig_tys ++ taus
- co_vars = coVarsOfTypes all_tys
+ co_vars = coVarsOfTypes (psig_tys ++ taus)
co_var_tvs = closeOverKinds co_vars
-- The co_var_tvs are tvs mentioned in the types of covars or
-- coercion holes. We can't quantify over these covars, so we
@@ -1074,7 +1073,7 @@ decideMonoTyVars infer_mode name_taus psigs candidates
-- quantify over k either! Hence closeOverKinds
mono_tvs0 = filterVarSet (not . isQuantifiableTv tc_lvl) $
- tyCoVarsOfTypes all_tys
+ tyCoVarsOfTypes candidates
-- We need to grab all the non-quantifiable tyvars in the
-- types so that we can grow this set to find other
-- non-quantifiable tyvars. This can happen with something
@@ -1093,21 +1092,14 @@ decideMonoTyVars infer_mode name_taus psigs candidates
-- (that's mono_tvs0) and the set of covars, closed over kinds.
-- Given this set of variables we know we will not quantify,
-- we want to find any other variables that are determined by this
- -- set, by functional dependencies or equalities. But we
- -- want to look at only those constraints which we are unlikely
- -- to quantify over, in the end. (If we quantify over the constraint
- -- itself, then there is no need to avoid quantifying over its
- -- variables.) This final determination is done by
- -- pickQuantifiablePreds, but it needs to know the set of
- -- quantified variables first. So we make an approximation here:
- -- we guess that we will not quantify over equalities, but will
- -- quantify over everything else.
-
- eq_constraints = filter isEqPrimPred candidates
- mono_tvs2 = oclose eq_constraints mono_tvs1
+ -- set, by functional dependencies or equalities. We thus use
+ -- oclose to find all further variables determined by this root
+ -- set.
+
+ mono_tvs2 = oclose candidates mono_tvs1
constrained_tvs = filterVarSet (isQuantifiableTv tc_lvl) $
- (oclose eq_constraints (tyCoVarsOfTypes no_quant)
+ (oclose candidates (tyCoVarsOfTypes no_quant)
`minusVarSet` mono_tvs2)
`delVarSetList` psig_qtvs
-- constrained_tvs: the tyvars that we are not going to
=====================================
compiler/GHC/Tc/Solver/Monad.hs
=====================================
@@ -1646,7 +1646,8 @@ maybeKickOut ics ct
; return ics' }
-- See [Kick out existing binding for implicit parameter]
- | CDictCan { cc_class = cls, cc_tyargs = [ip_name_strty, _ip_ty] } <- ct
+ | isGivenCt ct
+ , CDictCan { cc_class = cls, cc_tyargs = [ip_name_strty, _ip_ty] } <- ct
, isIPClass cls
, Just ip_name <- isStrLitTy ip_name_strty
-- Would this be more efficient if we used findDictsByClass and then delDict?
=====================================
testsuite/tests/typecheck/should_compile/T18398.stderr deleted
=====================================
@@ -1,13 +0,0 @@
-TYPE SIGNATURES
- f :: forall {p}. C Ex p => Ex -> (p -> (), p -> ())
- meth :: forall a b. C a b => a -> b -> ()
-TYPE CONSTRUCTORS
- class C{2} :: * -> * -> Constraint
- data type Ex{0} :: *
-COERCION AXIOMS
- axiom FloatFDs2.N:C :: C a b = a -> b -> ()
-DATA CONSTRUCTORS
- MkEx :: forall a. a -> Ex
-Dependent modules: []
-Dependent packages: [base-4.14.0.0, ghc-prim-0.6.1,
- integer-gmp-1.0.3.0]
=====================================
testsuite/tests/typecheck/should_compile/T7220a.stderr
=====================================
@@ -1,14 +1,22 @@
T7220a.hs:17:6: error:
- • Could not deduce (C a b)
- from the context: (C a0 b, TF b ~ Y)
- bound by a type expected by the context:
- forall b. (C a0 b, TF b ~ Y) => b
+ • Couldn't match type ‘a0’ with ‘a’
+ arising from a functional dependency between constraints:
+ ‘C a b’
+ arising from a type expected by the context:
+ forall b. (C a b, TF b ~ Y) => b at T7220a.hs:17:6-44
+ ‘C a0 b’
+ arising from a type expected by the context:
+ forall b. (C a0 b, TF b ~ Y) => b at T7220a.hs:17:6-44
+ ‘a0’ is untouchable
+ inside the constraints: (C a0 b, TF b ~ Y)
+ bound by a type expected by the context:
+ forall b. (C a0 b, TF b ~ Y) => b
+ at T7220a.hs:17:6-44
+ ‘a’ is a rigid type variable bound by
+ the type signature for:
+ f :: forall a. (forall b. (C a b, TF b ~ Y) => b) -> X
at T7220a.hs:17:6-44
- Possible fix:
- add (C a b) to the context of
- a type expected by the context:
- forall b. (C a0 b, TF b ~ Y) => b
• In the ambiguity check for ‘f’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature: f :: (forall b. (C a b, TF b ~ Y) => b) -> X
=====================================
testsuite/tests/typecheck/should_compile/all.T
=====================================
@@ -704,6 +704,4 @@ test('T18036', normal, compile, [''])
test('T18036a', normal, compile, [''])
test('FunDepOrigin1', normal, compile, [''])
test('FloatFDs', normal, compile, [''])
-test('T18398', normal, compile, [''])
test('ImplicitParamFDs', normal, compile, [''])
-test('T18406', normal, compile, [''])
=====================================
testsuite/tests/typecheck/should_fail/FD1.hs
=====================================
@@ -14,4 +14,3 @@ instance E a a
plus :: (E a (Int -> Int)) => Int -> a
plus x y = x + y
-
=====================================
testsuite/tests/typecheck/should_fail/FD1.stderr
=====================================
@@ -1,15 +1,10 @@
-FD1.hs:15:9: error:
- • Couldn't match type ‘a’ with ‘Int -> Int’
- arising from a functional dependency between:
- constraint ‘E a (Int -> Int)’
- arising from the type signature for:
- plus :: forall a. E a (Int -> Int) => Int -> a
- instance ‘E a1 a1’ at FD1.hs:13:10-14
+FD1.hs:16:1: error:
+ • Couldn't match expected type ‘a’ with actual type ‘Int -> Int’
‘a’ is a rigid type variable bound by
the type signature for:
plus :: forall a. E a (Int -> Int) => Int -> a
- at FD1.hs:15:9-38
- • In the ambiguity check for ‘plus’
- To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
- In the type signature: plus :: (E a (Int -> Int)) => Int -> a
+ at FD1.hs:15:1-38
+ • The equation(s) for ‘plus’ have two value arguments,
+ but its type ‘Int -> a’ has only one
+ • Relevant bindings include plus :: Int -> a (bound at FD1.hs:16:1)
=====================================
testsuite/tests/typecheck/should_fail/FD2.stderr
=====================================
@@ -1,17 +1,6 @@
-FD2.hs:24:12: error:
- • Couldn't match type ‘e1’ with ‘e’
- arising from a functional dependency between constraints:
- ‘Elem a e1’
- arising from the type signature for:
- mf :: forall e.
- Elem a e =>
- e -> Maybe e -> Maybe e at FD2.hs:24:12-54
- ‘Elem a e’
- arising from the type signature for:
- foldr1 :: forall e.
- Elem a e =>
- (e -> e -> e) -> a -> e at FD2.hs:21:13-47
+FD2.hs:26:36: error:
+ • Couldn't match expected type ‘e’ with actual type ‘e1’
‘e1’ is a rigid type variable bound by
the type signature for:
mf :: forall e1. Elem a e1 => e1 -> Maybe e1 -> Maybe e1
@@ -20,13 +9,12 @@ FD2.hs:24:12: error:
the type signature for:
foldr1 :: forall e. Elem a e => (e -> e -> e) -> a -> e
at FD2.hs:21:13-47
- • In an equation for ‘foldr1’:
- foldr1 f xs
- = fromMaybe (error "foldr1: empty structure") (foldr mf Nothing xs)
- where
- mf :: Elem a e => (e -> Maybe e -> Maybe e)
- mf x Nothing = Just x
- mf x (Just y) = Just (f x y)
+ • In the first argument of ‘f’, namely ‘x’
+ In the first argument of ‘Just’, namely ‘(f x y)’
+ In the expression: Just (f x y)
• Relevant bindings include
+ y :: e1 (bound at FD2.hs:26:23)
+ x :: e1 (bound at FD2.hs:26:15)
+ mf :: e1 -> Maybe e1 -> Maybe e1 (bound at FD2.hs:25:12)
f :: e -> e -> e (bound at FD2.hs:22:10)
foldr1 :: (e -> e -> e) -> a -> e (bound at FD2.hs:22:3)
=====================================
testsuite/tests/typecheck/should_fail/T10194.stderr
=====================================
@@ -2,6 +2,5 @@
T10194.hs:7:8: error:
• Cannot instantiate unification variable ‘b0’
with a type involving polytypes: X
- GHC doesn't yet support impredicative polymorphism
• In the expression: (.)
In an equation for ‘comp’: comp = (.)
=====================================
testsuite/tests/typecheck/should_fail/T11514.stderr
=====================================
@@ -2,7 +2,6 @@
T11514.hs:6:7: error:
• Cannot instantiate unification variable ‘a0’
with a type involving polytypes: (Show a => a -> a) -> ()
- GHC doesn't yet support impredicative polymorphism
• In the expression: undefined
In an equation for ‘foo’: foo = undefined
• Relevant bindings include
=====================================
testsuite/tests/typecheck/should_fail/T12563.stderr
=====================================
@@ -2,7 +2,6 @@
T12563.hs:7:15: error:
• Cannot instantiate unification variable ‘p0’
with a type involving polytypes: (forall a. f0 a) -> f0 r0
- GHC doesn't yet support impredicative polymorphism
• In the first argument of ‘foo’, namely ‘g’
In the expression: foo g
In the expression: \ g -> foo g
=====================================
testsuite/tests/typecheck/should_fail/T12589.stderr
=====================================
@@ -5,7 +5,6 @@ T12589.hs:13:5: error:
• Cannot instantiate unification variable ‘t1’
with a type involving polytypes:
(forall a. Bounded a => f0 a) -> h0 f0 xs0
- GHC doesn't yet support impredicative polymorphism
• In the second argument of ‘(&)’, namely ‘hcpure (Proxy @Bounded)’
In the expression: minBound & hcpure (Proxy @Bounded)
In an equation for ‘a’: a = minBound & hcpure (Proxy @Bounded)
=====================================
testsuite/tests/typecheck/should_compile/T18398.hs → testsuite/tests/typecheck/should_fail/T18398.hs
=====================================
=====================================
testsuite/tests/typecheck/should_fail/T18398.stderr
=====================================
@@ -0,0 +1,6 @@
+
+T18398.hs:13:70: error:
+ • No instance for (C Ex p0) arising from a use of ‘meth’
+ • In the expression: meth x z
+ In a case alternative: MkEx _ -> meth x z
+ In the expression: case x of { MkEx _ -> meth x z }
=====================================
testsuite/tests/typecheck/should_compile/T18406.hs → testsuite/tests/typecheck/should_fail/T18406.hs
=====================================
@@ -6,3 +6,10 @@ class C a b | a -> b where
op :: a -> b -> ()
f x = op True x
+
+{- We could accept this, quantifying over a C Bool b constraint. But this is a
+bit silly, actually, because the b is fixed by the fundep. We don't know what
+it's fix to, but it's definitely fixed. So, in the end, we choose not to
+Henry Ford polymorphism ("it works for any b as long as b is ???") and not
+to quantify. Users can quantify manually if they want.
+-}
=====================================
testsuite/tests/typecheck/should_fail/T18406.stderr
=====================================
@@ -0,0 +1,5 @@
+
+T18406.hs:8:7: error:
+ • No instance for (C Bool b0) arising from a use of ‘op’
+ • In the expression: op True x
+ In an equation for ‘f’: f x = op True x
=====================================
testsuite/tests/typecheck/should_fail/all.T
=====================================
@@ -572,3 +572,5 @@ test('FunDepOrigin1b', normal, compile_fail, [''])
test('FD1', normal, compile_fail, [''])
test('FD2', normal, compile_fail, [''])
test('FD3', normal, compile_fail, [''])
+test('T18398', normal, compile_fail, [''])
+test('T18406', normal, compile_fail, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/d57c9cdb2d4d11ecae98c75bb5c5d03abe61374d
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/d57c9cdb2d4d11ecae98c75bb5c5d03abe61374d
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/20200728/936f813f/attachment-0001.html>
More information about the ghc-commits
mailing list