From ac0b5a3f3b0241fe5a4a98da11e258c939e8442e Mon Sep 17 00:00:00 2001
From: Ohad Kammar <ohad.kammar@ed.ac.uk>
Date: Mon, 27 Jul 2020 20:47:30 +0100
Subject: [PATCH] Take into account syntactic sub-singletons when dotting in
 patterns

When an erased pattern argument in a non-erased context is of a
datatype that has 0 or 1 constructors, there is no need to dot it
(i.e., require that the canonical term is inferred by other
dependencies): it has to be the unique constructor that appears in the
source.
---
 src/TTImp/Elab/App.idr | 27 +++++++++++++++++++++++----
 1 file changed, 23 insertions(+), 4 deletions(-)

diff --git a/src/TTImp/Elab/App.idr b/src/TTImp/Elab/App.idr
index e1685b740..c3fffab2d 100644
--- a/src/TTImp/Elab/App.idr
+++ b/src/TTImp/Elab/App.idr
@@ -315,11 +315,16 @@ mutual
               else pure ()
   checkPatTyValid fc defs env _ _ _ = pure ()
 
-  dotErased : {auto c : Ref Ctxt Defs} ->
+  dotErased : {auto c : Ref Ctxt Defs} -> (argty : NF vars) ->
               Maybe Name -> Nat -> ElabMode -> RigCount -> RawImp -> Core RawImp
-  dotErased mn argpos (InLHS lrig ) rig tm
+  dotErased argty mn argpos (InLHS lrig ) rig tm
       = if not (isErased lrig) && isErased rig
            then
+              -- if the argument type aty has a single constructor, there's no need 
+              -- to dot it
+              if length (!(possibleConstructors argty)) <= 1
+              then pure tm
+              else 
                 -- if argpos is an erased position of 'n', leave it, otherwise dot if
                 -- necessary
                 do defs <- get Ctxt
@@ -330,6 +335,20 @@ mutual
                       else pure $ dotTerm tm
            else pure tm
     where
+      
+      ||| Find the constructors of a normal form that is a fully
+      ||| applied type constructor
+      possibleConstructors : NF vars -> Core (List Name)
+      possibleConstructors (NApp _ (NRef (TyCon _ n) tycName) args) = 
+        if length args == n
+        then do defs <- get Ctxt
+                Just gdef <- lookupCtxtExact tycName (gamma defs)
+                | Nothing => pure []
+                let (TCon _ _ _ _ _ _ datacons _) = gdef.definition                                                   | _ => pure []
+                pure datacons
+        else pure []
+      possibleConstructors _ = pure []
+    
       dotTerm : RawImp -> RawImp
       dotTerm tm
           = case tm of
@@ -340,7 +359,7 @@ mutual
                  IAs _ _ _ (Implicit _ _) => tm
                  IAs fc p t arg => IAs fc p t (IMustUnify fc ErasedArg tm)
                  _ => IMustUnify (getFC tm) ErasedArg tm
-  dotErased _ _ _ _ tm = pure tm
+  dotErased _ _ _ _ _ tm = pure tm
 
   -- Check the rest of an application given the argument type and the
   -- raw argument. We choose elaboration order depending on whether we know
@@ -367,7 +386,7 @@ mutual
   checkRestApp rig argRig elabinfo nest env fc tm x aty sc
                (n, argpos) arg_in expargs impargs knownret expty
      = do defs <- get Ctxt
-          arg <- dotErased n argpos (elabMode elabinfo) argRig arg_in
+          arg <- dotErased aty n argpos (elabMode elabinfo) argRig arg_in
           kr <- if knownret
                    then pure True
                    else do sc' <- sc defs (toClosure defaultOpts env (Erased fc False))