[ fix ] Don't include type of binder for let in addRefs

CHANGELOG.md

@@ -92,6 +92,9 @@
 
 * Constant folding of trivial let statements and `believe_me`.
 
+* Fixed an issue that caused total functions containing a `let` to be rejected
+  as not total.
+
 * Fixed a bug that caused holes to appear unexpectedly during quotation of dependent pairs.
 
 ### Library changes

src/Core/TT.idr

@@ -1843,7 +1843,7 @@ addRefs ua at ns (Meta fc n i xs)
     addRefsArgs ns [] = ns
     addRefsArgs ns (t :: ts) = addRefsArgs (addRefs ua at ns t) ts
 addRefs ua at ns (Bind fc x (Let _ c val ty) scope)
-    = addRefs ua at (addRefs ua at (addRefs ua at ns val) ty) scope
+    = addRefs ua at (addRefs ua at ns val) scope
 addRefs ua at ns (Bind fc x b scope)
     = addRefs ua at (addRefs ua at ns (binderType b)) scope
 addRefs ua at ns (App _ (App _ (Ref fc _ name) x) y)

tests/Main.idr

@@ -233,7 +233,7 @@ idrisTestsTotality = MkTestPool "Totality checking" [] Nothing
        "total001", "total002", "total003", "total004", "total005",
        "total006", "total007", "total008", "total009", "total010",
        "total011", "total012", "total013", "total014", "total015",
-       "total016", "total017", "total018", "total019"
+       "total016", "total017", "total018", "total019", "total020"
       ]
 
 -- This will only work with an Idris compiled via Chez or Racket, but at

tests/idris2/debug001/expected

@@ -75,7 +75,7 @@ Compiled: \ {arg:1}, {arg:2} => case {arg:2} of
   { Prelude.Basics.Lin {tag = 0} [nil] => Prelude.Basics.Lin {tag = 0} [nil]
   ; Prelude.Basics.(:<) {tag = 1} [cons] {e:2} {e:3} => let rest = Prelude.Types.SnocList.filter {arg:1} {e:2} incase {arg:1} {e:3} of  { 1 => Prelude.Basics.(:<) {tag = 1} [cons] rest {e:3}; 0 => rest}
   }
-Refers to: Prelude.Basics.SnocList, Prelude.Basics.Lin, Prelude.Types.SnocList.case block in filter, Prelude.Types.SnocList.filter
+Refers to: Prelude.Basics.Lin, Prelude.Types.SnocList.case block in filter, Prelude.Types.SnocList.filter
 Refers to (runtime): Prelude.Basics.Lin, Prelude.Basics.(:<), Prelude.Types.SnocList.filter
 Flags: total
 Size change: Prelude.Types.SnocList.filter: [Just (0, Same), Just (1, Same), Just (2, Smaller)]

tests/idris2/total020/Check.idr

@@ -0,0 +1,23 @@
+record RF infot where
+  constructor MkRF
+  info : infot
+  op : RF infot -> RF infot
+
+total
+test : RF a -> (a -> RF b) -> RF b
+test a f = let foo = f a.info in foo
+
+total
+test2 : RF a -> (a -> RF b) -> RF b
+test2 a f = f a.info
+
+total
+test3 : RF a -> (a -> RF b) -> RF b
+test3 a f = let foo = a in f foo.info
+
+total
+test4 : RF a -> (a -> RF b) -> RF b
+test4 a f = let foo : RF b
+                foo = f a.info
+             in foo
+

tests/idris2/total020/expected

@@ -0,0 +1 @@
+1/1: Building Check (Check.idr)

tests/idris2/total020/run

@@ -0,0 +1,3 @@
+rm -rf build
+
+$1 --no-color --console-width 0 --no-banner --check Check.idr