[ fix #1652 ] Save casefnty to TTC (#1686)

src/TTImp/Elab/Case.idr

@@ -211,6 +211,7 @@ caseBlock {vars} rigc elabinfo fc nest env scr scrtm scrty caseRig alts expected
 
          logEnv "elab.case" 10 "Case env" env
          logTermNF "elab.case" 2 ("Case function type: " ++ show casen) [] casefnty
+         traverse_ addToSave (keys (getMetas casefnty))
 
          -- If we've had to add implicits to the case type (because there
          -- were unbound implicits) then we're in a bit of a mess. Easiest

src/TTImp/Interactive/CaseSplit.idr

@@ -338,6 +338,7 @@ mkCase {c} {u} fn orig lhs_raw
                -- Fixes Issue #74. The problem is that if the function is defined in a sub module,
                -- then the current namespace (accessed by calling getNS) differs from the function
                -- namespace, therefore it is not considered visible by TTImp.Elab.App.checkVisibleNS
+               -- FIXME: Causes issue #1385
                setAllPublic True
 
                -- Use 'Rig0' since it might be a type level function, or it might

tests/Main.idr

@@ -79,7 +79,7 @@ idrisTestsInteractive = MkTestPool "Interactive editing" [] Nothing
        "interactive021", "interactive022", "interactive023", "interactive024",
        "interactive025", "interactive026", "interactive027", "interactive028",
        "interactive029", "interactive030", "interactive031", "interactive032",
-       "interactive033", "interactive034", "interactive035"]
+       "interactive033", "interactive034", "interactive035", "interactive036"]
 
 idrisTestsInterface : TestPool
 idrisTestsInterface = MkTestPool "Interface" [] Nothing

tests/idris2/interactive036/casefn.idr

@@ -0,0 +1,3 @@
+cfn : Bool -> Nat
+cfn = \case
+  bar => ?cfn_rhs

tests/idris2/interactive036/expected

@@ -0,0 +1,4 @@
+1/1: Building casefn (casefn.idr)
+Main>   False => ?cfn_rhs_1
+  True => ?cfn_rhs_2
+Main> Bye for now!

tests/idris2/interactive036/input

@@ -0,0 +1,2 @@
+:cs 3 3 bar
+:q

tests/idris2/interactive036/run

@@ -0,0 +1,3 @@
+$1 --no-color --console-width 0 --no-banner casefn.idr < input
+
+rm -rf build