An email from Matthew Pickering helped me realize that of course -dcore-lint works with a normal ghc build! So there's no infrastructure setup blocking this task!

With -dcore-lint, I made some strides here in commit fe00ce8 last night; the main target was Lacks constraint adjustments, which I knew were missing some casts.

In the process, I also learned the order that I had been assuming for the kind arguments was wrong for classes (e.g. Lacks, Lacks_Plus), but it was right for the dfuns. Lesson learned: always use -fprint-explicit-kinds with --show-iface for the dfuns and with :info for the classes.

As of that fe00ce8 commit, the latest unresolved -dcore-lint error is an out-of-scope cobox co var. I'm certainly not creating it directly (there are no U(plugin:coxswain,... in the Core Lint warning), but I have to wonder if my reckless use of UnivCo is violating some assumptions somewhere that's causing GHC to drop the co var binding or overlook this occurrence of it on a renaming/subst pass. I checked UnivCo for source comments looking for anything it should not be used for, but I didn't find an obvious explanation along those lines.

Note: I think #10 was due to bad coercions (manifesting as problematic Core simplifications) and it seems commit fe00ce8 "fixed" it.

So I'm labeling this issue as a Bug.

Note [Coercion evidence terms] in TcEvidence.hs lists an INVARIANT that the evidence for t1 ~# t2 must be built with EvCoercion. I'm very confident that I am instead building such evidence with a by-fiat EvCast, which sounds like it violates that invariant. I'm optimistic that this will help.

Bah. I misparsed the note; it doesn't rule out casting coboxes.

However, it does refer to Note [Bind new Givens immediately] in TcRnTypes.hs, which indicates that maybe I should be explicitly binding an evidence variable when adjusting given constraints of type t1 ~# t2...

Commit bfd5777 seems to have resolved this. Disclaimer: I've so far only tested it with a -DDEBUG from-source build of ghc-8.2.2-rc1.

The key change was:

 coxFiatCo :: Type -> Type -> Coercion
-coxFiatCo = mkUnivCo (PluginProv "coxswain") Representational
+coxFiatCo t1 t2
+  | eqType t1 t2 = mkNomReflCo t1
+  | otherwise = mkUnivCo (PluginProv "coxswain") Nominal t1 t2

 coxFiatCast :: Type -> Type -> EvTerm -> EvTerm
-coxFiatCast t0 t1 ev0 = EvCast ev0 (coxFiatCo t0 t1)
+coxFiatCast t0 t1 ev0
+  | Just (eq0,l0,r0) <- maybeEq t0
+  , Just (eq1,l1,r1) <- maybeEq t1
+  , not (eq1 `ltRole` eq0)  -- can downgrade eq0 to eq1
+  = EvCoercion $ downgradeRole eq1 eq0 $
+                  downgradeRole eq0 Nominal (coxFiatCo l1 l0)
+      `mkTransCo`
+                  evTermCoercion ev0
+      `mkTransCo`
+                  downgradeRole eq0 Nominal (coxFiatCo r0 r1)
+  | otherwise = EvCast ev0 $ downgradeRole Representational Nominal $ coxFiatCo t0 t1
+  where
+  maybeEq t = case classifyPredType t of
+    EqPred eq l r -> Just (eqRelRole eq,l,r)
+    _ -> Nothing

That is, prefer EvCoercion (TransCo U (TransCo co U)) to EvCast (EvCoercion co) U. That is in addition to simply being more careful about roles.