Detaggability under where clauses

Need to make sure we've got the right real name for the function - this
had previously only been tested in parameters blocks where the name
doesn't change.

src/TTImp/Elab/App.idr

@@ -99,6 +99,7 @@ getVarType rigc nest env fc x
                              do checkVisibleNS fc (fullname ndef) (visibility ndef)
                                 logTerm 10 ("Type of " ++ show n') tyenv
                                 logTerm 10 ("Expands to") tm
+                                log 10 $ "Arg length " ++ show arglen
                                 pure (tm, arglen, gnf env tyenv)
     where
       useVars : List (Term vars) -> Term vars -> Term vars
@@ -619,7 +620,10 @@ checkApp rig elabinfo nest env fc (IVar fc' n) expargs impargs exp
                           " to " ++ show expargs ++ "\n\tFunction type " ++
                           (show !(toFullNames fnty)) ++ "\n\tExpected app type "
                                 ++ show exptyt))
-        checkAppWith rig elabinfo nest env fc ntm nty (Just n, arglen) expargs impargs False exp
+        let fn = case lookup n (names nest) of
+                      Just (Just n', _) => n'
+                      _ => n
+        checkAppWith rig elabinfo nest env fc ntm nty (Just fn, arglen) expargs impargs False exp
   where
     isPrimName : List Name -> Name -> Bool
     isPrimName [] fn = False

src/TTImp/Elab/ImplicitBind.idr

@@ -225,7 +225,7 @@ push ofc n b tm = Bind ofc n b tm
 -- We only do this for variables named 'PV', since they are the unbound
 -- implicits, and we don't want to move any given by the programmer
 liftImps : BindMode -> (Term vars, Term vars) -> (Term vars, Term vars)
-liftImps (PI _) (tm, TType) = (liftImps' tm, TType)
+liftImps (PI _) (tm, TType fc) = (liftImps' tm, TType fc)
   where
     liftImps' : Term vars -> Term vars
     liftImps' (Bind fc (PV n i) (Pi c Implicit ty) sc)

src/TTImp/Elab/Prim.idr

@@ -1,4 +1,4 @@
-module TTImp.Elab.App
+module TTImp.Elab.Prim
 
 import Core.TT