Tweak linearity checker to deal with overloaded names properly

idris-lang · Mar 22, 2013 · 83b7ae5 · 83b7ae5
1 parent 22001e5
commit 83b7ae5
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 2 deletions.
diff --git a/src/Idris/AbsSyntax.hs b/src/Idris/AbsSyntax.hs
@@ -942,14 +942,17 @@ aiFn inpat expat ist fc f as
     find n (g : gs) acc = find n gs (g : acc)
 
 -- replace non-linear occurrences with _
+-- ASSUMPTION: This is called before adding 'alternatives' because otherwise
+-- it is hard to get right!
+
 stripLinear :: IState -> PTerm -> PTerm
 stripLinear i tm = evalState (sl tm) [] where 
     sl :: PTerm -> State [Name] PTerm
     sl (PRef fc f) 
          | (_:_) <- lookupTy Nothing f (tt_ctxt i)
               = return $ PRef fc f
          | otherwise = do ns <- get
-                          trace (show (f, ns)) $ if (f `elem` ns)
+                          if (f `elem` ns)
                              then return Placeholder
                              else do put (f : ns)
                                      return (PRef fc f)

diff --git a/src/Idris/ElabDecls.hs b/src/Idris/ElabDecls.hs
@@ -576,7 +576,7 @@ elabClause info tcgen (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
                          [t] -> t
                          _ -> [] 
         let params = getParamsInType i [] fn_is fn_ty
-        let lhs = stripLinear i $ addImplPat i (propagateParams params lhs_in)
+        let lhs = addImplPat i (propagateParams params (stripLinear i lhs_in))
         logLvl 5 ("LHS: " ++ show fc ++ " " ++ showImp True lhs)
         logLvl 4 ("Fixed parameters: " ++ show params ++ " from " ++ show (fn_ty, fn_is))
         ((lhs', dlhs, []), _) <-