Use updated NF for delayed elaborators

Since the NF might refer to hole names, and those hole names might be
possible to evaluate now, we'll need to recalculate the expected type's
normal form before rerunning the delayed elaborator

src/Core/Normalise.idr

@@ -678,4 +678,18 @@ logGlue lvl msg env gtm
                                           ++ ": " ++ show tm'
             else pure ()
 
+export
+logGlueNF : {auto c : Ref Ctxt Defs} ->
+            Nat -> Lazy String -> Env Term vars -> Glued vars -> Core ()
+logGlueNF lvl msg env gtm
+    = do opts <- getOpts
+         if logLevel opts >= lvl
+            then do defs <- get Ctxt
+                    tm <- getTerm gtm
+                    tmnf <- normaliseHoles defs env tm
+                    tm' <- toFullNames tmnf
+                    coreLift $ putStrLn $ "LOG " ++ show lvl ++ ": " ++ msg 
+                                          ++ ": " ++ show tm'
+            else pure ()
+
 

src/TTImp/Elab/Ambiguity.idr

@@ -137,23 +137,30 @@ checkAlternative rig elabinfo env fc uniq alts mexpected
                               InLHS c => InLHS
                               _ => InTerm
          solveConstraints solvemode Normal
-         defs <- get Ctxt
          delayOnFailure fc rig env expected ambiguous $ 
             (\delayed => 
                do defs <- get Ctxt
-                  -- If we don't know the target type, try again later
+                  exp <- getTerm expected
+                  -- If we don't know the target type on the first attempt, 
+                  -- delay
                   when (not delayed && 
-                        !(holeIn (gamma defs) !(getTerm expected))) $
+                        !(holeIn (gamma defs) exp)) $
                     throw (AllFailed [])
-                  let alts' = alts -- pruneByType defs expected alts TODO
-                  logGlue 5 ("Ambiguous elaboration " ++ show alts' ++ 
-                             "\nTarget type ") env expected
+                  -- We can't just used the old NF on the second attempt, 
+                  -- because we might know more now, so recalculate it
+                  let exp' = if delayed 
+                                then gnf env exp
+                                else expected
+
+                  let alts' = alts -- pruneByType defs !(getNF exp') alts TODO
+                  logGlueNF 5 ("Ambiguous elaboration " ++ show alts' ++ 
+                               "\nTarget type ") env exp'
                   let tryall = case uniq of
                                     FirstSuccess => anyOne fc
                                     _ => exactlyOne fc env
                   tryall (map (\t => 
                       (getName t, 
-                       do res <- checkImp rig elabinfo env t (Just expected)
+                       do res <- checkImp rig elabinfo env t (Just exp')
                           -- Do it twice for interface resolution;
                           -- first pass gets the determining argument
                           -- (maybe rethink this, there should be a better
@@ -168,7 +175,7 @@ checkAlternative rig elabinfo env fc uniq alts mexpected
         = case getFn tm of
                Meta _ _ idx _ =>
                   do Just (Hole _) <- lookupDefExact (Resolved idx) gam
-                          | Nothing => pure False
+                          | _ => pure False
                      pure True
                _ => pure False
 

src/TTImp/Elab/App.idr

@@ -304,7 +304,8 @@ checkApp rig elabinfo env fc (IVar fc' n) expargs impargs exp
                     fnty <- quote defs env nty
                     exptyt <- maybe (pure Nothing) 
                                        (\t => do ety <- getTerm t
-                                                 pure (Just !(toFullNames ety)))
+                                                 etynf <- normaliseHoles defs env ety
+                                                 pure (Just !(toFullNames etynf)))
                                        exp
                     pure ("Checking application of " ++ show n ++
                           " to " ++ show expargs ++ "\n\tFunction type " ++

src/TTImp/Elab/Delayed.idr

@@ -57,8 +57,9 @@ delayOnFailure fc rig env expected pred elab
                   then 
                     do nm <- genName "delayed"
                        (ci, dtm) <- newDelayed fc rig env nm !(getTerm expected)
-                       logGlue 5 ("Postponing elaborator " ++ show nm ++ 
+                       logGlueNF 5 ("Postponing elaborator " ++ show nm ++ 
                                     " for") env expected
+                       log 10 ("Due to error " ++ show err)
                        ust <- get UST
                        put UST (record { delayedElab $= insert ci
                                            (mkClosedElab fc env (elab True)) } 

tests/ttimp/basic005/Ambig.yaff

@@ -29,4 +29,17 @@ testList = Cons 1 (Cons 2 (Cons 3 Nil))
 testVect : Vect ? Integer
 testVect = Cons 1 (Cons 2 (Cons 3 (Cons 4 Nil)))
 
+data IsType : $a -> Type -> Type where
+     ItIs : {x : $a} -> IsType x $a
+
+foo : IsType 5 Integer
+foo = ItIs
+
+revapply : $arg -> ($arg -> $b) -> $b
+revapply $x $f = f x
+
+-- Testing delayed elaborationg; we can't check the list until we know
+-- whether it's List or Vect, which we work out from the second argument
+test : Integer -> Nat
+test $x = revapply (Cons x (Cons x Nil)) Vect.length
 

tests/ttimp/basic005/expected

@@ -2,4 +2,5 @@ Processing as TTImp
 Written TTC
 Yaffle> (Main.S (Main.S (Main.S Main.Z)))
 Yaffle> (Main.S (Main.S (Main.S (Main.S Main.Z))))
+Yaffle> (Main.S (Main.S Main.Z))
 Yaffle> Bye for now!

tests/ttimp/basic005/input

@@ -1,3 +1,4 @@
 length testList
 length testVect
+test 94
 :q