[TC] clean term in decompilation of goal

Author: FissoreD

apps/tc/elpi/ho_compile.elpi

@@ -375,13 +375,13 @@ namespace tc {
 
       decompile-problematic-term (fun N Ty Bo) L (fun N Ty' Bo') L3 :-
         (pi x\ fold-map (Bo x) [] (Bo' x) (Lx x)),
-        close-term-no-prune-ty Lx Ty L1,
+        close-term-no-prune-ty Lx {tc.compile.instance.clean-term Ty} L1,
         fold-map Ty L Ty' L2,
         std.append L2 L1 L3.
 
       decompile-problematic-term (prod N Ty Bo) L (prod N Ty' Bo') L3 :-
         (pi x\ fold-map (Bo x) [] (Bo' x) (Lx x)),
-        close-term-no-prune-ty Lx Ty L1,
+        close-term-no-prune-ty Lx {tc.compile.instance.clean-term Ty} L1,
         fold-map Ty L Ty' L2,
         std.append L2 L1 L3.