Record local hints in delayed elaborators

We might not have set up search problems yet when delaying an
elaborator, so we need to know what the local hints were at the point of
delay.

src/Core/UnifyState.idr

@@ -84,12 +84,13 @@ record UState where
   dotConstraints : List (Name, DotReason, Constraint) -- dot pattern constraints
   nextName : Int
   nextConstraint : Int
-  delayedElab : List (Nat, Int, Core ClosedTerm)
+  delayedElab : List (Nat, Int, NameMap (), Core ClosedTerm)
                 -- Elaborators which we need to try again later, because
                 -- we didn't have enough type information to elaborate
                 -- successfully yet.
                 -- 'Nat' is the priority (lowest first)
                 -- The 'Int' is the resolved name.
+                -- NameMap () is the set of local hints at the point of delay
   logging : Bool
 
 export

src/TTImp/Elab/Delayed.idr

@@ -15,6 +15,7 @@ import TTImp.Elab.Check
 import TTImp.TTImp
 
 import Libraries.Data.IntMap
+import Libraries.Data.NameMap
 import Data.List
 
 %default covering
@@ -81,8 +82,10 @@ delayOnFailure fc rig env expected pred pri elab
                                       " for") env expected
                          log "elab.delay" 10 ("Due to error " ++ show err)
                          ust <- get UST
+                         defs <- get Ctxt
                          put UST (record { delayedElab $=
-                                 ((pri, ci, mkClosedElab fc env (deeper (elab True))) :: ) }
+                                 ((pri, ci, localHints defs,
+                                   mkClosedElab fc env (deeper (elab True))) :: ) }
                                          ust)
                          pure (dtm, expected)
                     else throw err)
@@ -106,8 +109,9 @@ delayElab {vars} fc rig env exp pri elab
          logGlueNF "elab.delay" 5 ("Postponing elaborator " ++ show nm ++
                       " for") env expected
          ust <- get UST
+         defs <- get Ctxt
          put UST (record { delayedElab $=
-                 ((pri, ci, mkClosedElab fc env elab) :: ) }
+                 ((pri, ci, localHints defs, mkClosedElab fc env elab) :: ) }
                          ust)
          pure (dtm, expected)
   where
@@ -208,11 +212,11 @@ retryDelayed' : {vars : _} ->
                 {auto u : Ref UST UState} ->
                 {auto e : Ref EST (EState vars)} ->
                 RetryError ->
-                List (Nat, Int, Core ClosedTerm) ->
-                List (Nat, Int, Core ClosedTerm) ->
-                Core (List (Nat, Int, Core ClosedTerm))
+                List (Nat, Int, NameMap (), Core ClosedTerm) ->
+                List (Nat, Int, NameMap (), Core ClosedTerm) ->
+                Core (List (Nat, Int, NameMap (), Core ClosedTerm))
 retryDelayed' errmode acc [] = pure (reverse acc)
-retryDelayed' errmode acc (d@(_, i, elab) :: ds)
+retryDelayed' errmode acc (d@(_, i, hints, elab) :: ds)
     = do defs <- get Ctxt
          Just Delayed <- lookupDefExact (Resolved i) (gamma defs)
               | _ => retryDelayed' errmode acc ds
@@ -222,6 +226,9 @@ retryDelayed' errmode acc (d@(_, i, elab) :: ds)
                -- elab itself might have delays internally, so keep track of them
                ust <- get UST
                put UST (record { delayedElab = [] } ust)
+               defs <- get Ctxt
+               put Ctxt (record { localHints = hints } defs)
+
                tm <- elab
                ust <- get UST
                let ds' = reverse (delayedElab ust) ++ ds
@@ -247,7 +254,7 @@ retryDelayed : {vars : _} ->
                {auto m : Ref MD Metadata} ->
                {auto u : Ref UST UState} ->
                {auto e : Ref EST (EState vars)} ->
-               List (Nat, Int, Core ClosedTerm) ->
+               List (Nat, Int, NameMap (), Core ClosedTerm) ->
                Core ()
 retryDelayed ds
     = do est <- get EST

tests/Main.idr

@@ -90,7 +90,7 @@ idrisTestsInterface = MkTestPool []
        "interface009", "interface010", "interface011", "interface012",
        "interface013", "interface014", "interface015", "interface016",
        "interface017", "interface018", "interface019", "interface020",
-       "interface021", "interface022", "interface023"]
+       "interface021", "interface022", "interface023", "interface024"]
 
 idrisTestsLinear : TestPool
 idrisTestsLinear = MkTestPool []

tests/idris2/interface024/EH.idr

