Update type on delayed rewrite

Like in delayed ambiguity resolution, we need to reevaluate the target
type because it might have changed - and that's why we delayed in the
first place!

libs/base/Data/Strings.idr

@@ -72,3 +72,6 @@ public export
 break : (Char -> Bool) -> String -> (String, String)
 break p = span (not . p)
 
+export
+stringToNatOrZ : String -> Nat
+stringToNatOrZ = fromInteger . prim__cast_StringInteger

libs/base/Data/Vect.idr

@@ -807,13 +807,13 @@ exactLength {m} len xs with (decEq m len)
 ||| at least that length in its type, otherwise return Nothing
 ||| @len the required length
 ||| @xs the vector with the desired length
--- overLength : {m : Nat} -> -- expected at run-time
+overLength : {m : Nat} -> -- expected at run-time
---              (len : Nat) -> (xs : Vect m a) -> Maybe (p ** Vect (plus p len) a)
+             (len : Nat) -> (xs : Vect m a) -> Maybe (p ** Vect (plus p len) a)
--- overLength {m} n xs with (cmp m n)
+overLength {m} n xs with (cmp m n)
---   overLength {m = m} (plus m (S y)) xs | (CmpLT y) = Nothing
+  overLength {m = m} (plus m (S y)) xs | (CmpLT y) = Nothing
---   overLength {m = m} m xs | CmpEQ
+  overLength {m = m} m xs | CmpEQ
---          = Just (0 ** xs)
+         = Just (0 ** xs)
---   overLength {m = plus n (S x)} n xs | (CmpGT x)
+  overLength {m = plus n (S x)} n xs | (CmpGT x)
---          = Just (S x ** rewrite plusCommutative (S x) n in xs)
+         = Just (S x ** rewrite plusCommutative (S x) n in xs)
 
 

src/TTImp/Elab/Ambiguity.idr

@@ -177,6 +177,11 @@ couldBe {vars} defs ty@(NPrimVal _ _) app
           Concrete => pure $ Just (True, app)
           Poly => pure $ Just (False, app)
           NoMatch => pure Nothing
+couldBe {vars} defs ty@(NType _) app 
+   = case !(couldBeFn {vars} defs ty (getFn app)) of
+          Concrete => pure $ Just (True, app)
+          Poly => pure $ Just (False, app)
+          NoMatch => pure Nothing
 couldBe defs ty app = pure $ Just (False, app)
 
 
@@ -257,18 +262,30 @@ checkAlternative rig elabinfo nest env fc (UniqueDefault def) alts mexpected
                do solveConstraints solvemode Normal
                   defs <- get Ctxt
                   alts' <- pruneByType !(getNF expected) alts
+                  
+                  -- We can't just use the old NF on the second attempt, 
+                  -- because we might know more now, so recalculate it
+                  exp <- getTerm expected
+                  let exp' = if delayed 
+                                then gnf env exp
+                                else expected
+
+                  logGlueNF 5 ("Ambiguous elaboration " ++ show alts' ++ 
+                               " at " ++ show fc ++
+                               "\nWith default. Target type ") env exp'
                   if delayed -- use the default if there's still ambiguity
                      then try 
                             (exactlyOne fc env 
                                 (map (\t => 
                                    (getName t, 
                                     checkImp rig elabinfo nest env t 
-                                             (Just expected))) alts'))
+                                             (Just exp'))) alts'))
-                            (checkImp rig elabinfo nest env def (Just expected))
+                            (do log 5 "All failed, running default"
+                                checkImp rig elabinfo nest env def (Just exp'))
                      else exactlyOne fc env
                            (map (\t => 
                              (getName t, 
-                              checkImp rig elabinfo nest env t (Just expected)))
+                              checkImp rig elabinfo nest env t (Just exp')))
                               alts'))
 checkAlternative rig elabinfo nest env fc uniq alts mexpected
     = do expected <- maybe (do nm <- genName "altTy"

src/TTImp/Elab/App.idr

@@ -214,6 +214,7 @@ mutual
   needsDelayExpr True (IUpdate _ _ _) = pure True
   needsDelayExpr True (IAlternative _ _ _) = pure True
   needsDelayExpr True (ISearch _ _) = pure True
+  needsDelayExpr True (IRewrite _ _ _) = pure True
   needsDelayExpr True _ = pure False
   
   -- On the LHS, for any concrete thing, we need to make sure we know

src/TTImp/Elab/Check.idr

@@ -406,6 +406,7 @@ successful ((tm, elab) :: elabs)
          md <- get MD
          defs <- branch
          catch (do -- Run the elaborator 
+                   log 5 $ "Running " ++ show tm
                    res <- elab
                    -- Record post-elaborator state
                    ust' <- get UST

src/TTImp/Elab/Rewrite.idr

@@ -58,7 +58,7 @@ elabRewrite : {vars : _} ->
               {auto c : Ref Ctxt Defs} ->
               {auto u : Ref UST UState} -> 
               FC -> Env Term vars ->
-              (expected : Glued vars) -> 
+              (expected : Term vars) -> 
               (rulety : Term vars) ->
               Core (Name, Term vars, Term vars)
 elabRewrite loc env expected rulety
@@ -68,20 +68,27 @@ elabRewrite loc env expected rulety
          (lt, rt, lty) <- getRewriteTerms loc defs tynf (NotRewriteRule loc env rulety)
          lemn <- findRewriteLemma loc rulety
 
-         rwexp_sc <- replace defs env lt (Ref loc Bound parg) 
+         -- Need to normalise again, since we might have been delayed and
-                                        !(getNF expected)
+         -- the metavariables might have been updated
+         expnf <- nf defs env expected
+
+         logNF 5 "Rewriting" env lt 
+         logNF 5 "Rewriting in" env expnf
+         rwexp_sc <- replace defs env lt (Ref loc Bound parg) expnf
+         logTerm 5 "Rewritten to" rwexp_sc
+
          empty <- clearDefs defs
          let pred = Bind loc parg (Lam RigW Explicit 
                           !(quote empty env lty))
                           (refsToLocals (Add parg parg None) rwexp_sc)
          gpredty <- getType env pred
          predty <- getTerm gpredty
-         exptm <- getTerm expected
+         exptm <- quote defs env expected
 
          -- if the rewritten expected type converts with the original,
          -- then the rewrite did nothing, which is an error
          when !(convert defs env rwexp_sc exptm) $
-             throw (RewriteNoChange loc env rulety exptm)
+                throw (RewriteNoChange loc env rulety exptm)
          pure (lemn, pred, predty)
 
 export
@@ -101,7 +108,8 @@ checkRewrite {vars} rigc elabinfo nest env fc rule tm (Just expected)
         do (rulev, grulet) <- check Rig0 elabinfo nest env rule Nothing
            rulet <- getTerm grulet
            expTy <- getTerm expected
-           (lemma, pred, predty) <- elabRewrite fc env expected rulet
+           when delayed $ log 5 "Retrying rewrite"
+           (lemma, pred, predty) <- elabRewrite fc env expTy rulet
 
            rname <- genVarName "_"
            pname <- genVarName "_"