print full names in linear checking

Author: andrevidela

src/Core/LinearCheck.idr

@@ -346,12 +346,12 @@ mutual
                       do Just _ <- lookupCtxtExact n (gamma defs)
                               | _ => undefinedName fc n
                          tfty <- getTerm gfty
-                         throw (GenericMsg fc ("Linearity checking failed on " ++ show f' ++
-                              " (" ++ show tfty ++ " not a function type)"))
+                         throw (GenericMsg fc ("Linearity checking failed on " ++ show !(toFullNames f') ++
+                              " (" ++ show !(toFullNames tfty) ++ " not a function type)"))
 
                 _ => do tfty <- getTerm gfty
-                        throw (GenericMsg fc ("Linearity checking failed on " ++ show f' ++
-                              " (" ++ show tfty ++ " not a function type)"))
+                        throw (GenericMsg fc ("Linearity checking failed on " ++ show !(toFullNames f') ++
+                              " (" ++ show !(toFullNames tfty) ++ " not a function type)"))
 
   lcheck rig erase env (As fc s as pat)
       = do (as', _, _) <- lcheck rig erase env as
@@ -671,7 +671,7 @@ mutual
            empty <- clearDefs defs
            ty <- quote empty env nty
            throw (GenericMsg fc ("Linearity checking failed on metavar "
-                      ++ show n ++ " (" ++ show ty
+                      ++ show !(toFullNames n) ++ " (" ++ show !(toFullNames ty)
                       ++ " not a function type)"))
   lcheckMeta rig erase env fc n idx [] chk nty
       = do defs <- get Ctxt