[ new ] Dot inferred patterns in erased functions

CHANGELOG_NEXT.md

@@ -65,9 +65,10 @@ should target this file (`CHANGELOG_NEXT`).
   typically happens when a numeric literal or an ambiguous name appears in an
   `impossible` clause.
 * Do not inline `Core.sequence`, because it is recursively defined.
-* Fixed coverage checker issues (#1800, #1998, #2318, #2822, #3679).
+* Fixed coverage checker issues (#1800, #1998, #2318, #2822, #3357, #3679).
 * Fixed totality checking in namespace and mutual blocks (#2868, #3692).
 * Fixed incorrect argument multiplicity when using an as-pattern (#3687).
+* Do not match on inferred patterns in erased functions (#3721).
 
 ### Building/Packaging changes
 

idris2api.ipkg

@@ -279,6 +279,7 @@ modules =
     TTImp.ProcessDecls,
     TTImp.ProcessDecls.Totality,
     TTImp.ProcessDef,
+    TTImp.ProcessDef.Dot,
     TTImp.ProcessFnOpt,
     TTImp.ProcessParams,
     TTImp.ProcessRecord,

src/Core/Case/CaseBuilder.idr

@@ -342,9 +342,14 @@ clauseType phase (MkPatClause pvars (MkInfo arg _ ty :: rest) pid rhs)
              then Nothing
              else splitCon a xs
     getClauseType phase (PAs _ _ p) t = getClauseType phase p t
-    getClauseType phase l (Known r t) = if isErased r
-      then Nothing
-      else clauseType' l
+    getClauseType (CompileTime cr) l (Known r t)
+        = if isErased r && not (isErased cr)
+             then Nothing
+             else clauseType' l
+    getClauseType phase l (Known r t)
+        = if isErased r
+             then Nothing
+             else clauseType' l
     getClauseType phase l _ = clauseType' l
 
 partition : {a, as, vars : _} ->

src/Core/TT/Term.idr

@@ -317,6 +317,15 @@ getFnArgs tm = getFA [] tm
     getFA args (App _ f a) = getFA (a :: args) f
     getFA args tm = (tm, args)
 
+export
+getFnArgsWithFC : Term vars -> (Term vars, List (FC, Term vars))
+getFnArgsWithFC tm = getFA [] tm
+  where
+    getFA : List (FC, Term vars) -> Term vars ->
+            (Term vars, List (FC, Term vars))
+    getFA args (App fc f a) = getFA ((fc, a) :: args) f
+    getFA args tm = (tm, args)
+
 export
 getFn : Term vars -> Term vars
 getFn (App _ f a) = getFn f

src/Core/TT/Var.idr

@@ -35,10 +35,7 @@ data IsVar : a -> Nat -> List a -> Type where
 
 %name IsVar idx
 
--- `vs` is available in the erased fragment, and the case builder
--- pattern-matches on it. To simplify the case tree and help the
--- coverage checker, we use an explicit dot pattern here.
--- TODO: remove `{vs = .(_)}` once the compiler generates more optimal case trees.
+-- TODO: remove `{vs = .(_)}`
 export
 0 Last : HasLength (S n) vs -> Exists (\ nm => IsVar nm n vs)
 Last {vs = .(_)} (S Z) = Evidence _ First

src/TTImp/Elab/App.idr

@@ -573,6 +573,7 @@ mutual
   isImplicitAs (IAs _ _ UseLeft _ (Implicit {})) = True
   isImplicitAs _ = False
 
+  export
   isBindAllExpPattern : Name -> Bool
   isBindAllExpPattern (UN Underscore) = True
   isBindAllExpPattern _ = False

src/TTImp/ProcessDef.idr

@@ -27,6 +27,7 @@ import TTImp.Impossible
 import TTImp.PartialEval
 import TTImp.TTImp
 import TTImp.TTImp.Functor
+import TTImp.ProcessDef.Dot
 import TTImp.ProcessType
 import TTImp.Unelab
 import TTImp.WithClause
@@ -285,7 +286,7 @@ checkLHS : {vars : _} ->
            {auto u : Ref UST UState} ->
            {auto s : Ref Syn SyntaxInfo} ->
            {auto o : Ref ROpts REPLOpts} ->
-           Bool -> -- in transform
+           (trans : Bool) -> -- in transform
            (mult : RigCount) ->
            Int -> List ElabOpt -> NestedNames vars -> Env Term vars ->
            FC -> RawImp ->
@@ -311,7 +312,8 @@ checkLHS {vars} trans mult n opts nest env fc lhs_in
                    then pure lhs_bound
                    else implicitsAs n defs vars lhs_bound
 
-         logC "declare.def.lhs" 5 $ do pure $ "Checking LHS of " ++ show !(getFullName (Resolved n))
+         fullname <- getFullName (Resolved n)
+         log "declare.def.lhs" 5 $ "Checking LHS of " ++ show fullname
 -- todo: add Pretty RawImp instance
 --         logC "declare.def.lhs" 5 $ do pure $ show $ indent {ann = ()} 2 $ pretty lhs
          log "declare.def.lhs" 10 $ show lhs
@@ -320,7 +322,7 @@ checkLHS {vars} trans mult n opts nest env fc lhs_in
                           then InTransform
                           else InLHS mult
          (lhstm, lhstyg) <-
-             wrapErrorC opts (InLHS fc !(getFullName (Resolved n))) $
+             wrapErrorC opts (InLHS fc fullname) $
                      elabTerm n lhsMode opts nest env
                                 (IBindHere fc PATTERN lhs) Nothing
          logTerm "declare.def.lhs" 5 "Checked LHS term" lhstm
@@ -336,6 +338,7 @@ checkLHS {vars} trans mult n opts nest env fc lhs_in
          lhsty <- normaliseHoles defs env lhsty
          linvars_in <- findLinear True 0 linear lhstm
          logTerm "declare.def.lhs" 10 "Checked LHS term after normalise" lhstm
+
          log "declare.def.lhs" 5 $ "Linearity of names in " ++ show n ++ ": " ++
                  show linvars_in
 
@@ -347,8 +350,18 @@ checkLHS {vars} trans mult n opts nest env fc lhs_in
          logTerm "declare.def.lhs" 5 "LHS type" lhsty_lin
          setHoleLHS (bindEnv fc env lhstm_lin)
 
-         ext <- extendEnv env Refl nest lhstm_lin lhsty_lin
-         pure (lhs, ext)
+         (vars'  ** (sub', env', nest', lhstm', lhsty')) <-
+           extendEnv env Refl nest lhstm_lin lhsty_lin
+         logTerm "declare.def.lhs" 3 "LHS term after extension" lhstm'
+
+         lhstm' <- if trans || not (isErased mult)
+                      then pure lhstm'
+                      else do res <- wrapErrorC opts (InLHS fc fullname) $
+                                       dotInferred defs (thinNestedNames nest sub') env' True lhs lhstm'
+                              logTerm "declare.def.lhs" 3 "LHS term after dotting" res
+                              pure res
+
+         pure (lhs, (vars'  ** (sub', env', nest', lhstm', lhsty')))
 
 -- Return whether any of the pattern variables are in a trivially empty
 -- type, where trivally empty means one of:

src/TTImp/ProcessDef/Dot.idr

@@ -0,0 +1,174 @@
+module TTImp.ProcessDef.Dot
+
+import Core.Context
+import Core.Env
+import Core.Normalise
+import Core.Value
+
+import TTImp.TTImp
+import TTImp.Elab.App
+
+import Data.DPair
+import Data.SnocList
+
+isPattern : Term vars -> Bool
+isPattern (App {}) = True
+isPattern (Ref {}) = True
+isPattern (TDelay {}) = True
+isPattern (PrimVal {}) = True
+isPattern (TType {}) = True
+isPattern (Bind _ _ (Pi {}) _) = True
+isPattern _ = False
+
+isImplicit : RawImp -> Bool
+isImplicit (Implicit {}) = True
+isImplicit (IAs _ _ _ _ tm) = isImplicit tm
+isImplicit _ = False
+
+dot : FC -> Term vars -> Term vars
+dot _ tm@(Erased {}) = tm
+dot fc tm = if isPattern tm
+               then Erased fc $ Dotted tm
+               else tm
+
+parameters {auto c : Ref Ctxt Defs} {vars : Scope}
+           (defs : Defs) (nest : NestedNames vars) (env : Env Term vars)
+  export
+  dotInferred : (topLevel : Bool) ->
+                RawImp ->
+                Term vars ->
+                Core (Term vars)
+
+  dotIfInferred : FC -> RawImp -> Term vars ->
+                  Core (Term vars)
+  dotIfInferred fc (IAs _ _ _ _ rawArg) (As fc' s n arg)
+      = As fc' s n <$> dotIfInferred fc rawArg arg
+  dotIfInferred fc rawArg arg
+      = if isImplicit rawArg
+           then pure $ dot fc arg
+           else dotInferred False rawArg arg
+
+  addDots : (acc : SnocList (FC, Term vars)) ->
+            (ty : NF vars) ->
+            (args : List (FC, Term vars)) ->
+            (expargs : List RawImp) ->
+            (autoargs : List RawImp) ->
+            (namedargs : List (Name, RawImp)) ->
+            Core (List (FC, Term vars))
+  addDots acc (NBind _ n (Pi _ _ Explicit _) sc) ((fc, arg) :: args)  (rawArg :: exps) autos named
+      = addDots (acc :< (fc, !(dotIfInferred fc rawArg arg)))
+                !(sc defs $ toClosure defaultOpts env arg)
+                args exps autos named
+  addDots acc (NBind _ n (Pi _ _ AutoImplicit _) sc) ((fc, arg) :: args) exps (rawArg :: autos) named
+      = addDots (acc :< (fc, !(dotIfInferred fc rawArg arg)))
+                !(sc defs $ toClosure defaultOpts env arg)
+                args exps autos named
+  addDots acc (NBind _ n (Pi _ _ Explicit _) sc) ((fc, arg) :: args) [] autos named
+      = do (arg', named') <- case findNamed n named of
+               Nothing => case findBindAllExpPattern named of
+                   Nothing => throw $ InternalError "Impossible happened: explicit argument not found."
+                   Just rawArg => pure (!(dotIfInferred fc rawArg arg), named)
+               Just ((_, rawArg), named') => pure (!(dotIfInferred fc rawArg arg), named')
+           addDots (acc :< (fc, arg'))
+                   !(sc defs $ toClosure defaultOpts env arg')
+                   args [] autos named'
+  addDots acc (NBind _ n (Pi _ _ AutoImplicit _) sc) ((fc, arg) :: args) exps [] named
+      = do (arg', named') <- case findNamed n named of
+               Nothing => pure (dot fc arg, named)
+               Just ((_, rawArg), named') => pure (!(dotIfInferred fc rawArg arg), named')
+           addDots (acc :< (fc, arg'))
+                   !(sc defs $ toClosure defaultOpts env arg')
+                   args exps [] named'
+  addDots acc (NBind _ n (Pi _ _ Implicit _) sc) ((fc, arg) :: args) exps autos named
+      = do (arg', named') <- case findNamed n named of
+               Nothing => pure (dot fc arg, named)
+               Just ((_, rawArg), named') => pure (!(dotIfInferred fc rawArg arg), named')
+           addDots (acc :< (fc, arg'))
+                   !(sc defs $ toClosure defaultOpts env arg')
+                   args exps autos named'
+  addDots acc (NBind _ n (Pi _ _ (DefImplicit defArg) _) sc) ((fc, arg) :: args) exps autos named
+      = do (arg', named') <- case findNamed n named of
+               Nothing => pure (dot fc arg, named)
+               Just ((_, rawArg), named') => pure (!(dotIfInferred fc rawArg arg), named')
+           addDots (acc :< (fc, arg'))
+                   !(sc defs $ toClosure defaultOpts env arg')
+                   args exps autos named'
+  addDots acc ty [] [] [] named
+      = if null $ filter (not . isBindAllExpPattern . fst) named
+           then pure $ toList acc
+           else throw $ InternalError "Impossible happened: arguments mismatch."
+  addDots _ _ _ _ _ _
+      = throw $ InternalError $ "Impossible happened: arguments mismatch."
+
+  skipArgs : Nat ->
+             (acc : SnocList (FC, Term vars)) ->
+             (args : List (FC, Term vars)) ->
+             (ty : NF vars) ->
+             Core (SnocList (FC, Term vars), List (FC, Term vars), NF vars)
+  skipArgs Z acc args ty = pure (acc, args, ty)
+  skipArgs (S n) acc ((fc, arg) :: args) (NBind _ _ (Pi {}) sc)
+      = skipArgs n (acc :< (fc, arg)) args !(sc defs $ toClosure defaultOpts env arg)
+  skipArgs _ _  __
+      = throw $ InternalError "Impossible happened: expected nested argument."
+
+  dotInferred topLevel (IAlternative fc ty alts) tm
+      = do let (Ref _ _ nm) = getFn tm
+             | _ => pure tm
+           let Just alt = pickAlt !(toFullNames nm) alts
+             | _ => pure tm
+           dotInferred topLevel alt tm
+    where
+      pickAlt : Name -> List RawImp -> Maybe RawImp
+      pickAlt nm [] = Nothing
+      pickAlt nm (x :: xs)
+          = do let (IVar _ nm') = getFn x
+                 | _ => Nothing
+               if nm == nm'
+                  then Just x
+                  else pickAlt nm xs
+  dotInferred topLevel raw tm = go raw [] [] []
+    where
+      -- Don't dot primitives functions in argument position
+      needsDot : Name -> Core Bool
+      needsDot nm = if topLevel
+                       then pure $ True
+                       else pure $ not $ isPrimName !getPrimitiveNames nm
+
+      go : RawImp ->
+           (expargs : List RawImp) ->
+           (autoargs : List RawImp) ->
+           (namedargs : List (Name, RawImp)) ->
+           Core (Term vars)
+      go (IApp fc fn arg) exps autos named
+         = go fn (arg :: exps) autos named
+      go (IWithApp fc fn arg) exps autos named
+         = go fn (arg :: exps) autos named
+      go (IAutoApp fc fn arg) exps autos named
+         = go fn exps (arg :: autos) named
+      go (INamedApp fc fn nm arg) exps autos named
+         = go fn exps autos ((nm, arg) :: named)
+      go (IVar _ rawName) exps autos named
+          = do let (fn@(Ref fc t nm), args) = getFnArgsWithFC tm
+                 | _ => pure tm
+               Just def <- lookupCtxtExact nm (gamma defs)
+                 | Nothing => undefinedName fc nm
+               True <- needsDot rawName
+                 | _ => pure tm
+               -- TODO: remove `the` after fix idris-lang/Idris2#3418
+               let skip = maybe 0 (the (_ -> _) $ \(_, n, _) => length n) $
+                                  lookup nm (names nest) <|> lookup rawName (names nest)
+                               -- ^ Local block put raw name in `NestedNames`
+                               --   while parameters put `Resolved`.
+                               --   So, we need to check both
+               tynf <- nf defs env $ embed $ type def
+               (skipped, rest, ty') <- skipArgs skip [<] args tynf
+               args' <- addDots skipped ty' rest exps autos named
+               pure $ applyStackWithFC fn args'
+      go (IPi _ _ _ _ aty _) [] [] []
+         = case tm of
+                Bind fc n (Pi bfc r p ty) sc
+                   => pure $ Bind fc n (Pi bfc r p !(dotIfInferred bfc aty ty)) sc
+                _ => throw $ InternalError "Expected Pi type, got \{show tm}"
+      go (IPi _ _ _ _ aty _) exps autos named
+         = throw $ InternalError "Unexpected arguments Pi-type with arguments: \{show raw}"
+      go _ _ _ _ = pure tm

src/TTImp/TTImp.idr

@@ -34,6 +34,12 @@ Weaken NestedNames where
       wknName (n, (mn, vars, rep))
           = (n, (mn, map (weakenNs s) vars, \fc, nt => weakenNs s (rep fc nt)))
 
+export
+thinNestedNames : Thinnable NestedNames
+thinNestedNames (MkNested ns) sub
+    = MkNested $ ns <&> \(n, nm, vars, rep) =>
+        (n, nm, flip thin sub <$> vars, flip thin sub .: rep)
+
 -- replace nested name with full name
 export
 mapNestedName : NestedNames vars -> Name -> Name

tests/idris2/basic/basic044/expected

@@ -62,6 +62,7 @@ LOG unify.equal:10: Skipped unification (equal already): Type and Type
 LOG unify.equal:10: Skipped unification (equal already): Type and Type
 LOG unify.equal:10: Skipped unification (equal already): Type and Type
 LOG declare.def.lhs:3: LHS term: Term.Typ
+LOG declare.def.lhs:3: LHS term after extension: Term.Typ
 LOG unify.equal:10: Skipped unification (equal already): (vars : $resolved1) -> Type and (vars : $resolved1) -> Type
 LOG declare.def.clause:3: RHS term: Term.Chk
 LOG declare.def:2: Case tree for Term.Typ: [0] Term.Chk
@@ -74,6 +75,7 @@ LOG unify.equal:10: Skipped unification (equal already): Type and Type
 LOG unify.equal:10: Skipped unification (equal already): Type and Type
 LOG unify.equal:10: Skipped unification (equal already): Type and Type
 LOG declare.def.lhs:3: LHS term: Term.Term
+LOG declare.def.lhs:3: LHS term after extension: Term.Term
 LOG unify.equal:10: Skipped unification (equal already): Type and Type
 LOG declare.def.clause:3: RHS term: (Term.Chk Prelude.Basics.True)
 LOG declare.def:2: Case tree for Term.Term: [0] (Term.Chk Prelude.Basics.True)
@@ -86,6 +88,7 @@ LOG unify.equal:10: Skipped unification (equal already): Type and Type
 LOG unify.equal:10: Skipped unification (equal already): Type and Type
 LOG unify.equal:10: Skipped unification (equal already): Type and Type
 LOG declare.def.lhs:3: LHS term: Term.NF
+LOG declare.def.lhs:3: LHS term after extension: Term.NF
 LOG unify.equal:10: Skipped unification (equal already): Type and Type
 LOG declare.def.clause:3: RHS term: (Term.Chk Prelude.Basics.False)
 LOG declare.def:2: Case tree for Term.NF: [0] (Term.Chk Prelude.Basics.False)

tests/idris2/casetree/dotInferred001/Main.idr

@@ -0,0 +1,5 @@
+import Data.Vect
+
+0 foo : Vect n a -> Int
+foo [x, y, z] = 1
+foo _ = 2

tests/idris2/casetree/dotInferred001/expected

@@ -0,0 +1,17 @@
+1/1: Building Main (Main.idr)
+Main> 0 Main.foo
+Arguments [{arg:1}, {arg:2}, {arg:3}]
+Compile time tree: case {arg:3} of
+  (::) {e:1} {e:2} {e:3} {e:4} => case {e:4} of
+    (::) {e:5} {e:6} {e:7} {e:8} => case {e:8} of
+      (::) {e:9} {e:10} {e:11} {e:12} => case {e:12} of
+        Nil {e:13} => 1
+        _ => 2
+      _ => 2
+    _ => 2
+  _ => 2
+Erasable args: [0, 1]
+Inferrable args: [0, 1]
+Flags: covering
+Main> 
+Bye for now!

tests/idris2/casetree/dotInferred001/input

@@ -0,0 +1 @@
+:di foo

tests/idris2/casetree/dotInferred001/run

@@ -0,0 +1,3 @@
+. ../../../testutils.sh
+
+idris2 Main.idr < input

tests/idris2/casetree/dotInferred002/Main.idr

@@ -0,0 +1,18 @@
+import Data.Vect
+
+-- Check that `TTImp.ProcessDef.Dot` properly handles
+-- functions in parameters and where clauses
+
+parameters (str : String)
+  0 foo : Vect n a -> Int
+  foo [x, y, z] = 1
+  foo _ = 2
+
+bar : String -> ()
+bar str = ()
+  where
+    -- We can't print case tree for nested function,
+    -- so we just check that this function compiles
+    0 baz : Vect n a -> Int
+    baz [x, y, z] = 1
+    baz _ = 2