[ log ] Print only a name of a constructor during logging

src/Deriving/DepTyCheck/Util/Collections.idr

@@ -11,6 +11,7 @@ import public Data.SortedSet
 import public Data.Vect
 import public Data.Vect.Dependent
 
+import public Deriving.DepTyCheck.Util.Alternative
 import public Deriving.DepTyCheck.Util.Fin
 import public Deriving.DepTyCheck.Util.Syntax
 
@@ -72,6 +73,11 @@ inits' : (xs : List a) -> DVect xs.length $ \idx => Vect (S $ finToNat idx) a
 inits' []      = []
 inits' (x::xs) = [x] :: ((x ::) <$> inits' xs)
 
+export
+findLastIndex : (a -> Bool) -> (xs : List a) -> Maybe $ Fin xs.length
+findLastIndex f []      = Nothing
+findLastIndex f (x::xs) = FS <$> findLastIndex f xs <|> whenT (f x) FZ
+
 --- Transitive clojure stuff ---
 
 export covering

src/Deriving/DepTyCheck/Util/Reflection.idr

@@ -35,7 +35,10 @@ Interpolation TTImp where
 
 export
 SingleLogPosition Con where
-  logPosition con = "\{show con.name}"
+  logPosition con = do
+    let fullName = show con.name
+    let fullName' = unpack fullName
+    maybe fullName (pack . flip drop fullName' . finToNat) $ findLastIndex (== '.') fullName'
 
 ----------------------------------------------
 --- Compiler-based `TTImp` transformations ---