[ fix #1831 ] Be more careful about checking primitive names

src/Core/Context.idr

@@ -2157,6 +2157,17 @@ export
 getPrimitiveNames : {auto c : Ref Ctxt Defs} -> Core (List Name)
 getPrimitiveNames = primNamesToList <$> getPrimNames
 
+export
+isPrimName : List Name -> Name -> Bool
+isPrimName prims given = let (ns, nm) = splitNS given in go ns nm prims where
+
+  go : Namespace -> Name -> List Name -> Bool
+  go ns nm [] = False
+  go ns nm (p :: ps)
+    = let (ns', nm') = splitNS p in
+      (nm' == nm && (ns' `isApproximationOf` ns))
+      || go ns nm ps
+
 export
 addLogLevel : {auto c : Ref Ctxt Defs} ->
               Maybe LogLevel -> Core ()

src/Core/Name.idr

@@ -128,6 +128,11 @@ displayName (CaseBlock outer _) = (Nothing, "case block in " ++ show outer)
 displayName (WithBlock outer _) = (Nothing, "with block in " ++ show outer)
 displayName (Resolved i) = (Nothing, "$resolved" ++ show i)
 
+export
+splitNS : Name -> (Namespace, Name)
+splitNS (NS ns nm) = mapFst (ns <.>) (splitNS nm)
+splitNS nm = (emptyNS, nm)
+
 --- Drop a namespace from a name
 export
 dropNS : Name -> Name

src/Core/Normalise.idr

@@ -348,7 +348,7 @@ normalisePrims : {auto c : Ref Ctxt Defs} -> {vs : _} ->
                  -- output only evaluated if primitive
                  Core (Maybe (Term vs))
 normalisePrims boundSafe viewConstant all prims n args tm env
-   = do let True = elem (dropNS !(getFullName n)) prims -- is a primitive
+   = do let True = isPrimName prims !(getFullName n) -- is a primitive
               | _ => pure Nothing
         let (mc :: _) = reverse args -- with at least one argument
               | _ => pure Nothing

src/Core/Termination.idr

@@ -186,8 +186,11 @@ mutual
                  do scs <- traverse (findSC defs env Guarded pats) args
                     pure (concat scs)
              (_, Ref fc Func fn, args) =>
-                 do Just ty <- lookupTyExact fn (gamma defs)
-                         | Nothing =>
+                 do logC "totality" 50 $
+                       pure $ "Looking up type of " ++ show !(toFullNames fn)
+                    Just ty <- lookupTyExact fn (gamma defs)
+                         | Nothing => do
+                              log "totality" 50 $ "Lookup failed"
                               findSCcall defs env Unguarded pats fc fn 0 args
                     arity <- getArity defs [] ty
                     findSCcall defs env Unguarded pats fc fn arity args
@@ -523,7 +526,8 @@ checkSC defs f args path
              let Unchecked = isTerminating (totality gdef)
                   | IsTerminating => pure IsTerminating
                   | _ => pure (NotTerminating (BadCall [fnCall sc]))
-             log "totality.termination.sizechange.checkCall" 8 $ "CheckCall Size Change Graph: " ++ show !(toFullNames (fnCall sc))
+             log "totality.termination.sizechange.checkCall" 8 $
+                "CheckCall Size Change Graph: " ++ show !(toFullNames (fnCall sc))
              term <- checkSC defs (fnCall sc) (mkArgs (fnArgs sc)) path
              let inpath = fnCall sc `elem` map fst path
              if not inpath

src/TTImp/Elab/Ambiguity.idr

