diff --git a/CHANGELOG_NEXT.md b/CHANGELOG_NEXT.md
index 75d6684aa15..9858d86cab6 100644
--- a/CHANGELOG_NEXT.md
+++ b/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
 
diff --git a/idris2api.ipkg b/idris2api.ipkg
index a0f4831fe16..a7c9df704f3 100644
--- a/idris2api.ipkg
+++ b/idris2api.ipkg
@@ -279,6 +279,7 @@ modules =
     TTImp.ProcessDecls,
     TTImp.ProcessDecls.Totality,
     TTImp.ProcessDef,
+    TTImp.ProcessDef.Dot,
     TTImp.ProcessFnOpt,
     TTImp.ProcessParams,
     TTImp.ProcessRecord,
diff --git a/src/Core/Case/CaseBuilder.idr b/src/Core/Case/CaseBuilder.idr
index cb88ae857cc..e290184f0ee 100644
--- a/src/Core/Case/CaseBuilder.idr
+++ b/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 : _} ->
diff --git a/src/Core/TT/Term.idr b/src/Core/TT/Term.idr
index e68d634fcb9..b0de74a16a8 100644
--- a/src/Core/TT/Term.idr
+++ b/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
diff --git a/src/Core/TT/Var.idr b/src/Core/TT/Var.idr
index d5f370e8825..7a5ec94ed93 100644
--- a/src/Core/TT/Var.idr
+++ b/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
diff --git a/src/TTImp/Elab/App.idr b/src/TTImp/Elab/App.idr
index 9e992100ac4..f5534b2390e 100644
--- a/src/TTImp/Elab/App.idr
+++ b/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
diff --git a/src/TTImp/ProcessDef.idr b/src/TTImp/ProcessDef.idr
index b74e3920989..fbb4544aa69 100644
--- a/src/TTImp/ProcessDef.idr
+++ b/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:
diff --git a/src/TTImp/ProcessDef/Dot.idr b/src/TTImp/ProcessDef/Dot.idr
new file mode 100644
index 00000000000..e0af041578b
--- /dev/null
+++ b/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
diff --git a/src/TTImp/TTImp.idr b/src/TTImp/TTImp.idr
index 708ad506640..5b5f0624d09 100644
--- a/src/TTImp/TTImp.idr
+++ b/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
diff --git a/tests/idris2/basic/basic044/expected b/tests/idris2/basic/basic044/expected
index e6d7a545bdc..18c71a78436 100644
--- a/tests/idris2/basic/basic044/expected
+++ b/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)
diff --git a/tests/idris2/casetree/dotInferred001/Main.idr b/tests/idris2/casetree/dotInferred001/Main.idr
new file mode 100644
index 00000000000..81a063b253e
--- /dev/null
+++ b/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
diff --git a/tests/idris2/casetree/dotInferred001/expected b/tests/idris2/casetree/dotInferred001/expected
new file mode 100644
index 00000000000..ba39c553c9b
--- /dev/null
+++ b/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!
diff --git a/tests/idris2/casetree/dotInferred001/input b/tests/idris2/casetree/dotInferred001/input
new file mode 100644
index 00000000000..aad40bf263c
--- /dev/null
+++ b/tests/idris2/casetree/dotInferred001/input
@@ -0,0 +1 @@
+:di foo
diff --git a/tests/idris2/casetree/dotInferred001/run b/tests/idris2/casetree/dotInferred001/run
new file mode 100755
index 00000000000..7935482b8ca
--- /dev/null
+++ b/tests/idris2/casetree/dotInferred001/run
@@ -0,0 +1,3 @@
+. ../../../testutils.sh
+
+idris2 Main.idr < input
diff --git a/tests/idris2/casetree/dotInferred002/Main.idr b/tests/idris2/casetree/dotInferred002/Main.idr
new file mode 100644
index 00000000000..4915015ee3d
--- /dev/null
+++ b/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
diff --git a/tests/idris2/casetree/dotInferred002/expected b/tests/idris2/casetree/dotInferred002/expected
new file mode 100644
index 00000000000..6193ef56a4d
--- /dev/null
+++ b/tests/idris2/casetree/dotInferred002/expected
@@ -0,0 +1,17 @@
+1/1: Building Main (Main.idr)
+Main> 0 Main.foo
+Arguments [{arg:1}, {arg:2}, {arg:3}, {arg:4}]
+Compile time tree: case {arg:4} 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: [1, 2]
+Inferrable args: [1, 2]
+Flags: covering
+Main> 
+Bye for now!
diff --git a/tests/idris2/casetree/dotInferred002/input b/tests/idris2/casetree/dotInferred002/input
new file mode 100644
index 00000000000..aad40bf263c
--- /dev/null
+++ b/tests/idris2/casetree/dotInferred002/input
@@ -0,0 +1 @@
+:di foo
diff --git a/tests/idris2/casetree/dotInferred002/run b/tests/idris2/casetree/dotInferred002/run
new file mode 100755
index 00000000000..7935482b8ca
--- /dev/null
+++ b/tests/idris2/casetree/dotInferred002/run
@@ -0,0 +1,3 @@
+. ../../../testutils.sh
+
+idris2 Main.idr < input
diff --git a/tests/idris2/casetree/dotInferred003/Main.idr b/tests/idris2/casetree/dotInferred003/Main.idr
new file mode 100644
index 00000000000..cf4572a8065
--- /dev/null
+++ b/tests/idris2/casetree/dotInferred003/Main.idr
@@ -0,0 +1,6 @@
+import Data.Vect
+
+0 foo : Vect n a -> Bool -> Int
+foo [x, y, z] True = 1
+foo [x, y, z] False = 2
+foo {} = 3
diff --git a/tests/idris2/casetree/dotInferred003/expected b/tests/idris2/casetree/dotInferred003/expected
new file mode 100644
index 00000000000..ba67a8b1512
--- /dev/null
+++ b/tests/idris2/casetree/dotInferred003/expected
@@ -0,0 +1,20 @@
+1/1: Building Main (Main.idr)
+Main> 0 Main.foo
+Arguments [{arg:1}, {arg:2}, {arg:3}, {arg:4}]
+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} => case {arg:4} of
+          True => 1
+          False => 2
+          _ => 3
+        _ => 3
+      _ => 3
+    _ => 3
+  _ => 3
+Erasable args: [0, 1]
+Inferrable args: [0, 1]
+Flags: covering
+Main> 
+Bye for now!
diff --git a/tests/idris2/casetree/dotInferred003/input b/tests/idris2/casetree/dotInferred003/input
new file mode 100644
index 00000000000..aad40bf263c
--- /dev/null
+++ b/tests/idris2/casetree/dotInferred003/input
@@ -0,0 +1 @@
+:di foo
diff --git a/tests/idris2/casetree/dotInferred003/run b/tests/idris2/casetree/dotInferred003/run
new file mode 100755
index 00000000000..7935482b8ca
--- /dev/null
+++ b/tests/idris2/casetree/dotInferred003/run
@@ -0,0 +1,3 @@
+. ../../../testutils.sh
+
+idris2 Main.idr < input
diff --git a/tests/idris2/casetree/dotInferred004/Main.idr b/tests/idris2/casetree/dotInferred004/Main.idr
new file mode 100644
index 00000000000..591a2b2bc4a
--- /dev/null
+++ b/tests/idris2/casetree/dotInferred004/Main.idr
@@ -0,0 +1,2 @@
+0 fromString : (s : String) -> s = "()" -> ()
+fromString _ Refl = ()
diff --git a/tests/idris2/casetree/dotInferred004/expected b/tests/idris2/casetree/dotInferred004/expected
new file mode 100644
index 00000000000..fe1f1a37196
--- /dev/null
+++ b/tests/idris2/casetree/dotInferred004/expected
@@ -0,0 +1,15 @@
+1/1: Building Main (Main.idr)
+Main> 0 Main.fromString
+Arguments [{arg:1}, {arg:2}]
+Compile time tree: case {arg:2} of
+  Refl {e:1} {e:2} => ()
+Detaggable arg types: [1]
+Refers to: Builtin.MkUnit
+Refers to (runtime): Builtin.MkUnit
+Flags: allguarded, covering
+Size change:
+  Builtin.MkUnit:
+    l
+  r +
+Main> 
+Bye for now!
diff --git a/tests/idris2/casetree/dotInferred004/input b/tests/idris2/casetree/dotInferred004/input
new file mode 100644
index 00000000000..fbb6d94c6e9
--- /dev/null
+++ b/tests/idris2/casetree/dotInferred004/input
@@ -0,0 +1 @@
+:di Main.fromString
diff --git a/tests/idris2/casetree/dotInferred004/run b/tests/idris2/casetree/dotInferred004/run
new file mode 100755
index 00000000000..7935482b8ca
--- /dev/null
+++ b/tests/idris2/casetree/dotInferred004/run
@@ -0,0 +1,3 @@
+. ../../../testutils.sh
+
+idris2 Main.idr < input
diff --git a/tests/idris2/casetree/dotInferred005/Main.idr b/tests/idris2/casetree/dotInferred005/Main.idr
new file mode 100644
index 00000000000..c610b654198
--- /dev/null
+++ b/tests/idris2/casetree/dotInferred005/Main.idr
@@ -0,0 +1,6 @@
+import Data.Vect
+
+0 foo : {n : Nat} -> {a : Type} -> (u : ()) ->
+        case u of () => Vect n a -> Int
+foo () [x, y, z] = 1
+foo () _ = 2
diff --git a/tests/idris2/casetree/dotInferred005/expected b/tests/idris2/casetree/dotInferred005/expected
new file mode 100644
index 00000000000..c221556c259
--- /dev/null
+++ b/tests/idris2/casetree/dotInferred005/expected
@@ -0,0 +1,17 @@
+1/1: Building Main (Main.idr)
+Main> 0 Main.foo
+Arguments [{arg:1}, {arg:2}, {arg:3}, {arg:4}]
+Compile time tree: case {arg:3} of
+  MkUnit => case {arg:4} 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
+Detaggable arg types: [2]
+Flags: covering
+Main> 
+Bye for now!
diff --git a/tests/idris2/casetree/dotInferred005/input b/tests/idris2/casetree/dotInferred005/input
new file mode 100644
index 00000000000..aad40bf263c
--- /dev/null
+++ b/tests/idris2/casetree/dotInferred005/input
@@ -0,0 +1 @@
+:di foo
diff --git a/tests/idris2/casetree/dotInferred005/run b/tests/idris2/casetree/dotInferred005/run
new file mode 100755
index 00000000000..7935482b8ca
--- /dev/null
+++ b/tests/idris2/casetree/dotInferred005/run
@@ -0,0 +1,3 @@
+. ../../../testutils.sh
+
+idris2 Main.idr < input
diff --git a/tests/idris2/casetree/dotInferred006/Main.idr b/tests/idris2/casetree/dotInferred006/Main.idr
new file mode 100644
index 00000000000..f2362563dec
--- /dev/null
+++ b/tests/idris2/casetree/dotInferred006/Main.idr
@@ -0,0 +1,11 @@
+0 foo : (a, b : Type) -> a === b -> Int
+foo (_ -> _) _ Refl = 1
+foo _ _ _ = 2
+
+0 bar : (a, b : Type) -> a === b -> Int
+bar (Int -> _) (_ -> _) Refl = 1
+bar _ _ _ = 2
+
+0 baz : (a, b : Type) -> a === b -> Int
+baz (Maybe Nat -> _) (Maybe _ -> _) Refl = 1
+baz _ _ _ = 2
diff --git a/tests/idris2/casetree/dotInferred006/expected b/tests/idris2/casetree/dotInferred006/expected
new file mode 100644
index 00000000000..4dc4a0c923f
--- /dev/null
+++ b/tests/idris2/casetree/dotInferred006/expected
@@ -0,0 +1,42 @@
+1/1: Building Main (Main.idr)
+Main> 0 Main.foo
+Arguments [{arg:1}, {arg:2}, {arg:3}]
+Compile time tree: case {arg:1} of
+  (->) {e:1} {e:2} => case {arg:3} of
+    Refl {e:3} {e:4} => 1
+    _ => 2
+  _ => 2
+Detaggable arg types: [2]
+Flags: covering
+Main> 0 Main.bar
+Arguments [{arg:1}, {arg:2}, {arg:3}]
+Compile time tree: case {arg:1} of
+  (->) {e:1} {e:2} => case {e:1} of
+    Int => case {arg:2} of
+      (->) {e:3} {e:4} => case {arg:3} of
+        Refl {e:5} {e:6} => 1
+        _ => 2
+      _ => 2
+    _ => 2
+  _ => 2
+Detaggable arg types: [2]
+Flags: covering
+Main> 0 Main.baz
+Arguments [{arg:1}, {arg:2}, {arg:3}]
+Compile time tree: case {arg:1} of
+  (->) {e:1} {e:2} => case {e:1} of
+    Maybe {e:3} => case {e:3} of
+      Nat => case {arg:2} of
+        (->) {e:4} {e:5} => case {e:4} of
+          Maybe {e:6} => case {arg:3} of
+            Refl {e:7} {e:8} => 1
+            _ => 2
+          _ => 2
+        _ => 2
+      _ => 2
+    _ => 2
+  _ => 2
+Detaggable arg types: [2]
+Flags: covering
+Main> 
+Bye for now!
diff --git a/tests/idris2/casetree/dotInferred006/input b/tests/idris2/casetree/dotInferred006/input
new file mode 100644
index 00000000000..eaecb862ca2
--- /dev/null
+++ b/tests/idris2/casetree/dotInferred006/input
@@ -0,0 +1,3 @@
+:di foo
+:di bar
+:di baz
diff --git a/tests/idris2/casetree/dotInferred006/run b/tests/idris2/casetree/dotInferred006/run
new file mode 100755
index 00000000000..7935482b8ca
--- /dev/null
+++ b/tests/idris2/casetree/dotInferred006/run
@@ -0,0 +1,3 @@
+. ../../../testutils.sh
+
+idris2 Main.idr < input
diff --git a/tests/idris2/casetree/dotInferred007/Main.idr b/tests/idris2/casetree/dotInferred007/Main.idr
new file mode 100644
index 00000000000..d5df944f058
--- /dev/null
+++ b/tests/idris2/casetree/dotInferred007/Main.idr
@@ -0,0 +1,5 @@
+import Data.Vect
+
+0 foo : Vect n a -> Int
+foo v@[x, y, z] = 1
+foo _ = 2
diff --git a/tests/idris2/casetree/dotInferred007/expected b/tests/idris2/casetree/dotInferred007/expected
new file mode 100644
index 00000000000..ba39c553c9b
--- /dev/null
+++ b/tests/idris2/casetree/dotInferred007/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!
diff --git a/tests/idris2/casetree/dotInferred007/input b/tests/idris2/casetree/dotInferred007/input
new file mode 100644
index 00000000000..aad40bf263c
--- /dev/null
+++ b/tests/idris2/casetree/dotInferred007/input
@@ -0,0 +1 @@
+:di foo
diff --git a/tests/idris2/casetree/dotInferred007/run b/tests/idris2/casetree/dotInferred007/run
new file mode 100755
index 00000000000..7935482b8ca
--- /dev/null
+++ b/tests/idris2/casetree/dotInferred007/run
@@ -0,0 +1,3 @@
+. ../../../testutils.sh
+
+idris2 Main.idr < input
diff --git a/tests/idris2/casetree/dotInferred008/Main.idr b/tests/idris2/casetree/dotInferred008/Main.idr
new file mode 100644
index 00000000000..f97a9da977d
--- /dev/null
+++ b/tests/idris2/casetree/dotInferred008/Main.idr
@@ -0,0 +1,16 @@
+import Data.Vect
+
+0 pair : (Int, Int) -> Int
+pair (x, y) = 1
+
+0 pairVect : (Vect n Int, Vect m Int) -> Int
+pairVect ([x, y], [z, w]) = 1
+pairVect _ = 2
+
+0 dpair : (t ** Maybe t) -> Int
+dpair (Bool ** Just y) = 1
+dpair _ = 2
+
+0 dpairVect : (t ** Vect n t) -> Int
+dpairVect (Bool ** [y, z]) = 1
+dpairVect _ = 2
diff --git a/tests/idris2/casetree/dotInferred008/expected b/tests/idris2/casetree/dotInferred008/expected
new file mode 100644
index 00000000000..383888d0492
--- /dev/null
+++ b/tests/idris2/casetree/dotInferred008/expected
@@ -0,0 +1,57 @@
+1/1: Building Main (Main.idr)
+Main> 0 Main.pair
+Arguments [{arg:1}]
+Compile time tree: case {arg:1} of
+  MkPair {e:1} {e:2} {e:3} {e:4} => 1
+Detaggable arg types: [0]
+Flags: covering
+Main> 0 Main.pairVect
+Arguments [{arg:1}, {arg:2}, {arg:3}]
+Compile time tree: case {arg:3} of
+  MkPair {e:1} {e:2} {e:3} {e:4} => case {e:3} 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} => case {e:4} of
+          (::) {e:14} {e:15} {e:16} {e:17} => case {e:17} of
+            (::) {e:18} {e:19} {e:20} {e:21} => case {e:21} of
+              Nil {e:22} => 1
+              _ => 2
+            _ => 2
+          _ => 2
+        _ => 2
+      _ => 2
+    _ => 2
+  _ => 2
+Erasable args: [0, 1]
+Detaggable arg types: [2]
+Inferrable args: [0, 1]
+Flags: covering
+Main> 0 Main.dpair
+Arguments [{arg:1}]
+Compile time tree: case {arg:1} of
+  MkDPair {e:1} {e:2} {e:3} {e:4} => case {e:3} of
+    Bool => case {e:4} of
+      Just {e:5} {e:6} => 1
+      _ => 2
+    _ => 2
+  _ => 2
+Detaggable arg types: [0]
+Flags: covering
+Main> 0 Main.dpairVect
+Arguments [{arg:1}, {arg:2}]
+Compile time tree: case {arg:2} of
+  MkDPair {e:1} {e:2} {e:3} {e:4} => case {e:3} of
+    Bool => 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
+  _ => 2
+Erasable args: [0]
+Detaggable arg types: [1]
+Flags: covering
+Main> 
+Bye for now!
diff --git a/tests/idris2/casetree/dotInferred008/input b/tests/idris2/casetree/dotInferred008/input
new file mode 100644
index 00000000000..38fd9aa6940
--- /dev/null
+++ b/tests/idris2/casetree/dotInferred008/input
@@ -0,0 +1,4 @@
+:di pair
+:di pairVect
+:di dpair
+:di dpairVect
diff --git a/tests/idris2/casetree/dotInferred008/run b/tests/idris2/casetree/dotInferred008/run
new file mode 100755
index 00000000000..7935482b8ca
--- /dev/null
+++ b/tests/idris2/casetree/dotInferred008/run
@@ -0,0 +1,3 @@
+. ../../../testutils.sh
+
+idris2 Main.idr < input
diff --git a/tests/idris2/coverage/coverage032/Issue3357.idr b/tests/idris2/coverage/coverage032/Issue3357.idr
new file mode 100644
index 00000000000..91a9e04b858
--- /dev/null
+++ b/tests/idris2/coverage/coverage032/Issue3357.idr
@@ -0,0 +1,34 @@
+namespace PrimInt
+  0 oops : (0 x : Int) -> if x == 0 then Unit else Void
+  oops 0 = ()
+
+  boom : Void
+  boom = void (oops 1)
+
+namespace PrimString
+  0 oops : (0 x : String) -> if x == "" then Unit else Void
+  oops "" = ()
+
+  boom : Void
+  boom = void (oops "foo")
+
+namespace PrimTy
+  0 oops : (0 a : Type) -> a
+  oops Int = 0
+
+  boom : Void
+  boom = void (oops Void)
+
+namespace TyCon
+  0 oops : (0 a : Type) -> a
+  oops Nat = Z
+
+  boom : Void
+  boom = void (oops Void)
+
+namespace Type
+  0 oops : (0 a : Type) -> a
+  oops Type = Type
+
+  boom : Void
+  boom = void (oops Void)
diff --git a/tests/idris2/coverage/coverage032/expected b/tests/idris2/coverage/coverage032/expected
new file mode 100644
index 00000000000..a17bfa4d6e1
--- /dev/null
+++ b/tests/idris2/coverage/coverage032/expected
@@ -0,0 +1,118 @@
+1/1: Building Issue3357 (Issue3357.idr)
+Error: boom is not covering.
+
+Issue3357:5:3--5:14
+ 1 | namespace PrimInt
+ 2 |   0 oops : (0 x : Int) -> if x == 0 then Unit else Void
+ 3 |   oops 0 = ()
+ 4 | 
+ 5 |   boom : Void
+       ^^^^^^^^^^^
+
+Calls non covering function Main.PrimInt.oops
+Error: boom is not covering.
+
+Issue3357:12:3--12:14
+ 08 | namespace PrimString
+ 09 |   0 oops : (0 x : String) -> if x == "" then Unit else Void
+ 10 |   oops "" = ()
+ 11 | 
+ 12 |   boom : Void
+        ^^^^^^^^^^^
+
+Calls non covering function Main.PrimString.oops
+Error: boom is not covering.
+
+Issue3357:19:3--19:14
+ 15 | namespace PrimTy
+ 16 |   0 oops : (0 a : Type) -> a
+ 17 |   oops Int = 0
+ 18 | 
+ 19 |   boom : Void
+        ^^^^^^^^^^^
+
+Calls non covering function Main.PrimTy.oops
+Error: boom is not covering.
+
+Issue3357:26:3--26:14
+ 22 | namespace TyCon
+ 23 |   0 oops : (0 a : Type) -> a
+ 24 |   oops Nat = Z
+ 25 | 
+ 26 |   boom : Void
+        ^^^^^^^^^^^
+
+Calls non covering function Main.TyCon.oops
+Error: boom is not covering.
+
+Issue3357:33:3--33:14
+ 29 | namespace Type
+ 30 |   0 oops : (0 a : Type) -> a
+ 31 |   oops Type = Type
+ 32 | 
+ 33 |   boom : Void
+        ^^^^^^^^^^^
+
+Calls non covering function Main.Type.oops
+Error: oops is not covering.
+
+Issue3357:2:3--2:56
+ 1 | namespace PrimInt
+ 2 |   0 oops : (0 x : Int) -> if x == 0 then Unit else Void
+       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+Missing cases:
+    oops _
+
+Error: oops is not covering.
+
+Issue3357:9:3--9:60
+ 5 |   boom : Void
+ 6 |   boom = void (oops 1)
+ 7 | 
+ 8 | namespace PrimString
+ 9 |   0 oops : (0 x : String) -> if x == "" then Unit else Void
+       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+Missing cases:
+    oops _
+
+Error: oops is not covering.
+
+Issue3357:16:3--16:29
+ 12 |   boom : Void
+ 13 |   boom = void (oops "foo")
+ 14 | 
+ 15 | namespace PrimTy
+ 16 |   0 oops : (0 a : Type) -> a
+        ^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+Missing cases:
+    oops _
+
+Error: oops is not covering.
+
+Issue3357:23:3--23:29
+ 19 |   boom : Void
+ 20 |   boom = void (oops Void)
+ 21 | 
+ 22 | namespace TyCon
+ 23 |   0 oops : (0 a : Type) -> a
+        ^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+Missing cases:
+    oops _
+
+Error: oops is not covering.
+
+Issue3357:30:3--30:29
+ 26 |   boom : Void
+ 27 |   boom = void (oops Void)
+ 28 | 
+ 29 | namespace Type
+ 30 |   0 oops : (0 a : Type) -> a
+        ^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+Missing cases:
+    oops _
+
diff --git a/tests/idris2/coverage/coverage032/run b/tests/idris2/coverage/coverage032/run
new file mode 100755
index 00000000000..ea4b74ef3c3
--- /dev/null
+++ b/tests/idris2/coverage/coverage032/run
@@ -0,0 +1,4 @@
+. ../../../testutils.sh
+
+# expect a coverage error
+check Issue3357.idr