[Git][ghc/ghc][wip/derived-refactor] Float fundep constraints
Richard Eisenberg
gitlab at gitlab.haskell.org
Fri Jun 26 10:21:01 UTC 2020
Richard Eisenberg pushed to branch wip/derived-refactor at Glasgow Haskell Compiler / GHC
Commits:
a7074a72 by Richard Eisenberg at 2020-06-26T11:20:36+01:00
Float fundep constraints
- - - - -
8 changed files:
- compiler/GHC/Tc/Errors.hs
- compiler/GHC/Tc/Solver.hs
- compiler/GHC/Tc/Solver/Canonical.hs
- compiler/GHC/Tc/Types/Constraint.hs
- compiler/GHC/Tc/Types/Origin.hs
- compiler/GHC/Tc/Utils/Unify.hs
- + testsuite/tests/typecheck/should_compile/FloatFDs.hs
- testsuite/tests/typecheck/should_compile/all.T
Changes:
=====================================
compiler/GHC/Tc/Errors.hs
=====================================
@@ -548,8 +548,9 @@ instance Outputable ErrorItem where
pp_supp = if supp then text "suppress:" else empty
--- | Makes an error item based on the predicate-at-birth of the provided
--- constraint. This should be rewritten w.r.t. givens before reported.
+-- | Makes an error item from a constraint, calculating whether or not
+-- the item should be suppressed. See Note [Wanteds rewrite Wanteds]
+-- in GHC.Tc.Types.Constraint
mkErrorItem :: Ct -> TcM ErrorItem
mkErrorItem ct
= do { let loc = ctLoc ct
@@ -3168,9 +3169,12 @@ warnDefaulting :: [Ct] -> Type -> TcM ()
warnDefaulting wanteds default_ty
= do { warn_default <- woptM Opt_WarnTypeDefaults
; env0 <- tcInitTidyEnv
- ; let tidy_env = tidyFreeTyCoVars env0 $
- tyCoVarsOfCtsList (listToBag wanteds)
- tidy_wanteds = map (tidyCt tidy_env) wanteds
+ -- don't want to report all the superclass constraints, which
+ -- add unhelpful clutter
+ ; let filtered = filter (not . is_wanted_superclass . ctOrigin) wanteds
+ tidy_env = tidyFreeTyCoVars env0 $
+ tyCoVarsOfCtsList (listToBag filtered)
+ tidy_wanteds = map (tidyCt tidy_env) filtered
(loc, ppr_wanteds) = pprWithArising tidy_wanteds
warn_msg =
hang (hsep [ text "Defaulting the following"
@@ -3180,6 +3184,9 @@ warnDefaulting wanteds default_ty
2
ppr_wanteds
; setCtLocM loc $ warnTc (Reason Opt_WarnTypeDefaults) warn_default warn_msg }
+ where
+ is_wanted_superclass (WantedSuperclassOrigin {}) = True
+ is_wanted_superclass _ = False
{-
Note [Runtime skolems]
=====================================
compiler/GHC/Tc/Solver.hs
=====================================
@@ -29,7 +29,7 @@ module GHC.Tc.Solver(
import GHC.Prelude
import GHC.Data.Bag
-import GHC.Core.Class ( Class, classKey, classTyCon )
+import GHC.Core.Class ( Class, classKey, classTyCon, classHasFds )
import GHC.Driver.Session
import GHC.Types.Id ( idType )
import GHC.Tc.Utils.Instantiate
@@ -1655,7 +1655,7 @@ solveImplication imp@(Implic { ic_tclvl = tclvl
; residual_wanted <- solveWanteds wanteds
-- solveWanteds, *not* solveWantedsAndDrop, because
-- we want to retain derived equalities so we can float
- -- them out in floatEqualities
+ -- them out in floatConstraints
; (no_eqs, given_insols) <- getNoGivenEqs tclvl skols
-- Call getNoGivenEqs /after/ solveWanteds, because
@@ -1665,8 +1665,8 @@ solveImplication imp@(Implic { ic_tclvl = tclvl
; return (no_eqs, given_insols, residual_wanted) }
; (floated_eqs, residual_wanted)
- <- floatEqualities skols given_ids ev_binds_var
- no_given_eqs residual_wanted
+ <- floatConstraints skols given_ids ev_binds_var
+ no_given_eqs residual_wanted
; traceTcS "solveImplication 2"
(ppr given_insols $$ ppr residual_wanted)
@@ -2288,10 +2288,10 @@ beta! Concrete example is in indexed_types/should_fail/ExtraTcsUntch.hs:
* *
*********************************************************************************
-Note [Float Equalities out of Implications]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Note [Float constraints out of implications]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
For ordinary pattern matches (including existentials) we float
-equalities out of implications, for instance:
+constraints out of implications, for instance:
data T where
MkT :: Eq a => a -> T
f x y = case x of MkT _ -> (y::Int)
@@ -2300,7 +2300,7 @@ We get the implication constraint (x::T) (y::alpha):
We want to float out the equality into a scope where alpha is no
longer untouchable, to solve the implication!
-But we cannot float equalities out of implications whose givens may
+But we cannot float constraints out of implications whose givens may
yield or contain equalities:
data T a where
@@ -2326,7 +2326,7 @@ But if we just leave them inside the implications, we unify alpha := beta and
solve everything.
Principle:
- We do not want to float equalities out which may
+ We do not want to float constraints out which may
need the given *evidence* to become soluble.
Consequence: classes with functional dependencies don't matter (since there is
@@ -2334,10 +2334,10 @@ no evidence for a fundep equality), but equality superclasses do matter (since
they carry evidence).
-}
-floatEqualities :: [TcTyVar] -> [EvId] -> EvBindsVar -> Bool
- -> WantedConstraints
- -> TcS (Cts, WantedConstraints)
--- Main idea: see Note [Float Equalities out of Implications]
+floatConstraints :: [TcTyVar] -> [EvId] -> EvBindsVar -> Bool
+ -> WantedConstraints
+ -> TcS (Cts, WantedConstraints)
+-- Main idea: see Note [Float constraints out of implications]
--
-- Precondition: the wc_simple of the incoming WantedConstraints are
-- fully zonked, so that we can see their free variables
@@ -2352,10 +2352,10 @@ floatEqualities :: [TcTyVar] -> [EvId] -> EvBindsVar -> Bool
-- Subtleties: Note [Float equalities from under a skolem binding]
-- Note [Skolem escape]
-- Note [What prevents a constraint from floating]
-floatEqualities skols given_ids ev_binds_var no_given_eqs
- wanteds@(WC { wc_simple = simples })
+floatConstraints skols given_ids ev_binds_var no_given_eqs
+ wanteds@(WC { wc_simple = simples })
| not no_given_eqs -- There are some given equalities, so don't float
- = return (emptyBag, wanteds) -- Note [Float Equalities out of Implications]
+ = return (emptyBag, wanteds) -- Note [Float constraints out of implications]
| otherwise
= do { -- First zonk: the inert set (from whence they came) is fully
@@ -2367,7 +2367,7 @@ floatEqualities skols given_ids ev_binds_var no_given_eqs
-- Now we can pick the ones to float
-- The constraints are un-flattened and de-canonicalised
- ; let (candidate_eqs, no_float_cts) = partitionBag is_float_eq_candidate simples
+ ; let (candidates, no_float_cts) = partitionBag is_float_candidate simples
seed_skols = mkVarSet skols `unionVarSet`
mkVarSet given_ids `unionVarSet`
@@ -2376,25 +2376,25 @@ floatEqualities skols given_ids ev_binds_var no_given_eqs
-- seed_skols: See Note [What prevents a constraint from floating] (1,2,3)
-- Include the EvIds of any non-floating constraints
- extended_skols = transCloVarSet (add_captured_ev_ids candidate_eqs) seed_skols
+ extended_skols = transCloVarSet (add_captured_ev_ids candidates) seed_skols
-- extended_skols contains the EvIds of all the trapped constraints
-- See Note [What prevents a constraint from floating] (3)
- (flt_eqs, no_flt_eqs) = partitionBag (is_floatable extended_skols)
- candidate_eqs
+ (flts, no_flts) = partitionBag (is_floatable extended_skols)
+ candidates
- remaining_simples = no_float_cts `andCts` no_flt_eqs
+ remaining_simples = no_float_cts `andCts` no_flts
-- Promote any unification variables mentioned in the floated equalities
-- See Note [Promoting unification variables]
- ; mapM_ promoteTyVarTcS (tyCoVarsOfCtsList flt_eqs)
+ ; mapM_ promoteTyVarTcS (tyCoVarsOfCtsList flts)
- ; traceTcS "floatEqualities" (vcat [ text "Skols =" <+> ppr skols
- , text "Extended skols =" <+> ppr extended_skols
- , text "Simples =" <+> ppr simples
- , text "Candidate eqs =" <+> ppr candidate_eqs
- , text "Floated eqs =" <+> ppr flt_eqs])
- ; return ( flt_eqs, wanteds { wc_simple = remaining_simples } ) }
+ ; traceTcS "floatConstraints" (vcat [ text "Skols =" <+> ppr skols
+ , text "Extended skols =" <+> ppr extended_skols
+ , text "Simples =" <+> ppr simples
+ , text "Candidate cts =" <+> ppr candidates
+ , text "Floated cts =" <+> ppr flts ])
+ ; return ( flts, wanteds { wc_simple = remaining_simples } ) }
where
add_one_bind :: EvBind -> VarSet -> VarSet
@@ -2417,25 +2417,26 @@ floatEqualities skols given_ids ev_binds_var no_given_eqs
| tyCoVarsOfCt ct `intersectsVarSet` skols = extendVarSet acc (ctEvId ct)
| otherwise = acc
- -- Identify which equalities are candidates for floating
+ -- Identify which constraints are candidates for floating
-- Float out alpha ~ ty, or ty ~ alpha which might be unified outside
- -- See Note [Which equalities to float]
- is_float_eq_candidate ct
- | pred <- ctPred ct
- , EqPred NomEq ty1 ty2 <- classifyPredType pred
- = case (tcGetTyVar_maybe ty1, tcGetTyVar_maybe ty2) of
+ -- Also float out class constraints with functional dependencies
+ -- See Note [Which constraints to float]
+ is_float_candidate ct = case classifyPredType (ctPred ct) of
+ EqPred NomEq ty1 ty2 ->
+ case (tcGetTyVar_maybe ty1, tcGetTyVar_maybe ty2) of
(Just tv1, _) -> float_tv_eq_candidate tv1 ty2
(_, Just tv2) -> float_tv_eq_candidate tv2 ty1
_ -> False
- | otherwise = False
+ ClassPred cls _ -> classHasFds cls
+ _ -> False
- float_tv_eq_candidate tv1 ty2 -- See Note [Which equalities to float]
+ float_tv_eq_candidate tv1 ty2 -- See Note [Which constraints to float]
= isMetaTyVar tv1
&& (not (isTyVarTyVar tv1) || isTyVarTy ty2)
{- Note [Float equalities from under a skolem binding]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Which of the simple equalities can we float out? Obviously, only
ones that don't mention the skolem-bound variables. But that is
over-eager. Consider
@@ -2457,11 +2458,13 @@ We had a very complicated rule previously, but this is nice and
simple. (To see the notes, look at this Note in a version of
GHC.Tc.Solver prior to Oct 2014).
-Note [Which equalities to float]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Which equalities should we float? We want to float ones where there
+Note [Which constraints to float]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Which constraints should we float? We want to float ones where there
is a decent chance that floating outwards will allow unification to
-happen. In particular, float out equalities that are:
+happen.
+
+1. Float out equalities that are:
* Of form (alpha ~# ty) or (ty ~# alpha), where
* alpha is a meta-tyvar.
@@ -2473,6 +2476,18 @@ happen. In particular, float out equalities that are:
unify representational equalities even if alpha is touchable.
See Note [Do not unify representational equalities] in GHC.Tc.Solver.Interact.
+2. Float out class constraints with functional dependencies. Example:
+
+ class C a b | a -> b
+
+ forall [1]. C a[sk] beta1[tau]
+ forall [1]. C a[sk] beta2[tau]
+
+We want the two class constraints to interact, so that we can unify beta1 := beta2.
+But since they are in separate implications, they won't find each other. Thus: float.
+
+This is tested in test case typecheck/should_compile/FloatFDs.
+
Note [Skolem escape]
~~~~~~~~~~~~~~~~~~~~
You might worry about skolem escape with all this floating.
=====================================
compiler/GHC/Tc/Solver/Canonical.hs
=====================================
@@ -595,7 +595,7 @@ mk_strict_superclasses rec_clss ev tvs theta cls tys
= ASSERT2( null tvs && null theta, ppr tvs $$ ppr theta )
concatMapM do_one_derived (immSuperClasses cls tys)
where
- loc = ctEvLoc ev
+ loc = ctEvLoc ev `updateCtLocOrigin` WantedSuperclassOrigin (ctEvPred ev)
do_one_derived sc_pred
= do { sc_ev <- newDerivedNC loc (ctEvRewriters ev) sc_pred
=====================================
compiler/GHC/Tc/Types/Constraint.hs
=====================================
@@ -1300,7 +1300,7 @@ untouchables, and therefore cannot be unified with anything at all,
let alone the skolems.
Instead, ic_skols is used only when considering floating a constraint
-outside the implication in GHC.Tc.Solver.floatEqualities or
+outside the implication in GHC.Tc.Solver.floatConstraints or
GHC.Tc.Solver.approximateImplications
Note [Insoluble constraints]
=====================================
compiler/GHC/Tc/Types/Origin.hs
=====================================
@@ -441,6 +441,11 @@ data CtOrigin
| InstProvidedOrigin Module ClsInst
-- Skolem variable arose when we were testing if an instance
-- is solvable or not.
+ | WantedSuperclassOrigin PredType CtOrigin
+ -- From expanding out the superclasses of a Wanted; the PredType
+ -- is the subclass predicate, and the origin
+ -- of the original Wanted is the CtOrigin
+
-- An origin is visible if the place where the constraint arises is manifest
-- in user code. Currently, all origins are visible except for invisible
-- TypeEqOrigins. This is used when choosing which error of
@@ -540,7 +545,6 @@ lGRHSCtOrigin _ = Shouldn'tHappenOrigin "multi-way GRHS"
pprCtOrigin :: CtOrigin -> SDoc
-- "arising from ..."
--- Not an instance of Outputable because of the "arising from" prefix
pprCtOrigin (GivenOrigin sk) = ctoHerald <+> ppr sk
pprCtOrigin (SpecPragOrigin ctxt)
@@ -615,6 +619,10 @@ pprCtOrigin (InstProvidedOrigin mod cls_inst)
, ppr cls_inst
, text "is provided by" <+> quotes (ppr mod)]
+pprCtOrigin (WantedSuperclassOrigin subclass_pred subclass_orig)
+ = sep [ ctoHerald <+> text "a superclass required to satisfy" <+> quotes (ppr subclass_pred) <> comma
+ , pprCtOrigin subclass_orig ]
+
pprCtOrigin simple_origin
= ctoHerald <+> pprCtO simple_origin
=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -1756,7 +1756,7 @@ So we look for a positive reason to swap, using a three-step test:
Generally speaking we always try to put a MetaTv on the left
in preference to SkolemTv or RuntimeUnkTv:
a) Because the MetaTv may be touchable and can be unified
- b) Even if it's not touchable, GHC.Tc.Solver.floatEqualities
+ b) Even if it's not touchable, GHC.Tc.Solver.floatConstraints
looks for meta tyvars on the left
Tie-breaking rules for MetaTvs:
=====================================
testsuite/tests/typecheck/should_compile/FloatFDs.hs
=====================================
@@ -0,0 +1,180 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE Safe #-}
+
+-----------------------------------------------------------------------------
+-- |
+-- Module : Text.Parsec.Expr
+-- Copyright : (c) Daan Leijen 1999-2001, (c) Paolo Martini 2007
+-- License : BSD-style (see the LICENSE file)
+--
+-- Maintainer : derek.a.elkins at gmail.com
+-- Stability : provisional
+-- Portability : non-portable
+--
+-- A helper module to parse \"expressions\".
+-- Builds a parser given a table of operators and associativities.
+--
+-----------------------------------------------------------------------------
+
+module Text.Parsec.Expr
+ ( Assoc(..), Operator(..), OperatorTable
+ , buildExpressionParser
+ ) where
+
+import Data.Typeable ( Typeable )
+
+import Text.Parsec.Prim
+import Text.Parsec.Combinator
+
+-----------------------------------------------------------
+-- Assoc and OperatorTable
+-----------------------------------------------------------
+
+-- | This data type specifies the associativity of operators: left, right
+-- or none.
+
+data Assoc = AssocNone
+ | AssocLeft
+ | AssocRight
+ deriving ( Typeable )
+
+-- | This data type specifies operators that work on values of type @a at .
+-- An operator is either binary infix or unary prefix or postfix. A
+-- binary operator has also an associated associativity.
+
+data Operator s u m a = Infix (ParsecT s u m (a -> a -> a)) Assoc
+ | Prefix (ParsecT s u m (a -> a))
+ | Postfix (ParsecT s u m (a -> a))
+#if MIN_VERSION_base(4,7,0)
+ deriving ( Typeable )
+#endif
+
+-- | An @OperatorTable s u m a@ is a list of @Operator s u m a@
+-- lists. The list is ordered in descending
+-- precedence. All operators in one list have the same precedence (but
+-- may have a different associativity).
+
+type OperatorTable s u m a = [[Operator s u m a]]
+
+-----------------------------------------------------------
+-- Convert an OperatorTable and basic term parser into
+-- a full fledged expression parser
+-----------------------------------------------------------
+
+-- | @buildExpressionParser table term@ builds an expression parser for
+-- terms @term@ with operators from @table@, taking the associativity
+-- and precedence specified in @table@ into account. Prefix and postfix
+-- operators of the same precedence can only occur once (i.e. @--2@ is
+-- not allowed if @-@ is prefix negate). Prefix and postfix operators
+-- of the same precedence associate to the left (i.e. if @++@ is
+-- postfix increment, than @-2++@ equals @-1@, not @-3@).
+--
+-- The @buildExpressionParser@ takes care of all the complexity
+-- involved in building expression parser. Here is an example of an
+-- expression parser that handles prefix signs, postfix increment and
+-- basic arithmetic.
+--
+-- > expr = buildExpressionParser table term
+-- > <?> "expression"
+-- >
+-- > term = parens expr
+-- > <|> natural
+-- > <?> "simple expression"
+-- >
+-- > table = [ [prefix "-" negate, prefix "+" id ]
+-- > , [postfix "++" (+1)]
+-- > , [binary "*" (*) AssocLeft, binary "/" (div) AssocLeft ]
+-- > , [binary "+" (+) AssocLeft, binary "-" (-) AssocLeft ]
+-- > ]
+-- >
+-- > binary name fun assoc = Infix (do{ reservedOp name; return fun }) assoc
+-- > prefix name fun = Prefix (do{ reservedOp name; return fun })
+-- > postfix name fun = Postfix (do{ reservedOp name; return fun })
+
+buildExpressionParser :: (Stream s m t)
+ => OperatorTable s u m a
+ -> ParsecT s u m a
+ -> ParsecT s u m a
+{-# INLINABLE buildExpressionParser #-}
+buildExpressionParser operators simpleExpr
+ = foldl (makeParser) simpleExpr operators
+ where
+-- makeParser :: Stream s m t => ParsecT s u m a -> [Operator s u m a] -> ParsecT s u m a
+-- uncommenting this avoids the original problem, but we want to compile even
+-- without offering this hint
+ makeParser term ops
+ = let (rassoc,lassoc,nassoc
+ ,prefix,postfix) = foldr splitOp ([],[],[],[],[]) ops
+
+ rassocOp = choice rassoc
+ lassocOp = choice lassoc
+ nassocOp = choice nassoc
+ prefixOp = choice prefix <?> ""
+ postfixOp = choice postfix <?> ""
+
+ ambiguous assoc op= try $
+ do{ _ <- op; fail ("ambiguous use of a " ++ assoc
+ ++ " associative operator")
+ }
+
+ ambiguousRight = ambiguous "right" rassocOp
+ ambiguousLeft = ambiguous "left" lassocOp
+ ambiguousNon = ambiguous "non" nassocOp
+
+ termP = do{ pre <- prefixP
+ ; x <- term
+ ; post <- postfixP
+ ; return (post (pre x))
+ }
+
+ postfixP = postfixOp <|> return id
+
+ prefixP = prefixOp <|> return id
+
+ rassocP x = do{ f <- rassocOp
+ ; y <- do{ z <- termP; rassocP1 z }
+ ; return (f x y)
+ }
+ <|> ambiguousLeft
+ <|> ambiguousNon
+ -- <|> return x
+
+ rassocP1 x = rassocP x <|> return x
+
+ lassocP x = do{ f <- lassocOp
+ ; y <- termP
+ ; lassocP1 (f x y)
+ }
+ <|> ambiguousRight
+ <|> ambiguousNon
+ -- <|> return x
+
+ lassocP1 x = lassocP x <|> return x
+
+ nassocP x = do{ f <- nassocOp
+ ; y <- termP
+ ; ambiguousRight
+ <|> ambiguousLeft
+ <|> ambiguousNon
+ <|> return (f x y)
+ }
+ -- <|> return x
+
+ in do{ x <- termP
+ ; rassocP x <|> lassocP x <|> nassocP x <|> return x
+ <?> "operator"
+ }
+
+
+ splitOp (Infix op assoc) (rassoc,lassoc,nassoc,prefix,postfix)
+ = case assoc of
+ AssocNone -> (rassoc,lassoc,op:nassoc,prefix,postfix)
+ AssocLeft -> (rassoc,op:lassoc,nassoc,prefix,postfix)
+ AssocRight -> (op:rassoc,lassoc,nassoc,prefix,postfix)
+
+ splitOp (Prefix op) (rassoc,lassoc,nassoc,prefix,postfix)
+ = (rassoc,lassoc,nassoc,op:prefix,postfix)
+
+ splitOp (Postfix op) (rassoc,lassoc,nassoc,prefix,postfix)
+ = (rassoc,lassoc,nassoc,prefix,op:postfix)
=====================================
testsuite/tests/typecheck/should_compile/all.T
=====================================
@@ -703,3 +703,4 @@ test('T18023', normal, compile, [''])
test('T18036', normal, compile, [''])
test('T18036a', normal, compile, [''])
test('FunDepOrigin1', normal, compile, [''])
+test('FloatFDs', normal, compile, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/a7074a72e6bcad81bd8822749e6967098c54e878
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/a7074a72e6bcad81bd8822749e6967098c54e878
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/20200626/c8db92b2/attachment-0001.html>
More information about the ghc-commits
mailing list