@@ -104,11 +104,6 @@ expandAmbigName mode nest env orig args (IVar fc x) exp
     buildAlt f ((fc', Just (Just i), a) :: as)
         = buildAlt (INamedApp fc' f i a) as
 
-    isPrimName : List Name -> Name -> Bool
-    isPrimName [] fn = False
-    isPrimName (p :: ps) fn
-        = dropNS fn == p || isPrimName ps fn
-
     -- If it's not a constructor application, dot it
     wrapDot : Bool -> EState vars ->
               ElabMode -> Name -> List RawImp -> Def -> RawImp -> RawImp

src/TTImp/Elab/App.idr

@@ -827,7 +827,7 @@ checkApp rig elabinfo nest env fc (IVar fc' n) expargs autoargs namedargs exp
     -- as an expression because we'll normalise the function away and match on
     -- the result
     updateElabInfo prims (InLHS _) n [IPrimVal fc c] elabinfo =
-        do if elem (dropNS !(getFullName n)) prims
+        do if isPrimName prims !(getFullName n)
               then pure (record { elabMode = InExpr } elabinfo)
               else pure elabinfo
     updateElabInfo _ _ _ _ info = pure info

tests/Main.idr

@@ -51,7 +51,7 @@ idrisTestsCoverage = MkTestPool "Coverage checking" [] Nothing
        "coverage005", "coverage006", "coverage007", "coverage008",
        "coverage009", "coverage010", "coverage011", "coverage012",
        "coverage013", "coverage014", "coverage015", "coverage016",
-       "coverage017"]
+       "coverage017", "coverage018"]
 
 idrisTestsCasetree : TestPool
 idrisTestsCasetree = MkTestPool "Case tree building" [] Nothing

tests/idris2/coverage018/Issue1831_1.idr

@@ -0,0 +1,14 @@
+module Issue1831_1
+
+export
+fooFromInteger : Num x => Integer -> x
+fooFromInteger x = fromInteger (x + x)
+
+%integerLit Issue1831_1.fooFromInteger
+
+test : Nat
+test = 5 + 6
+
+test2 : Nat -> Bool
+test2 1 = True
+test2 _ = False

tests/idris2/coverage018/Issue1831_2.idr

@@ -0,0 +1,14 @@
+module Issue1831_2
+
+export
+fooFromInteger : Num x => Integer -> x
+fooFromInteger x = fromInteger (x + x)
+
+%integerLit fooFromInteger
+
+test : Nat
+test = 5 + 6
+
+test2 : Nat -> Bool
+test2 1 = True
+test2 _ = False

tests/idris2/coverage018/expected

@@ -0,0 +1,48 @@
+1/1: Building Issue1831_1 (Issue1831_1.idr)
+Issue1831_1> Issue1831_1.test2 ==> [{arg:0}];
+Compile time tree: case {arg:0}[0] : [__] of
+ { Prelude.Types.S {e:0} => case {e:0}[0] : [__] of
+   { Prelude.Types.S {e:1} => case {e:1}[0] : [__] of
+     { Prelude.Types.Z => [0] Prelude.Basics.True
+     | _ => [0] Prelude.Basics.False
+     }
+   | _ => [0] Prelude.Basics.False
+   }
+ | _ => [0] Prelude.Basics.False
+ }
+Run time tree: Error: ""
+RigW
+Erasable args: []
+Detaggable arg types: []
+Specialise args: []
+Inferrable args: []
+Compiled: [{arg:0}]: (%case !{arg:0} [(%constcase 0 0)] Just (%let {e:0} (-Integer [!{arg:0}, 1]) (%case !{e:0} [(%constcase 0 0)] Just (%let {e:1} (-Integer [!{e:0}, 1]) (%case !{e:1} [(%constcase 0 1)] Just 0)))))
+Refers to: [Prelude.Basics.True, Prelude.Basics.False]
+Refers to (runtime): []
+Flags: [allguarded, covering]
+Issue1831_1> 
+Bye for now!
+1/1: Building Issue1831_2 (Issue1831_2.idr)
+Issue1831_2> Issue1831_2.test2 ==> [{arg:0}];
+Compile time tree: case {arg:0}[0] : [__] of
+ { Prelude.Types.S {e:0} => case {e:0}[0] : [__] of
+   { Prelude.Types.S {e:1} => case {e:1}[0] : [__] of
+     { Prelude.Types.Z => [0] Prelude.Basics.True
+     | _ => [0] Prelude.Basics.False
+     }
+   | _ => [0] Prelude.Basics.False
+   }
+ | _ => [0] Prelude.Basics.False
+ }
+Run time tree: Error: ""
+RigW
+Erasable args: []
+Detaggable arg types: []
+Specialise args: []
+Inferrable args: []
+Compiled: [{arg:0}]: (%case !{arg:0} [(%constcase 0 0)] Just (%let {e:0} (-Integer [!{arg:0}, 1]) (%case !{e:0} [(%constcase 0 0)] Just (%let {e:1} (-Integer [!{e:0}, 1]) (%case !{e:1} [(%constcase 0 1)] Just 0)))))
+Refers to: [Prelude.Basics.True, Prelude.Basics.False]
+Refers to (runtime): []
+Flags: [allguarded, covering]
+Issue1831_2> 
+Bye for now!

tests/idris2/coverage018/input

@@ -0,0 +1,2 @@
+:di test2
+:q

tests/idris2/coverage018/run

@@ -0,0 +1,4 @@
+rm -rf build
+
+$1 --no-color --no-banner --console-width 0 Issue1831_1.idr < input
+$1 --no-color --no-banner --console-width 0 Issue1831_2.idr < input