[Git][ghc/ghc][wip/T24359] Improve matters wrt equalities in specialisation

Simon Peyton Jones (@simonpj) gitlab at gitlab.haskell.org
Mon Nov 18 17:44:18 UTC 2024



Simon Peyton Jones pushed to branch wip/T24359 at Glasgow Haskell Compiler / GHC


Commits:
065de8c9 by Simon Peyton Jones at 2024-11-18T17:43:55+00:00
Improve matters wrt equalities in specialisation

- - - - -


2 changed files:

- compiler/GHC/HsToCore/Binds.hs
- compiler/GHC/Tc/Gen/Sig.hs


Changes:

=====================================
compiler/GHC/HsToCore/Binds.hs
=====================================
@@ -847,8 +847,8 @@ dsSpec mb_poly_rhs (SpecPragE { spe_poly_id = poly_id
 
        ; mk_spec_call <- do { ds_call <- dsLExpr the_call
                             ; return $ \ poly_id poly_rhs ->
-                                  mkLets ds_lhs_binds  $
                                   mkLets ds_rhs_binds  $
+                                  mkLets ds_lhs_binds  $
                                   mkLetNonRec (localiseId poly_id) poly_rhs $
                                   ds_call }
 


=====================================
compiler/GHC/Tc/Gen/Sig.hs
=====================================
@@ -923,21 +923,25 @@ tcSpecPrag poly_id (SpecSigE nm bndrs spec_e inl)
        -- Quantify
        ; let (quant_cts, residual_wanted) = getRuleQuantCts wanted
              quant_preds = ctsPreds quant_cts
+             (quant_eq_cts, quant_dict_cts) = partitionBag (isEqPred . ctPred) quant_cts
        ; dvs <- candidateQTyVarsOfTypes (quant_preds ++ seed_tys)
        ; let grown_tcvs = growThetaTyVars quant_preds (tyCoVarsOfTypes seed_tys)
              weeded_dvs = weedOutCandidates (`dVarSetIntersectVarSet` grown_tcvs) dvs
        ; qtkvs <- quantifyTyVars skol_info DefaultNonStandardTyVars weeded_dvs
 
        -- Left hand side of the RULE
-       ; lhs_evs <- mk_quant_evs quant_cts
+       ; lhs_eq_evs   <- mk_quant_evs quant_eq_cts
+       ; lhs_dict_evs <- mk_quant_evs quant_dict_cts
+       ; let lhs_evs = lhs_eq_evs ++ lhs_dict_evs
        ; (implic1, lhs_binds) <- buildImplicationFor tc_lvl skol_info_anon
                                                      qtkvs lhs_evs residual_wanted
 
        -- rhs_binds uses rhs_evs to build `wanted` (NB not just `residual_wanted`)
-       ; rhs_evs <- mapM newEvVar quant_preds
+       ; rhs_dict_evs <- mapM newEvVar (ctsPreds quant_dict_cts)
+       ; let rhs_evs = lhs_eq_evs ++ rhs_dict_evs
        ; (implic2, rhs_binds) <- buildImplicationFor tc_lvl skol_info_anon
                                                      qtkvs rhs_evs
-                                                     (emptyWC { wc_simple = quant_cts })
+                                                     (emptyWC { wc_simple = quant_dict_cts })
 
        ; emitImplications (implic1 `unionBags` implic2)
 
@@ -1187,21 +1191,12 @@ tcRule (HsRule { rd_ext  = ext
                                          lhs_evs rhs_wanted
        ; emitImplications (lhs_implic `unionBags` rhs_implic)
 
-       -- A type error on the LHS of a rule will be reported earlier while solving for
-       -- lhs_implic. However, we should also drop the rule entirely for cases where
-       -- compilation continues regardless of the error. For example with
-       -- `-fdefer-type-errors`, where this ill-typed LHS rule may cause follow-on errors
-       -- (#24026).
-       ; if anyBag insolubleImplic lhs_implic
-        then
-          return Nothing -- The RULE LHS does not type-check and will be dropped.
-        else
-          return . Just $ HsRule { rd_ext   = ext
-                                 , rd_name  = rname
-                                 , rd_act   = act
-                                 , rd_bndrs = mkTcRuleBndrs bndrs (qtkvs ++ tpl_ids)
-                                 , rd_lhs   = mkHsDictLet lhs_binds lhs'
-                                 , rd_rhs   = mkHsDictLet rhs_binds rhs' } }
+       ; return $ Just $ HsRule { rd_ext   = ext
+                                , rd_name  = rname
+                                , rd_act   = act
+                                , rd_bndrs = mkTcRuleBndrs bndrs (qtkvs ++ tpl_ids)
+                                , rd_lhs   = mkHsDictLet lhs_binds lhs'
+                                , rd_rhs   = mkHsDictLet rhs_binds rhs' } }
   where
     mkTcRuleBndrs (RuleBndrs { rb_tyvs = tyvs }) vars
       = RuleBndrs { rb_ext = noAnn
@@ -1509,9 +1504,8 @@ getRuleQuantCts wc
       = ( simple_yes `andCts` implic_yes
         , emptyWC { wc_simple = simple_no, wc_impl = implics_no, wc_errors = errs })
      where
-        (simple_yes, simple_no) = partitionBag (rule_quant_ct skol_tvs) simples
-        (implic_yes, implics_no) = mapAccumBagL (float_implic skol_tvs)
-                                                emptyBag implics
+        (simple_yes, simple_no)  = partitionBag (rule_quant_ct skol_tvs) simples
+        (implic_yes, implics_no) = mapAccumBagL (float_implic skol_tvs)  emptyBag implics
 
     float_implic :: TcTyCoVarSet -> Cts -> Implication -> (Cts, Implication)
     float_implic skol_tvs yes1 imp
@@ -1521,17 +1515,23 @@ getRuleQuantCts wc
         new_skol_tvs = skol_tvs `extendVarSetList` ic_skols imp
 
     rule_quant_ct :: TcTyCoVarSet -> Ct -> Bool
-    rule_quant_ct skol_tvs ct = case classifyPredType (ctPred ct) of
-      EqPred _ t1 t2
-        | not (ok_eq t1 t2)
-        -> False        -- Note [RULE quantification over equalities]
-      _ -> tyCoVarsOfCt ct `disjointVarSet` skol_tvs
+    rule_quant_ct skol_tvs ct
+      | insolubleWantedCt ct
+      = False
+      | otherwise
+      = case classifyPredType (ctPred ct) of
+           EqPred _ t1 t2
+             | not (ok_eq t1 t2)
+             -> False        -- Note [RULE quantification over equalities]
+           _ -> tyCoVarsOfCt ct `disjointVarSet` skol_tvs
 
     ok_eq t1 t2
-       | t1 `tcEqType` t2 = False
-       | otherwise        = is_fun_app t1 || is_fun_app t2
+       | t1 `tcEqType` t2 = False  -- Our solving step may have turned it into Refl
+       | otherwise        = True
 
-    is_fun_app ty   -- ty is of form (F tys) where F is a type function
-      = case tyConAppTyCon_maybe ty of
-          Just tc -> isTypeFamilyTyCon tc
-          Nothing -> False
+--         is_fun_app t1 || is_fun_app t2
+--
+--    is_fun_app ty   -- ty is of form (F tys) where F is a type function
+--      = case tyConAppTyCon_maybe ty of
+--          Just tc -> isTypeFamilyTyCon tc
+--          Nothing -> False



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/065de8c9775826b335ba0c6d0f56f5395afdd625

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/065de8c9775826b335ba0c6d0f56f5395afdd625
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/20241118/a50de4b5/attachment-0001.html>


More information about the ghc-commits mailing list