[ debug ] logging for dotting decision

src/Core/Options/Log.idr

@@ -87,6 +87,7 @@ knownTopics = [
     ("elab", Nothing),
     ("elab.ambiguous", Nothing),
     ("elab.app.var", Nothing),
+    ("elab.app.dot", Just "Dealing with forced expressions when elaborating applications"),
     ("elab.app.lhs", Nothing),
     ("elab.as", Nothing),
     ("elab.bindnames", Nothing),

src/TTImp/Elab/App.idr

@@ -365,7 +365,12 @@ mutual
             -- if the argument type aty has a single constructor, there's no need
             -- to dot it
             defs <- get Ctxt
-            mconsCount <- countConstructors !(evalClosure defs argty)
+            nfargty <- evalClosure defs argty
+            mconsCount <- countConstructors nfargty
+            logNF "elab.app.dot" 50
+              "Found \{show mconsCount} constructors for type"
+              (mkEnv emptyFC vars)
+              nfargty
             if mconsCount == Just 1 || mconsCount == Just 0
               then pure tm
               else
@@ -378,6 +383,8 @@ mutual
                       else pure $ dotTerm tm
           else pure tm
     where
+      -- TODO: this seems too conservative. If we get back an expression stuck on a
+      -- meta, shouldn't we delay the check instead of declaring the tm dotted?
       ||| Count the constructors of a fully applied concrete datatype
       countConstructors : NF vars -> Core (Maybe Nat)
       countConstructors (NTCon _ tycName _ n args) =