Unifying pi binders, add implicit lambda

sample/Id.yaff

@@ -0,0 +1,19 @@
+id : {a : Type} -> a -> a
+id = \ x : _ => x
+
+idid : {a : Type} -> a -> a
+idid = id id id id id id id id id id
+       id id id id id id id id id id
+       id id id id id id id id id id
+       id id id id id id id id id id
+       id id id id id id id id id id
+       id id id id id id id id id id
+       id id id id id id id id id id
+       id id id id id id id id id id
+       id id id id id id id id id id
+       id id id id id id id id id id
+       id id id id id id id id id id
+       id id id id id id id id id id
+       id id id id id id id id id id
+       id id id id id id id id id id
+       id id id id id id id id id id

src/Core/TT.idr

@@ -797,8 +797,57 @@ data Bounds : List Name -> Type where
      None : Bounds []
      Add : (x : Name) -> Name -> Bounds xs -> Bounds (x :: xs)
 
--- export
+addVars : {later, bound : _} ->
--- refsToLocals : Bounds bound -> Term vars -> Term (bound ++ vars)
+          Bounds bound -> IsVar name idx (later ++ vars) ->
+          (idx' ** IsVar name idx' (later ++ (bound ++ vars)))
+addVars {later = []} {bound} bs p = weakenVar bound p
+addVars {later = (x :: xs)} bs First = (_ ** First)
+addVars {later = (x :: xs)} bs (Later p) 
+  = let (_ ** p') = addVars {later = xs} bs p in
+        (_ ** Later p')
+
+resolveRef : (done : List Name) -> Bounds bound -> FC -> Name -> 
+             Term (later ++ (done ++ bound ++ vars))
+resolveRef done None fc n = Ref fc Bound n
+resolveRef {later} {vars} done (Add {xs} new old bs) fc n 
+    = if n == old
+         then rewrite appendAssociative later done (new :: xs ++ vars) in
+              let (_ ** p) = weakenVar {inner = new :: xs ++ vars}
+                                       (later ++ done) First in
+                    Local fc Nothing _ p
+         else rewrite appendAssociative done [new] (xs ++ vars)
+                in resolveRef (done ++ [new]) bs fc n
+
+mkLocals : {later, bound : _} ->
+           Bounds bound -> 
+           Term (later ++ vars) -> Term (later ++ (bound ++ vars))
+mkLocals bs (Local fc r idx p) 
+    = let (_ ** p') = addVars bs p in Local fc r _ p'
+mkLocals bs (Ref fc Bound name) 
+    = resolveRef [] bs fc name
+mkLocals bs (Ref fc nt name) 
+    = Ref fc nt name
+mkLocals bs (Meta fc x y xs) 
+    = Meta fc x y (map (mkLocals bs) xs)
+mkLocals {later} bs (Bind fc x b scope) 
+    = Bind fc x (map (mkLocals bs) b) 
+           (mkLocals {later = x :: later} bs scope)
+mkLocals bs (App fc fn p arg) 
+    = App fc (mkLocals bs fn) p (mkLocals bs arg)
+mkLocals bs (Case fc cs ty x alts) = ?mkLocals_case
+mkLocals bs (TDelayed fc x y) 
+    = TDelayed fc x (mkLocals bs y)
+mkLocals bs (TDelay fc x y)
+    = TDelay fc x (mkLocals bs y)
+mkLocals bs (TForce fc x)
+    = TForce fc (mkLocals bs x)
+mkLocals bs (PrimVal fc c) = PrimVal fc c
+mkLocals bs (Erased fc) = Erased fc
+mkLocals bs (TType fc) = TType fc
+
+export
+refsToLocals : Bounds bound -> Term vars -> Term (bound ++ vars)
+refsToLocals bs y = mkLocals {later = []} bs y
 
 export Show (Term vars) where
   show tm = let (fn, args) = getFnArgs tm in showApp fn args

src/Core/Unify.idr

@@ -455,6 +455,62 @@ mutual
               then pure []
               else doUnifyBothApps mode loc env xfc hx ax yfc hy ay
 
+  -- Comparing multiplicities when converting pi binders
+  subRig : RigCount -> RigCount -> Bool
+  subRig Rig1 RigW = True -- we can pass a linear function if a general one is expected
+  subRig x y = x == y -- otherwise, the multiplicities need to match up
+
+  unifyBothBinders: {auto c : Ref Ctxt Defs} ->
+                    {auto u : Ref UST UState} ->
+                    {vars : _} ->
+                    UnifyMode -> FC -> Env Term vars ->
+                    FC -> Name -> Binder (NF vars) -> (Closure vars -> Core (NF vars)) ->
+                    FC -> Name -> Binder (NF vars) -> (Closure vars -> Core (NF vars)) ->
+                    Core (List Int)
+  unifyBothBinders mode loc env xfc x (Pi cx ix tx) scx yfc y (Pi cy iy ty) scy
+      = do defs <- get Ctxt
+           if ix /= iy || not (subRig cx cy)
+             then convertError loc env 
+                    (NBind xfc x (Pi cx ix tx) scx)
+                    (NBind yfc y (Pi cy iy ty) scy)
+             else
+               do empty <- clearDefs defs
+                  tx' <- quote empty env tx
+                  logC 10 $ (do ty' <- quote empty env ty
+                                pure ("Unifying arg types " ++ show tx' ++ " and " ++ show ty'))
+                  ct <- unify mode loc env tx ty
+                  xn <- genName "x"
+                  let env' : Env Term (x :: _)
+                           = Pi cx ix tx' :: env
+                  case ct of
+                      [] => -- No constraints, check the scope
+                         do tscx <- scx (toClosure defaultOpts env (Ref loc Bound xn))
+                            tscy <- scy (toClosure defaultOpts env (Ref loc Bound xn))
+                            tmx <- quote empty env tscx
+                            tmy <- quote empty env tscy
+                            unify mode loc env' (refsToLocals (Add x xn None) tmx)
+                                                (refsToLocals (Add x xn None) tmy)
+                      cs => -- Constraints, make new guarded constant
+                         do txtm <- quote empty env tx
+                            tytm <- quote empty env ty
+                            c <- newConstant loc Rig0 env
+                                   (Bind xfc x (Lam cx Explicit txtm) (Local xfc Nothing _ First))
+                                   (Bind xfc x (Pi cx Explicit txtm)
+                                       (weaken tytm)) cs
+                            tscx <- scx (toClosure defaultOpts env (Ref loc Bound xn))
+                            tscy <- scy (toClosure defaultOpts env (App loc c (explApp Nothing) (Ref loc Bound xn)))
+                            tmx <- quote empty env tscx
+                            tmy <- quote empty env tscy
+                            cs' <- unify mode loc env' (refsToLocals (Add x xn None) tmx)
+                                                       (refsToLocals (Add x xn None) tmy)
+                            pure (union cs cs')
+
+  unifyBothBinders mode loc env xfc x bx scx yfc y by scy
+      = convertError loc env 
+                  (NBind xfc x bx scx)
+                  (NBind yfc y by scy)
+
+
   unifyNoEta : {auto c : Ref Ctxt Defs} ->
                {auto u : Ref UST UState} ->
                {vars : _} ->
@@ -475,6 +531,8 @@ mutual
   export
   Unify NF where
     -- TODO: Eta!
+    unifyD _ _ mode loc env (NBind xfc x bx scx) (NBind yfc y by scy) 
+        = unifyBothBinders mode loc env xfc x bx scx yfc y by scy
     unifyD _ _ mode loc env tmx tmy = unifyNoEta mode loc env tmx tmy
 
   export

src/TTImp/Elab/Term.idr

@@ -15,6 +15,53 @@ import TTImp.TTImp
 
 %default covering
 
+-- If the expected type has an implicit pi, elaborate with leading
+-- implicit lambdas if they aren't there already. 
+insertImpLam : {auto c : Ref Ctxt Defs} ->
+               {auto u : Ref UST UState} ->
+               Env Term vars ->
+               (term : RawImp) -> (expected : Maybe (Glued vars)) ->
+               Core RawImp
+insertImpLam {vars} env tm (Just ty) = bindLam tm ty
+  where
+    -- If we can decide whether we need implicit lambdas without looking
+    -- at the normal form, do so
+    bindLamTm : RawImp -> Term vs -> Core (Maybe RawImp)
+    bindLamTm tm@(ILam _ _ Implicit _ _ _) (Bind fc n (Pi _ Implicit _) sc)
+        = pure (Just tm)
+    bindLamTm tm (Bind fc n (Pi c Implicit ty) sc)
+        = do n' <- genName ("imp_" ++ show n)
+             Just sc' <- bindLamTm tm sc
+                 | Nothing => pure Nothing
+             pure $ Just (ILam fc c Implicit (Just n') (Implicit fc) sc')
+    bindLamTm tm exp
+        = case getFn exp of
+               Ref _ Func _ => pure Nothing -- might still be implicit
+               Case _ _ _ _ _ => pure Nothing
+               TForce _ _ => pure Nothing
+               Bind _ _ (Lam _ _ _) _ => pure Nothing
+               _ => pure $ Just tm
+
+    bindLamNF : RawImp -> NF vars -> Core RawImp
+    bindLamNF tm@(ILam _ _ Implicit _ _ _) (NBind fc n (Pi _ Implicit _) sc)
+        = pure tm
+    bindLamNF tm (NBind fc n (Pi c Implicit ty) sc)
+        = do n' <- genName ("imp_" ++ show n)
+             sctm <- sc (toClosure defaultOpts env (Ref fc Bound n'))
+             sc' <- bindLamNF tm sctm
+             pure $ ILam fc c Implicit (Just n') (Implicit fc) sc'
+    bindLamNF tm sc = pure tm
+
+    bindLam : RawImp -> Glued vars -> Core RawImp
+    bindLam tm gty
+        = do ty <- getTerm gty
+             Just tm' <- bindLamTm tm ty
+                | Nothing =>
+                    do nf <- getNF gty
+                       bindLamNF tm nf
+             pure tm'
+insertImpLam env tm _ = pure tm
+
 -- Main driver for checking terms, after implicits have been added.
 -- Implements 'checkImp' in TTImp.Elab.Check
 checkTerm : {vars : _} ->
@@ -65,7 +112,13 @@ checkTerm rig elabinfo env (Implicit fc) Nothing
 
 -- Declared in TTImp.Elab.Check
 TTImp.Elab.Check.check rigc elabinfo env tm exp 
-    = checkImp rigc elabinfo env tm exp
+    = do defs <- get Ctxt
+         case elabMode elabinfo of
+              InLHS _ => -- Don't expand implicit lambda on lhs
+                 checkImp rigc elabinfo env tm exp
+              _ => do tm' <- insertImpLam env tm exp
+                      checkImp rigc elabinfo env tm' exp
+
 TTImp.Elab.Check.checkImp rigc elabinfo env tm exp
     = checkTerm rigc elabinfo env tm exp
 

src/TTImp/ProcessDef.idr

@@ -23,7 +23,7 @@ processDef env fc n_in tm_raw
          let expty = gnf defs [] (type gdef)
          -- TODO: abstract env in tm_raw
          (tm, _) <- elabTerm n InExpr [] tm_raw (Just expty)
-         logC 0 $ (do -- tm' <- normalise defs [] tm
+         logC 5 $ (do -- tm' <- normalise defs [] tm
                       pure (show n ++ " = " ++ show tm))
          addDef n (record { definition = Fn tm } gdef)
          pure ()

src/TTImp/ProcessType.idr

@@ -22,7 +22,7 @@ processType env fc rig vis opts (MkImpTy tfc n_in ty_raw)
          log 5 $ "Checking type decl " ++ show n ++ " : " ++ show ty_raw
          (ty, _) <- elabTerm n InType env 
                              ty_raw (Just (gType fc))
-         log 0 $ show n ++ " : " ++ show (abstractEnvType tfc env ty)
+         log 1 $ show n ++ " : " ++ show (abstractEnvType tfc env ty)
          -- TODO: Check name visibility
          let def = None -- TODO: External definitions