@@ -0,0 +1,138 @@
+import Syntax.PreorderReasoning
+
+-------- some notation ----------
+infixr 6 .+.,:+:
+infixr 7 .*.,:*:
+
+interface Additive a where
+  constructor MkAdditive
+  (.+.) : a -> a -> a
+  O   : a
+
+interface Additive2 a where
+  constructor MkAdditive2
+  (:+:) : a -> a -> a
+  O2   : a 
+  
+interface Multiplicative a where
+  constructor MkMultiplicative
+  (.*.) : a -> a -> a
+  I     : a
+
+record MonoidOver U where            
+  constructor WithStruct
+  Unit    : U
+  Mult    : U -> U -> U
+  lftUnit : (x : U) -> Unit `Mult` x    = x
+  rgtUnit : (x : U) -> x    `Mult` Unit = x
+  assoc   : (x,y,z : U) 
+                    -> x `Mult` (y `Mult` z) = (x `Mult` y) `Mult` z
+
+record Monoid where
+  constructor MkMonoid
+  U : Type
+  Struct : MonoidOver U
+
+AdditiveStruct : (m : MonoidOver a) -> Additive a
+AdditiveStruct m = MkAdditive (Mult $ m) 
+                              (Unit $ m)
+AdditiveStruct2 : (m : MonoidOver a) -> Additive2 a
+AdditiveStruct2 m = MkAdditive2 (Mult $ m) 
+                                (Unit $ m)
+AdditiveStructs : (ma : MonoidOver a) -> (mb : MonoidOver b) 
+              -> (Additive a, Additive2 b)
+AdditiveStructs ma mb = (AdditiveStruct ma, AdditiveStruct2 mb)
+
+getAdditive : (m : Monoid) -> Additive (U m)
+getAdditive m = AdditiveStruct (Struct m)
+
+MultiplicativeStruct : (m : Monoid) -> Multiplicative (U m)
+MultiplicativeStruct m = MkMultiplicative (Mult $ Struct m)
+                                          (Unit $ Struct m)
+-----------------------------------------------------                   
+
+Commutative : MonoidOver a -> Type
+Commutative m = (x,y : a) -> let _ = AdditiveStruct m in
+                x .+. y = y .+. x
+                
+Commute : (Additive a, Additive2 a) => Type
+Commute =
+          (x11,x12,x21,x22 : a) -> 
+          ((x11 :+: x12) .+. (x21 :+: x22))
+          =
+          ((x11 .+. x21) :+: (x12 .+. x22))
+
+product : (ma, mb : Monoid) -> Monoid 
+product ma mb = 
+  let 
+      %hint aStruct : Additive (U ma)
+      aStruct = getAdditive ma
+      %hint bStruct : Additive (U mb)
+      bStruct = getAdditive mb
+      
+  in MkMonoid (U ma, U mb) $ WithStruct
+     (O, O)
+     (\(x1,y1), (x2, y2)  => (x1 .+. x2, y1 .+. y2))
+     (\(x,y) => rewrite lftUnit (Struct ma) x in 
+                rewrite lftUnit (Struct mb) y in
+                Refl)
+     (\(x,y) => rewrite rgtUnit (Struct ma) x in
+                rewrite rgtUnit (Struct mb) y in
+                Refl)
+     (\(x1,y1),(x2,y2),(x3,y3) => 
+                rewrite assoc (Struct ma) x1 x2 x3 in
+                rewrite assoc (Struct mb) y1 y2 y3 in
+                Refl)
+
+EckmannHilton : forall a . (ma,mb : MonoidOver a) 
+             -> let ops = AdditiveStructs ma mb in
+                Commute @{ops}
+             -> (Commutative ma, (x,y : a) -> x .+. y = x :+: y)
+EckmannHilton ma mb prf = 
+  let %hint first : Additive a
+      first = AdditiveStruct ma
+      %hint second : Additive2 a
+      second = AdditiveStruct2 mb in
+  let SameUnits : (the a O === O2)
+      SameUnits = Calc $
+        |~ O
+        ~~  O         .+.         O  ...(sym $ lftUnit ma O)
+        ~~ (O :+: O2) .+. (O2 :+: O) ...(sym $ cong2 (.+.) 
+                                             (rgtUnit mb O)
+                                             (lftUnit mb O))
+        ~~ (O .+. O2) :+: (O2 .+. O) ...(prf O O2 O2 O)
+        ~~        O2  :+:  O2        ...(cong2 (:+:)
+                                             (lftUnit ma O2)
+                                             (rgtUnit ma O2))
+        ~~ O2                        ...(lftUnit mb O2)
+        
+      SameMults : (x,y : a) -> (x .+. y) === (x :+: y)
+      SameMults x y = Calc $
+        |~ x .+. y
+        ~~ (x :+: O2) .+. (O2 :+: y) ...(sym $ cong2 (.+.)
+                                             (rgtUnit mb x)
+                                             (lftUnit mb y))
+        ~~ (x .+. O2) :+: (O2 .+. y) ...(prf x O2 O2 y)
+        ~~ (x .+. O ) :+: (O  .+. y) ...(cong (\u => 
+                                              (x .+. u) :+: (u .+. y))
+                                              (sym SameUnits))
+        ~~ x :+: y                   ...(cong2 (:+:)
+                                              (rgtUnit ma x)
+                                              (lftUnit ma y))
+                                                    
+      Commutativity : Commutative ma
+      Commutativity x y = Calc $
+        |~ x .+. y
+        ~~ (O2 :+: x) .+. (y :+: O2) ...(sym $ cong2 (.+.)
+                                             (lftUnit mb x)
+                                             (rgtUnit mb y))
+        ~~ (O2 .+. y) :+: (x .+. O2) ...(prf O2 x y O2)
+        ~~ (O  .+. y) :+: (x .+. O ) ...(cong (\u => 
+                                              (u .+. y) :+: (x .+. u))
+                                              (sym SameUnits))
+        ~~ y :+: x                   ...(cong2 (:+:)
+                                              (lftUnit ma y)
+                                              (rgtUnit ma x))
+        ~~ y .+. x                   ...(sym $ SameMults y x)
+  in (Commutativity, SameMults)
+

tests/idris2/interface024/expected

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

tests/idris2/interface024/run

@@ -0,0 +1,3 @@
+$1 --no-banner --no-color --check EH.idr -p contrib
+
+rm -rf build