[ fix #55 ] Propagate linear context from Definition to Clauses

Author: fabianhjr

src/TTImp/Elab/Local.idr

@@ -33,17 +33,25 @@ localHelper {vars} nest env nestdecls_in func
     = do est <- get EST
          let f = defining est
          defs <- get Ctxt
-         let vis = case !(lookupCtxtExact (Resolved (defining est)) (gamma defs)) of
-                        Just gdef => visibility gdef
-                        Nothing => Public
+         gdef <- lookupCtxtExact (Resolved (defining est)) (gamma defs)
+         let vis  = maybe Public visibility gdef
+         let mult = maybe linear GlobalDef.multiplicity gdef
+
          -- If the parent function is public, the nested definitions need
          -- to be public too
-         let nestdecls =
+         let nestdeclsVis =
                if vis == Public
                   then map setPublic nestdecls_in
                   else nestdecls_in
 
-         let defNames = definedInBlock emptyNS nestdecls
+         -- If the parent function is erased, then the nested definitions
+         -- will be erased too
+         let nestdeclsMult =
+           if mult == erased
+              then map setErased nestdeclsVis
+              else nestdeclsVis
+
+         let defNames = definedInBlock emptyNS nestdeclsMult
          names' <- traverse (applyEnv f)
                             (nub defNames) -- binding names must be unique
                                            -- fixes bug #115
@@ -60,7 +68,7 @@ localHelper {vars} nest env nestdecls_in func
          -- everything
          let oldhints = localHints defs
 
-         let nestdecls = map (updateName nest') nestdecls
+         let nestdecls = map (updateName nest') nestdeclsMult
          log "elab.def.local" 20 $ show nestdecls
 
          traverse_ (processDecl [] nest' env') nestdecls
@@ -134,6 +142,14 @@ localHelper {vars} nest env nestdecls_in func
         = INamespace fc ps (map setPublic decls)
     setPublic d = d
 
+    setErased : ImpDecl -> ImpDecl
+    setErased (IClaim fc _ v opts ty) = IClaim fc erased v opts ty
+    setErased (IParameters fc ps decls)
+        = IParameters fc ps (map setErased decls)
+    setErased (INamespace fc ps decls)
+        = INamespace fc ps (map setErased decls)
+    setErased d = d
+
 export
 checkLocal : {vars : _} ->
              {auto c : Ref Ctxt Defs} ->

src/TTImp/ProcessDef.idr

@@ -854,6 +854,7 @@ processDef opts nest env fc n_in cs_in
 
          -- Dynamically rebind default totality requirement to this function's totality requirement
          -- and use this requirement when processing `with` blocks
+         log "declare.def" 5 $ "Traversing clauses of " ++ show n ++ " with mult " ++ show mult
          let treq = fromMaybe !getDefaultTotalityOption (findSetTotal (flags gdef))
          cs <- withTotality treq $
                traverse (checkClause mult (visibility gdef) treq

src/TTImp/ProcessType.idr

@@ -19,6 +19,7 @@ import TTImp.TTImp
 import TTImp.Utils
 
 import Data.List
+import Data.Strings
 import Libraries.Data.NameMap
 
 %default covering
@@ -267,7 +268,7 @@ processType {vars} eopts nest env fc rig vis opts (MkImpTy tfc nameFC n_in ty_ra
          addNameLoc nameFC n
 
          log "declare.type" 1 $ "Processing " ++ show n
-         log "declare.type" 5 $ "Checking type decl " ++ show n ++ " : " ++ show ty_raw
+         log "declare.type" 5 $ unwords ["Checking type decl:", show rig, show n, ":", show ty_raw]
          idx <- resolveName n
 
          -- Check 'n' is undefined

src/TTImp/TTImp.idr

@@ -360,7 +360,7 @@ mutual
 
   export
   Show ImpDecl where
-    show (IClaim _ _ _ opts ty) = show opts ++ " " ++ show ty
+    show (IClaim _ c _ opts ty) = show opts ++ " " ++ show c ++ " " ++ show ty
     show (IData _ _ d) = show d
     show (IDef _ n cs) = "(%def " ++ show n ++ " " ++ show cs ++ ")"
     show (IParameters _ ps ds)

tests/Main.idr

@@ -107,7 +107,7 @@ idrisTestsLinear = MkTestPool "Quantities" []
        ["linear001", "linear002", "linear003", -- "linear004" -- disabled due to requiring linearity subtyping
         "linear005", "linear006", "linear007", "linear008",
         "linear009", "linear010", "linear011", "linear012",
-        "linear013"]
+        "linear013", "linear014"]
 
 idrisTestsLiterate : TestPool
 idrisTestsLiterate = MkTestPool "Literate programming" []

tests/idris2/linear014/Issue55.idr

@@ -0,0 +1,16 @@
+0
+foo : (0 b : Bool) -> Bool
+foo b = b
+
+0
+bar : Bool
+bar = q
+  where
+    q : Bool
+    q = foo True
+
+0
+baz : Bool
+baz = let q : Bool
+          q = foo True in
+      q

tests/idris2/linear014/expected

@@ -0,0 +1 @@
+1/1: Building Issue55 (Issue55.idr)

tests/idris2/linear014/run

@@ -0,0 +1,3 @@
+$1 -c Issue55.idr
+
+rm -r build