[Git][ghc/ghc][wip/infer-mult-more] Make 'undefined x' linear in 'x' (#18731)

[Krzysztof Gogolewski]

Krzysztof Gogolewski pushed to branch wip/infer-mult-more at Glasgow Haskell Compiler / GHC


Commits:
83047a10 by Krzysztof Gogolewski at 2020-09-21T18:09:03+02:00
Make 'undefined x' linear in 'x' (#18731)

- - - - -


5 changed files:

- compiler/GHC/Tc/Utils/Unify.hs
- testsuite/tests/dependent/should_compile/dynamic-paper.stderr
- + testsuite/tests/linear/should_compile/T18731.hs
- testsuite/tests/linear/should_compile/all.T
- testsuite/tests/typecheck/should_fail/T7869.stderr


Changes:

=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -340,9 +340,12 @@ matchActualFunTySigma herald ct_orig mb_thing err_info fun_ty
     defer fun_ty
       = do { arg_ty <- newOpenFlexiTyVarTy
            ; res_ty <- newOpenFlexiTyVarTy
-           ; let unif_fun_ty = mkVisFunTyMany arg_ty res_ty
+           ; mult  <- newFlexiTyVarTy multiplicityTy
+             -- We need a new variable for multiplicity (#18731)
+             -- Otherwise, 'undefined x' wouldn't be linear in x
+           ; let unif_fun_ty = mkVisFunTy mult arg_ty res_ty
            ; co <- unifyType mb_thing fun_ty unif_fun_ty
-           ; return (mkWpCastN co, unrestricted arg_ty, res_ty) }
+           ; return (mkWpCastN co, Scaled mult arg_ty, res_ty) }
 
     ------------
     mk_ctxt :: TcType -> TidyEnv -> TcM (TidyEnv, MsgDoc)


=====================================
testsuite/tests/dependent/should_compile/dynamic-paper.stderr
=====================================
@@ -12,4 +12,4 @@ Simplifier ticks exhausted
   simplifier non-termination has been judged acceptable.
    
   To see detailed counts use -ddump-simpl-stats
-  Total ticks: 136961
+  Total ticks: 140801


=====================================
testsuite/tests/linear/should_compile/T18731.hs
=====================================
@@ -0,0 +1,5 @@
+{-# LANGUAGE LinearTypes #-}
+module T18731 where
+
+f :: a #-> b
+f x = undefined x


=====================================
testsuite/tests/linear/should_compile/all.T
=====================================
@@ -35,3 +35,4 @@ test('MultConstructor', expect_broken(broken_multiplicity_syntax), compile, ['']
 test('LinearLetRec', expect_broken(405), compile, ['-O -dlinear-core-lint'])
 test('LinearTH1', normal, compile, [''])
 test('LinearTH2', expect_broken(broken_multiplicity_syntax), compile, [''])
+test('T18731', normal, compile, [''])


=====================================
testsuite/tests/typecheck/should_fail/T7869.stderr
=====================================
@@ -1,16 +1,18 @@
 
 T7869.hs:3:12: error:
-    • Couldn't match type ‘b1’ with ‘b’
+    • Couldn't match type ‘a1’ with ‘a’
       Expected: [a1] -> b1
         Actual: [a] -> b
-      ‘b1’ is a rigid type variable bound by
+      ‘a1’ is a rigid type variable bound by
         an expression type signature:
           forall a1 b1. [a1] -> b1
         at T7869.hs:3:20-27
-      ‘b’ is a rigid type variable bound by
+      ‘a’ is a rigid type variable bound by
         the inferred type of f :: [a] -> b
         at T7869.hs:3:1-27
     • In the expression: f x
       In the expression: (\ x -> f x) :: [a] -> b
       In an equation for ‘f’: f = (\ x -> f x) :: [a] -> b
-    • Relevant bindings include f :: [a] -> b (bound at T7869.hs:3:1)
+    • Relevant bindings include
+        x :: [a1] (bound at T7869.hs:3:7)
+        f :: [a] -> b (bound at T7869.hs:3:1)



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/83047a104850ff77e076bc66e6127015dfdd5f00

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/83047a104850ff77e076bc66e6127015dfdd5f00
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/20200921/03353986/attachment-0001.html>