Skip forced arguments in conversion check

This isn't always safe - we have to have also checked the type of the
things we're converting - but in the place where it is safe it can be a
pretty significant saving.

src/Core/Normalise.idr

@@ -866,15 +866,26 @@ interface Convert tm where
             {vars : List Name} ->
             Defs -> Env Term vars ->
             tm vars -> tm vars -> Core Bool
+  convertInf : {auto c : Ref Ctxt Defs} ->
+               {vars : List Name} ->
+               Defs -> Env Term vars ->
+               tm vars -> tm vars -> Core Bool
+
   convGen : {auto c : Ref Ctxt Defs} ->
             {vars : _} ->
             Ref QVar Int ->
+            Bool -> -- skip forced arguments (must have checked the type
+                    -- elsewhere first)
             Defs -> Env Term vars ->
             tm vars -> tm vars -> Core Bool
 
   convert defs env tm tm'
       = do q <- newRef QVar 0
-           convGen q defs env tm tm'
+           convGen q False defs env tm tm'
+
+  convertInf defs env tm tm'
+      = do q <- newRef QVar 0
+           convGen q True defs env tm tm'
 
 tryUpdate : {vars, vars' : _} ->
             List (Var vars, Var vars') ->
@@ -920,14 +931,14 @@ tryUpdate ms (TType fc) = pure $ TType fc
 mutual
   allConvNF : {auto c : Ref Ctxt Defs} ->
               {vars : _} ->
-              Ref QVar Int -> Defs -> Env Term vars ->
+              Ref QVar Int -> Bool -> Defs -> Env Term vars ->
               List (NF vars) -> List (NF vars) -> Core Bool
-  allConvNF q defs env [] [] = pure True
+  allConvNF q i defs env [] [] = pure True
-  allConvNF q defs env (x :: xs) (y :: ys)
+  allConvNF q i defs env (x :: xs) (y :: ys)
-      = do ok <- allConvNF q defs env xs ys
+      = do ok <- allConvNF q i defs env xs ys
-           if ok then convGen q defs env x y
+           if ok then convGen q i defs env x y
                  else pure False
-  allConvNF q defs env _ _ = pure False
+  allConvNF q i defs env _ _ = pure False
 
   -- return False if anything differs at the head, to quickly find
   -- conversion failures without going deeply into all the arguments.
@@ -961,13 +972,13 @@ mutual
 
   allConv : {auto c : Ref Ctxt Defs} ->
             {vars : _} ->
-            Ref QVar Int -> Defs -> Env Term vars ->
+            Ref QVar Int -> Bool -> Defs -> Env Term vars ->
             List (Closure vars) -> List (Closure vars) -> Core Bool
-  allConv q defs env xs ys
+  allConv q i defs env xs ys
       = do xsnf <- traverse (evalClosure defs) xs
            ysnf <- traverse (evalClosure defs) ys
            if quickConv xsnf ysnf
-              then allConvNF q defs env xsnf ysnf
+              then allConvNF q i defs env xsnf ysnf
               else pure False
 
   -- If the case trees match in structure, get the list of variables which
@@ -1056,10 +1067,10 @@ mutual
 
   chkSameDefs : {auto c : Ref Ctxt Defs} ->
                 {vars : _} ->
-                Ref QVar Int -> Defs -> Env Term vars ->
+                Ref QVar Int -> Bool -> Defs -> Env Term vars ->
                 Name -> Name ->
                 List (Closure vars) -> List (Closure vars) -> Core Bool
-  chkSameDefs q defs env n n' nargs nargs'
+  chkSameDefs q i defs env n n' nargs nargs'
      = do Just (PMDef _ args ct rt _) <- lookupDefExact n (gamma defs)
                | _ => pure False
           Just (PMDef _ args' ct' rt' _) <- lookupDefExact n' (gamma defs)
@@ -1083,27 +1094,27 @@ mutual
                         List (Var vs, Var vs') ->
                         Core Bool
        convertMatches [] = pure True
-       convertMatches ((MkVar {i} p, MkVar {i=i'} p') :: vs)
+       convertMatches ((MkVar {i=ix} p, MkVar {i=iy} p') :: vs)
-          = do let Just varg = getArgPos i nargs
+          = do let Just varg = getArgPos ix nargs
                    | Nothing => pure False
-               let Just varg' = getArgPos i' nargs'
+               let Just varg' = getArgPos iy nargs'
                    | Nothing => pure False
-               pure $ !(convGen q defs env varg varg') &&
+               pure $ !(convGen q i defs env varg varg') &&
                       !(convertMatches vs)
 
   -- If two names are standing for case blocks, check the blocks originate
   -- from the same place, and have the same scrutinee
   chkConvCaseBlock : {auto c : Ref Ctxt Defs} ->
                      {vars : _} ->
-                     FC -> Ref QVar Int -> Defs -> Env Term vars ->
+                     FC -> Ref QVar Int -> Bool -> Defs -> Env Term vars ->
                      NHead vars -> List (Closure vars) ->
                      NHead vars -> List (Closure vars) -> Core Bool
-  chkConvCaseBlock fc q defs env (NRef _ n) nargs (NRef _ n') nargs'
+  chkConvCaseBlock fc q i defs env (NRef _ n) nargs (NRef _ n') nargs'
       = do NS _ (CaseBlock _ _) <- full (gamma defs) n
               | _ => pure False
            NS _ (CaseBlock _ _) <- full (gamma defs) n'
               | _ => pure False
-           False <- chkSameDefs q defs env n n' nargs nargs'
+           False <- chkSameDefs q i defs env n n' nargs nargs'
               | True => pure True
            -- both case operators. Due to the way they're elaborated, two
            -- blocks might arise from the same source but have different
@@ -1127,7 +1138,7 @@ mutual
                 | Nothing => pure False
            let Just sc' = getScrutinee scpos' nargs'
                 | Nothing => pure False
-           ignore $ convGen q defs env sc sc'
+           ignore $ convGen q i defs env sc sc'
            pure (location def == location def')
     where
       -- Need to find the position of the scrutinee to see if they are the
@@ -1140,70 +1151,88 @@ mutual
       getScrutinee Z (x :: xs) = Just x
       getScrutinee (S k) (x :: xs) = getScrutinee k xs
       getScrutinee _ _ = Nothing
-  chkConvCaseBlock _ _ _ _ _ _ _ _ = pure False
+  chkConvCaseBlock _ _ _ _ _ _ _ _ _ = pure False
 
   chkConvHead : {auto c : Ref Ctxt Defs} ->
                 {vars : _} ->
-                Ref QVar Int -> Defs -> Env Term vars ->
+                Ref QVar Int -> Bool -> Defs -> Env Term vars ->
                 NHead vars -> NHead vars -> Core Bool
-  chkConvHead q defs env (NLocal _ idx _) (NLocal _ idx' _) = pure $ idx == idx'
+  chkConvHead q i defs env (NLocal _ idx _) (NLocal _ idx' _) = pure $ idx == idx'
-  chkConvHead q defs env (NRef _ n) (NRef _ n') = pure $ n == n'
+  chkConvHead q i defs env (NRef _ n) (NRef _ n') = pure $ n == n'
-  chkConvHead q defs env (NMeta n i args) (NMeta n' i' args')
+  chkConvHead q inf defs env (NMeta n i args) (NMeta n' i' args')
      = if i == i'
-          then allConv q defs env args args'
+          then allConv q inf defs env args args'
           else pure False
-  chkConvHead q defs env _ _ = pure False
+  chkConvHead q i defs env _ _ = pure False
 
   convBinders : {auto c : Ref Ctxt Defs} ->
                 {vars : _} ->
-                Ref QVar Int -> Defs -> Env Term vars ->
+                Ref QVar Int -> Bool -> Defs -> Env Term vars ->
                 Binder (NF vars) -> Binder (NF vars) -> Core Bool
-  convBinders q defs env (Pi _ cx ix tx) (Pi _ cy iy ty)
+  convBinders q i defs env (Pi _ cx ix tx) (Pi _ cy iy ty)
       = if cx /= cy
            then pure False
-           else convGen q defs env tx ty
+           else convGen q i defs env tx ty
-  convBinders q defs env (Lam _ cx ix tx) (Lam _ cy iy ty)
+  convBinders q i defs env (Lam _ cx ix tx) (Lam _ cy iy ty)
       = if cx /= cy
            then pure False
-           else convGen q defs env tx ty
+           else convGen q i defs env tx ty
-  convBinders q defs env bx by
+  convBinders q i defs env bx by
       = if multiplicity bx /= multiplicity by
            then pure False
-           else convGen q defs env (binderType bx) (binderType by)
+           else convGen q i defs env (binderType bx) (binderType by)
 
 
   export
   Convert NF where
-    convGen q defs env (NBind fc x b sc) (NBind _ x' b' sc')
+    convGen q i defs env (NBind fc x b sc) (NBind _ x' b' sc')
         = do var <- genName "conv"
              let c = MkClosure defaultOpts [] env (Ref fc Bound var)
-             bok <- convBinders q defs env b b'
+             bok <- convBinders q i defs env b b'
              if bok
                 then do bsc <- sc defs c
                         bsc' <- sc' defs c
-                        convGen q defs env bsc bsc'
+                        convGen q i defs env bsc bsc'
                 else pure False
 
-    convGen q defs env tmx@(NBind fc x (Lam fc' c ix tx) scx) tmy
+    convGen q i defs env tmx@(NBind fc x (Lam fc' c ix tx) scx) tmy
         = do empty <- clearDefs defs
              etay <- nf defs env
                         (Bind fc x (Lam fc' c !(traverse (quote empty env) ix) !(quote empty env tx))
                            (App fc (weaken !(quote empty env tmy))
                                 (Local fc Nothing _ First)))
-             convGen q defs env tmx etay
+             convGen q i defs env tmx etay
-    convGen q defs env tmx tmy@(NBind fc y (Lam fc' c iy ty) scy)
+    convGen q i defs env tmx tmy@(NBind fc y (Lam fc' c iy ty) scy)
         = do empty <- clearDefs defs
              etax <- nf defs env
                         (Bind fc y (Lam fc' c !(traverse (quote empty env) iy) !(quote empty env ty))
                            (App fc (weaken !(quote empty env tmx))
                                 (Local fc Nothing _ First)))
-             convGen q defs env etax tmy
+             convGen q i defs env etax tmy
 
-    convGen q defs env (NApp fc val args) (NApp _ val' args')
+    convGen q inf defs env (NApp fc val args) (NApp _ val' args')
-        = if !(chkConvHead q defs env val val')
+        = if !(chkConvHead q inf defs env val val')
-             then allConv q defs env args1 args2
+             then do i <- getInfPos val
-             else chkConvCaseBlock fc q defs env val args1 val' args2
+                     allConv q inf defs env (dropInf 0 i args1) (dropInf 0 i args2)
+             else chkConvCaseBlock fc q inf defs env val args1 val' args2
         where
+          getInfPos : NHead vars -> Core (List Nat)
+          getInfPos (NRef _ n)
+              = if inf
+                   then do Just gdef <- lookupCtxtExact n (gamma defs)
+                                | _ => pure []
+                           pure (inferrable gdef)
+                   else pure []
+          getInfPos _ = pure []
+
+          dropInf : Nat -> List Nat -> List a -> List a
+          dropInf _ [] xs = xs
+          dropInf _ _ [] = []
+          dropInf i ds (x :: xs)
+              = if i `elem` ds
+                   then dropInf (S i) ds xs
+                   else x :: dropInf (S i) ds xs
+
           -- Discard file context information irrelevant for conversion checking
           args1 : List (Closure vars)
           args1 = map snd args
@@ -1211,52 +1240,52 @@ mutual
           args2 : List (Closure vars)
           args2 = map snd args'
 
-    convGen q defs env (NDCon _ nm tag _ args) (NDCon _ nm' tag' _ args')
+    convGen q i defs env (NDCon _ nm tag _ args) (NDCon _ nm' tag' _ args')
         = if tag == tag'
-             then allConv q defs env (map snd args) (map snd args')
+             then allConv q i defs env (map snd args) (map snd args')
              else pure False
-    convGen q defs env (NTCon _ nm tag _ args) (NTCon _ nm' tag' _ args')
+    convGen q i defs env (NTCon _ nm tag _ args) (NTCon _ nm' tag' _ args')
         = if nm == nm'
-             then allConv q defs env (map snd args) (map snd args')
+             then allConv q i defs env (map snd args) (map snd args')
              else pure False
-    convGen q defs env (NAs _ _ _ tm) (NAs _ _ _ tm')
+    convGen q i defs env (NAs _ _ _ tm) (NAs _ _ _ tm')
-        = convGen q defs env tm tm'
+        = convGen q i defs env tm tm'
 
-    convGen q defs env (NDelayed _ r arg) (NDelayed _ r' arg')
+    convGen q i defs env (NDelayed _ r arg) (NDelayed _ r' arg')
         = if compatible r r'
-             then convGen q defs env arg arg'
+             then convGen q i defs env arg arg'
              else pure False
-    convGen q defs env (NDelay _ r _ arg) (NDelay _ r' _ arg')
+    convGen q i defs env (NDelay _ r _ arg) (NDelay _ r' _ arg')
         = if compatible r r'
              then do -- if it's codata, don't reduce the argument or we might
                      -- go for ever, if it's infinite
                      adefs <- case r of
                                    LLazy => pure defs
                                    _ => clearDefs defs
-                     convGen q adefs env arg arg'
+                     convGen q i adefs env arg arg'
              else pure False
-    convGen q defs env (NForce _ r arg args) (NForce _ r' arg' args')
+    convGen q i defs env (NForce _ r arg args) (NForce _ r' arg' args')
         = if compatible r r'
-             then if !(convGen q defs env arg arg')
+             then if !(convGen q i defs env arg arg')
-                     then allConv q defs env (map snd args) (map snd args')
+                     then allConv q i defs env (map snd args) (map snd args')
                      else pure False
              else pure False
 
-    convGen q defs env (NPrimVal _ c) (NPrimVal _ c') = pure (c == c')
+    convGen q i defs env (NPrimVal _ c) (NPrimVal _ c') = pure (c == c')
-    convGen q defs env (NErased _ _) _ = pure True
+    convGen q i defs env (NErased _ _) _ = pure True
-    convGen q defs env _ (NErased _ _) = pure True
+    convGen q i defs env _ (NErased _ _) = pure True
-    convGen q defs env (NType _) (NType _) = pure True
+    convGen q i defs env (NType _) (NType _) = pure True
-    convGen q defs env x y = pure False
+    convGen q i defs env x y = pure False
 
   export
   Convert Term where
-    convGen q defs env x y
+    convGen q i defs env x y
-        = convGen q defs env !(nf defs env x) !(nf defs env y)
+        = convGen q i defs env !(nf defs env x) !(nf defs env y)
 
   export
   Convert Closure where
-    convGen q defs env x y
+    convGen q i defs env x y
-        = convGen q defs env !(evalClosure defs x) !(evalClosure defs y)
+        = convGen q i defs env !(evalClosure defs x) !(evalClosure defs y)
 
 export
 getValArity : Defs -> Env Term vars -> NF vars -> Core Nat

src/Core/Unify.idr

@@ -667,7 +667,7 @@ mutual
               Core UnifyResult
   unifyIfEq post loc mode env x y
         = do defs <- get Ctxt
-             if !(convert defs env x y)
+             if !(convertInf defs env x y)
                 then pure success
                 else if post
                         then postpone loc mode ("Postponing unifyIfEq " ++