[Git][ghc/ghc][wip/fabu/T24026-early-reject-type-failing-rules] compiler: Rejects RULES whose LHS immediately fails to type-check

[Fabricio Nascimento (@fabu)]

Fabricio Nascimento pushed to branch wip/fabu/T24026-early-reject-type-failing-rules at Glasgow Haskell Compiler / GHC


Commits:
2d96f436 by Fabricio de Sousa Nascimento at 2024-06-14T11:07:00+09:00
compiler: Rejects RULES whose LHS immediately fails to type-check

Fixes GHC crashing on `decomposeRuleLhs` due to ignoring coercion values. This
happens when we have a RULE that does not type check, and enable
`-fdefer-type-errors`. We prevent this to happen by rejecting RULES with an
immediately LHS type error.

Fixes #24026

- - - - -


7 changed files:

- compiler/GHC/HsToCore/Binds.hs
- compiler/GHC/Tc/Gen/Rule.hs
- + testsuite/tests/typecheck/T24026/T24026a.hs
- + testsuite/tests/typecheck/T24026/T24026a.stderr
- + testsuite/tests/typecheck/T24026/T24026b.hs
- + testsuite/tests/typecheck/T24026/T24026b.stderr
- + testsuite/tests/typecheck/T24026/all.T


Changes:

=====================================
compiler/GHC/HsToCore/Binds.hs
=====================================
@@ -1031,9 +1031,12 @@ decomposeRuleLhs dflags orig_bndrs orig_lhs rhs_fvs
                 extra_bndrs = scopedSort extra_tvs ++ extra_dicts
                   where
                     extra_tvs   = [ v | v <- extra_vars, isTyVar v ]
+
+                -- isEvVar: this includes coercions, matching what
+                --          happens in `split_lets` (isDictId, isCoVar)
                 extra_dicts =
-                  [ mkLocalId (localiseName (idName d)) ManyTy (idType d)
-                  | d <- extra_vars, isDictId d ]
+                  [ mkLocalIdOrCoVar (localiseName (idName d)) ManyTy (idType d)
+                    | d <- extra_vars, isEvVar d ]
                 extra_vars  =
                   [ v
                   | v <- exprsFreeVarsList args


=====================================
compiler/GHC/Tc/Gen/Rule.hs
=====================================
@@ -108,11 +108,13 @@ tcRules decls = mapM (wrapLocMA tcRuleDecls) decls
 tcRuleDecls :: RuleDecls GhcRn -> TcM (RuleDecls GhcTc)
 tcRuleDecls (HsRules { rds_ext = src
                      , rds_rules = decls })
-   = do { tc_decls <- mapM (wrapLocMA tcRule) decls
+   = do { maybe_tc_decls <- mapM (wrapLocMA tcRule) decls
+        ; let tc_decls = [L loc rule | (L loc (Just rule)) <- maybe_tc_decls]
         ; return $ HsRules { rds_ext   = src
                            , rds_rules = tc_decls } }
 
-tcRule :: RuleDecl GhcRn -> TcM (RuleDecl GhcTc)
+
+tcRule :: RuleDecl GhcRn -> TcM (Maybe (RuleDecl GhcTc))
 tcRule (HsRule { rd_ext  = ext
                , rd_name = rname@(L _ name)
                , rd_act  = act
@@ -181,7 +183,16 @@ tcRule (HsRule { rd_ext  = ext
        ; (rhs_implic, rhs_binds) <- buildImplicationFor tc_lvl (getSkolemInfo skol_info) qtkvs
                                          lhs_evs rhs_wanted
        ; emitImplications (lhs_implic `unionBags` rhs_implic)
-       ; return $ HsRule { rd_ext = ext
+
+       -- The error will be reported when lhs_implic is solved. But meanwhile we should drop
+       -- this (ill-typed) rule entirely; with `-fdefer-type-errors`, we will proceed with
+       -- compilation regardless of the error, and an ill-typed LHS 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_tyvs = ty_bndrs -- preserved for ppr-ing


=====================================
testsuite/tests/typecheck/T24026/T24026a.hs
=====================================
@@ -0,0 +1,7 @@
+-- This rule has a type error on the LHS
+module T24026a where
+
+{-# RULES "f" forall (x :: Bool). f x = 0 #-}
+
+f :: Int -> Int
+f x = 0


=====================================
testsuite/tests/typecheck/T24026/T24026a.stderr
=====================================
@@ -0,0 +1,9 @@
+T24026a.hs:4:11: warning: [GHC-95396] [-Winline-rule-shadowing (in -Wdefault)]
+    Rule "f" may never fire because ‘f’ might inline first
+    Suggested fix: Add an INLINE[n] or NOINLINE[n] pragma for ‘f’
+
+T24026a.hs:4:37: warning: [GHC-83865] [-Wdeferred-type-errors (in -Wdefault)]
+    • Couldn't match expected type ‘Int’ with actual type ‘Bool’
+    • In the first argument of ‘f’, namely ‘x’
+      In the expression: f x
+      When checking the rewrite rule "f"
\ No newline at end of file


=====================================
testsuite/tests/typecheck/T24026/T24026b.hs
=====================================
@@ -0,0 +1,7 @@
+-- This rule has a type error on the LHS
+module T24026b where
+
+{-# RULES "f" forall (x :: Bool). f x = 0 #-}
+
+f :: Int -> Int
+f x = 0


=====================================
testsuite/tests/typecheck/T24026/T24026b.stderr
=====================================
@@ -0,0 +1,5 @@
+T24026b.hs:4:37: error: [GHC-83865]
+    • Couldn't match expected type ‘Int’ with actual type ‘Bool’
+    • In the first argument of ‘f’, namely ‘x’
+      In the expression: f x
+      When checking the rewrite rule "f"
\ No newline at end of file


=====================================
testsuite/tests/typecheck/T24026/all.T
=====================================
@@ -0,0 +1,2 @@
+test('T24026a', normal, compile, ['-dlint -fdefer-type-errors'])
+test('T24026b', normal, compile_fail, [''])
\ No newline at end of file



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/2d96f436ab6e4f4ab20f29054cbf2c8553039e59

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/2d96f436ab6e4f4ab20f29054cbf2c8553039e59
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/20240613/fd784ab2/attachment-0001.html>