diff --git a/bootstrap/newt.js b/bootstrap/newt.js
index 4f7936d..d4a6cbe 100644
--- a/bootstrap/newt.js
+++ b/bootstrap/newt.js
@@ -2,7 +2,7 @@
 const bouncer = (f,ini) => { let obj = ini; while (obj.tag) obj = f(obj); return obj.h0 };
 const Lib_Types_errorMsg = ( _$$0 ) => { switch (_$$0.tag) { case 1: return _$$0.h2; case 0: return _$$0.h1; } };
 const Lib_Types_Lib_Common_HasFC$20Lib_Common_Error$2CgetFC = ( _$$0 ) => { switch (_$$0.tag) { case 1: return _$$0.h0; case 0: return _$$0.h0; } };
-const Lib_Common_Prelude_Show$20Lib_Common_FC$2Cshow = ( _$$0 ) => ((((((((((("") + (_$$0.h0)) + (":(")) + (Prelude_showInt((_$$0.h1.h0) + (1)))) + (":")) + (Prelude_showInt((_$$0.h1.h1) + (1)))) + ("-")) + (Prelude_showInt((_$$0.h1.h2) + (1)))) + (":")) + (Prelude_showInt((_$$0.h1.h3) + (2)))) + (")"));
+const Lib_Common_Prelude_Show$20Lib_Common_FC$2Cshow = ( _$$0 ) => ((((((((((("") + (_$$0.h0)) + (":")) + (Prelude_showInt((_$$0.h1.h0) + (1)))) + (":")) + (Prelude_showInt((_$$0.h1.h1) + (1)))) + ("--")) + (Prelude_showInt((_$$0.h1.h2) + (1)))) + (":")) + (Prelude_showInt((_$$0.h1.h3) + (2)))) + (""));
 const Prelude_showInt = (i) => String(i);
 const Node_exitFailure = (_, msg) => {
   console.log(msg);
@@ -549,7 +549,7 @@ const Lib_Elab_unify = ( _$$0, _$$1, _$$2, _$$3 ) => (Lib_Types_Prelude_Monad$20
 const Lib_Elab_unify_unifyRest_unifyRef_unifyVar_unifyLam_unifyMeta = ( _, _1, _2, _3, _4, _5, _6, _7, _8, _$$9, _$$10 ) => { switch (_$$10.tag) { case 3: switch (_$$9.tag) { case 3: { const sc$$17 = Lib_Common_Prelude_Eq$20Lib_Common_QName$2C_$3D$3D_(_$$9.h1, _$$10.h1); switch (sc$$17) { case 1: { const sc$$18 = Prelude_Prelude_Eq$20Prelude_Ordering$2C_$3D$3D_(Prelude_Prelude_Ord$20Prelude_Nat$2Ccompare(Data_SnocList_snoclen(null, _$$9.h2), Data_SnocList_snoclen(null, _$$10.h2)), 0); switch (sc$$18) { case 1: return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Elab_solve(_, _$$9.h1, _$$9.h2, Lib_Types_VMeta(_$$10.h0, _$$10.h1, _$$10.h2)), ( _9 ) => (Lib_Types_Prelude_Applicative$20Lib_Types_M$2Creturn(null, Lib_Elab_Prelude_Monoid$20Lib_Elab_UnifyResult$2Cneutral))); case 0: return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Elab_solve(_, _$$10.h1, _$$10.h2, Lib_Types_VMeta(_$$9.h0, _$$9.h1, _$$9.h2)), ( _9 ) => (Lib_Types_Prelude_Applicative$20Lib_Types_M$2Creturn(null, Lib_Elab_Prelude_Monoid$20Lib_Elab_UnifyResult$2Cneutral))); } break; } case 0: return Lib_Elab_unifySpine(_, _1, Lib_Common_Prelude_Eq$20Lib_Common_QName$2C_$3D$3D_(_$$9.h1, _$$10.h1), _$$9.h2, _$$10.h2); } break; } default: return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Elab_solve(_, _$$10.h1, _$$10.h2, _$$9), ( _9 ) => (Lib_Types_Prelude_Applicative$20Lib_Types_M$2Creturn(null, Lib_Elab_Prelude_Monoid$20Lib_Elab_UnifyResult$2Cneutral))); } break; default: switch (_$$9.tag) { case 3: return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Elab_solve(_, _$$9.h1, _$$9.h2, _$$10), ( _9 ) => (Lib_Types_Prelude_Applicative$20Lib_Types_M$2Creturn(null, Lib_Elab_Prelude_Monoid$20Lib_Elab_UnifyResult$2Cneutral))); default: return Lib_Elab_unify_unifyRest_unifyRef_unifyVar_unifyLam(_, _1, _2, _3, _4, _5, _6, _7, _$$9, _$$10); } break; } };
 const Lib_Elab_unify_unifyRest_unifyRef_unifyVar_unifyLam = ( _, _1, _2, _3, _4, _5, _6, _7, _$$8, _$$9 ) => { switch (_$$9.tag) { case 4: switch (_$$8.tag) { case 4: { const fresh = Lib_Types_VVar(_$$8.h0, Prelude_length$27(null, _), Prelude_Lin(null)); return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Eval_eval(Prelude__$3A$3A_(null, fresh, _$$8.h4.h0), _$$8.h4.h1), ( vappt ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Eval_eval(Prelude__$3A$3A_(null, fresh, _$$9.h4.h0), _$$9.h4.h1), ( vappt$27 ) => (Lib_Elab_unify(Prelude__$3A$3A_(null, fresh, _), _1, vappt, vappt$27))))); break; } default: return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_log(2, ( _8 ) => ((("ETA ") + (Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow(_$$8))) + (""))), ( _8 ) => { const fresh = Lib_Types_VVar(_$$9.h0, Prelude_length$27(null, _), Prelude_Lin(null)); return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Eval_vapp(_$$8, fresh), ( vappt ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Eval_eval(Prelude__$3A$3A_(null, fresh, _$$9.h4.h0), _$$9.h4.h1), ( vappt$27 ) => (Lib_Elab_unify(Prelude__$3A$3A_(null, fresh, _), _1, vappt, vappt$27))))); }); } break; default: switch (_$$8.tag) { case 4: return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_log(2, ( _8 ) => ((("ETA' ") + (Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow(_$$9))) + (""))), ( _8 ) => { const fresh = Lib_Types_VVar(_$$8.h0, Prelude_length$27(null, _), Prelude_Lin(null)); return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Eval_eval(Prelude__$3A$3A_(null, fresh, _$$8.h4.h0), _$$8.h4.h1), ( appt ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Eval_vapp(_$$9, fresh), ( vappt$27 ) => (Lib_Elab_unify(Prelude__$3A$3A_(null, fresh, _), _1, appt, vappt$27))))); }); default: return Lib_Elab_unify_unifyRest_unifyRef_unifyVar(_, _1, _2, _3, _4, _5, _6, _$$8, _$$9); } break; } };
 const Lib_Elab_unify_unifyRest_unifyRef_unifyVar = ( _, _1, _2, _3, _4, _5, _6, _$$7, _$$8 ) => { switch (_$$8.tag) { case 0: switch (_$$7.tag) { case 0: { const sc$$15 = Prelude_jsEq(null, _$$7.h1, _$$8.h1); switch (sc$$15) { case 1: return Lib_Types_MkM(null, ( _7 ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(_$$7.h0, (((("Failed to unify ") + (Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow(_$$7))) + (" and ")) + (Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow(_$$8))) + (""))), eta)))); case 0: return Lib_Elab_unifySpine(_, _1, Prelude_jsEq(null, _$$7.h1, _$$8.h1), _$$7.h2, _$$8.h2); } break; } default: switch (_$$8.h2.tag) { case 0: return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Eval_tryEval(_, _$$7), ( vt ) => { switch (vt.tag) { case 1: return Lib_Types_MkM(null, ( _7 ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(_$$8.h0, (((("Failed to unify ") + (Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow(_$$7))) + (" and ")) + (Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow(_$$8))) + (""))), eta)))); case 0: return Lib_Elab_unify(_, _1, vt.h1, _$$8); } }); default: return Lib_Elab_unify_unifyRest_unifyRef(_, _1, _2, _3, _4, _5, _$$7, _$$8); } break; } break; default: switch (_$$7.tag) { case 0: switch (_$$7.h2.tag) { case 0: return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Eval_tryEval(_, _$$8), ( vu ) => { switch (vu.tag) { case 1: return Lib_Types_MkM(null, ( _7 ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(_$$7.h0, (((("Failed to unify ") + (Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow(_$$7))) + (" and ")) + (Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow(_$$8))) + (""))), eta)))); case 0: return Lib_Elab_unify(_, _1, _$$7, vu.h1); } }); default: return Lib_Elab_unify_unifyRest_unifyRef(_, _1, _2, _3, _4, _5, _$$7, _$$8); } break; default: return Lib_Elab_unify_unifyRest_unifyRef(_, _1, _2, _3, _4, _5, _$$7, _$$8); } break; } };
-const Lib_Elab_unify_unifyRest_unifyRef = ( _, _1, _2, _3, _4, _5, _$$6, _$$7 ) => { switch (_$$7.tag) { case 1: switch (_$$6.tag) { case 1: return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Eval_tryEval(_, _$$6), ( $$sc ) => { switch ($$sc.tag) { case 1: return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Eval_tryEval(_, _$$7), ( $$sc1 ) => { switch ($$sc1.tag) { case 1: { const sc$$20 = Lib_Common_Prelude_Eq$20Lib_Common_QName$2C_$3D$3D_(_$$6.h1, _$$7.h1); switch (sc$$20) { case 1: return Lib_Types_MkM(null, ( _6 ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(_$$6.h0, (((("vref mismatch ") + (Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow(_$$6))) + (" =?= ")) + (Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow(_$$7))) + (""))), eta)))); case 0: return Lib_Elab_unifySpine(_, _1, Lib_Common_Prelude_Eq$20Lib_Common_QName$2C_$3D$3D_(_$$6.h1, _$$7.h1), _$$6.h2, _$$7.h2); } break; } case 0: return Lib_Elab_unify(_, _1, _$$6, $$sc1.h1); } }); case 0: return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_log(2, ( _6 ) => ((((("tryEval ") + (Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow(_$$6))) + (" to ")) + (Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow($$sc.h1))) + (""))), ( _6 ) => (Lib_Elab_unify(_, _1, $$sc.h1, _$$7))); } }); default: return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_log(2, ( _6 ) => ((((("expand ") + (Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow(_$$6))) + (" =?= %ref ")) + (Lib_Common_Prelude_Show$20Lib_Common_QName$2Cshow(_$$7.h1))) + (""))), ( _6 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_getTop, ( top ) => { const sc$$13 = Lib_TopContext_lookup(_$$7.h1, top); switch (sc$$13.tag) { case 0: switch (sc$$13.h1.h3.tag) { case 3: return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Eval_eval(Prelude_Nil(null), sc$$13.h1.h3.h0), ( vtm ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Eval_vappSpine(vtm, _$$7.h2), ( appvtm ) => (Lib_Elab_unify(_, _1, _$$6, appvtm))))); default: return Lib_Types_MkM(null, ( _7 ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(_$$7.h0, (((((("unify failed ") + (Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow(_$$6))) + (" =?= ")) + (Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow(_$$7))) + (" [no Fn]\n  env is ")) + (Prelude_joinBy(", ", Prelude_Prelude_Functor$20Prelude_List$2Cmap(null, null, Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow, _)))) + (""))), eta)))); } break; default: return Lib_Types_MkM(null, ( _7 ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(_$$7.h0, (((((("unify failed ") + (Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow(_$$6))) + (" =?= ")) + (Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow(_$$7))) + (" [no Fn]\n  env is ")) + (Prelude_joinBy(", ", Prelude_Prelude_Functor$20Prelude_List$2Cmap(null, null, Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow, _)))) + (""))), eta)))); } }))); } break; default: switch (_$$6.tag) { case 1: return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_log(2, ( _6 ) => ((((((("expand %ref ") + (Lib_Common_Prelude_Show$20Lib_Common_QName$2Cshow(_$$6.h1))) + (" ")) + (Prelude_joinBy(", ", Prelude_Prelude_Functor$20Prelude_List$2Cmap(null, null, Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow, Prelude__$3C$3E$3E_(null, _$$6.h2, Prelude_Nil(null)))))) + (" =?= ")) + (Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow(_$$7))) + (""))), ( _6 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_getTop, ( top ) => { const sc$$13 = Lib_TopContext_lookup(_$$6.h1, top); switch (sc$$13.tag) { case 0: switch (sc$$13.h1.h3.tag) { case 3: return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Eval_eval(Prelude_Nil(null), sc$$13.h1.h3.h0), ( vtm ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Eval_vappSpine(vtm, _$$6.h2), ( tmsp ) => (Lib_Elab_unify(_, _1, tmsp, _$$7))))); default: return Lib_Types_MkM(null, ( _7 ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(_$$6.h0, (((((("unify failed ") + (Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow(_$$6))) + (" [no Fn] =?= ")) + (Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow(_$$7))) + ("\n  env is ")) + (Prelude_joinBy(", ", Prelude_Prelude_Functor$20Prelude_List$2Cmap(null, null, Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow, _)))) + (""))), eta)))); } break; default: return Lib_Types_MkM(null, ( _7 ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(_$$6.h0, (((((("unify failed ") + (Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow(_$$6))) + (" [no Fn] =?= ")) + (Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow(_$$7))) + ("\n  env is ")) + (Prelude_joinBy(", ", Prelude_Prelude_Functor$20Prelude_List$2Cmap(null, null, Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow, _)))) + (""))), eta)))); } }))); default: return Lib_Elab_unify_unifyRest(_, _1, _2, _3, _4, _$$6, _$$7); } break; } };
+const Lib_Elab_unify_unifyRest_unifyRef = ( _, _1, _2, _3, _4, _5, _$$6, _$$7 ) => { switch (_$$7.tag) { case 1: switch (_$$6.tag) { case 1: return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Eval_tryEval(_, _$$6), ( $$sc ) => { switch ($$sc.tag) { case 1: return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Eval_tryEval(_, _$$7), ( $$sc1 ) => { switch ($$sc1.tag) { case 1: { const sc$$20 = Lib_Common_Prelude_Eq$20Lib_Common_QName$2C_$3D$3D_(_$$6.h1, _$$7.h1); switch (sc$$20) { case 1: return Lib_Types_MkM(null, ( _6 ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(_$$6.h0, (((("vref mismatch ") + (Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow(_$$6))) + (" =?= ")) + (Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow(_$$7))) + (""))), eta)))); case 0: return Lib_Elab_unifySpine(_, _1, Lib_Common_Prelude_Eq$20Lib_Common_QName$2C_$3D$3D_(_$$6.h1, _$$7.h1), _$$6.h2, _$$7.h2); } break; } case 0: return Lib_Elab_unify(_, _1, _$$6, $$sc1.h1); } }); case 0: return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_log(2, ( _6 ) => ((((("tryEval ") + (Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow(_$$6))) + (" to ")) + (Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow($$sc.h1))) + (""))), ( _6 ) => (Lib_Elab_unify(_, _1, $$sc.h1, _$$7))); } }); default: return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_log(2, ( _6 ) => ((((("expand ") + (Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow(_$$6))) + (" =?= %ref ")) + (Lib_Common_Prelude_Show$20Lib_Common_QName$2Cshow(_$$7.h1))) + (""))), ( _6 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_getTop, ( top ) => { const sc$$13 = Lib_TopContext_lookup(_$$7.h1, top); switch (sc$$13.tag) { case 0: switch (sc$$13.h1.h3.tag) { case 3: return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Eval_eval(Prelude_Nil(null), sc$$13.h1.h3.h0), ( vtm ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Eval_vappSpine(vtm, _$$7.h2), ( appvtm ) => (Lib_Elab_unify(_, _1, _$$6, appvtm))))); default: return Lib_Types_MkM(null, ( _7 ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(_$$7.h0, (((("unify failed ") + (Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow(_$$6))) + (" =?= ")) + (Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow(_$$7))) + (" [no Fn]"))), eta)))); } break; default: return Lib_Types_MkM(null, ( _7 ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(_$$7.h0, (((("unify failed ") + (Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow(_$$6))) + (" =?= ")) + (Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow(_$$7))) + (" [no Fn]"))), eta)))); } }))); } break; default: switch (_$$6.tag) { case 1: return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_log(2, ( _6 ) => ((((((("expand %ref ") + (Lib_Common_Prelude_Show$20Lib_Common_QName$2Cshow(_$$6.h1))) + (" ")) + (Prelude_joinBy(", ", Prelude_Prelude_Functor$20Prelude_List$2Cmap(null, null, Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow, Prelude__$3C$3E$3E_(null, _$$6.h2, Prelude_Nil(null)))))) + (" =?= ")) + (Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow(_$$7))) + (""))), ( _6 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_getTop, ( top ) => { const sc$$13 = Lib_TopContext_lookup(_$$6.h1, top); switch (sc$$13.tag) { case 0: switch (sc$$13.h1.h3.tag) { case 3: return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Eval_eval(Prelude_Nil(null), sc$$13.h1.h3.h0), ( vtm ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Eval_vappSpine(vtm, _$$6.h2), ( tmsp ) => (Lib_Elab_unify(_, _1, tmsp, _$$7))))); default: return Lib_Types_MkM(null, ( _7 ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(_$$6.h0, (((("unify failed ") + (Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow(_$$6))) + (" [no Fn] =?= ")) + (Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow(_$$7))) + (""))), eta)))); } break; default: return Lib_Types_MkM(null, ( _7 ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(_$$6.h0, (((("unify failed ") + (Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow(_$$6))) + (" [no Fn] =?= ")) + (Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow(_$$7))) + (""))), eta)))); } }))); default: return Lib_Elab_unify_unifyRest(_, _1, _2, _3, _4, _$$6, _$$7); } break; } };
 const Lib_Elab_unify_unifyRest = ( _, _1, _2, _3, _4, _$$5, _$$6 ) => { switch (_$$6.tag) { case 10: switch (_$$5.tag) { case 10: { const sc$$11 = Lib_Types_Prelude_Eq$20Lib_Types_Literal$2C_$3D$3D_(_$$5.h1, _$$6.h1); switch (sc$$11) { case 1: return Lib_Types_MkM(null, ( _5 ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(_$$5.h0, (((("unify failed ") + (Lib_Types_Prelude_Show$20Lib_Types_Literal$2Cshow(_$$5.h1))) + (" =?= ")) + (Lib_Types_Prelude_Show$20Lib_Types_Literal$2Cshow(_$$6.h1))) + (""))), eta)))); case 0: return Lib_Types_Prelude_Applicative$20Lib_Types_M$2Creturn(null, Lib_Elab_Prelude_Monoid$20Lib_Elab_UnifyResult$2Cneutral); } break; } default: return Lib_Types_MkM(null, ( _5 ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(Lib_Types_getValFC(_$$5), (((((("unify failed ") + (Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow(_$$5))) + (" =?= ")) + (Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow(_$$6))) + (" \n  env is ")) + (Prelude_joinBy(", ", Prelude_Prelude_Functor$20Prelude_List$2Cmap(null, null, Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow, _)))) + (""))), eta)))); } break; case 8: switch (_$$5.tag) { case 8: return Lib_Types_Prelude_Applicative$20Lib_Types_M$2Creturn(null, Lib_Elab_Prelude_Monoid$20Lib_Elab_UnifyResult$2Cneutral); default: return Lib_Types_MkM(null, ( _5 ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(Lib_Types_getValFC(_$$5), (((((("unify failed ") + (Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow(_$$5))) + (" =?= ")) + (Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow(_$$6))) + (" \n  env is ")) + (Prelude_joinBy(", ", Prelude_Prelude_Functor$20Prelude_List$2Cmap(null, null, Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow, _)))) + (""))), eta)))); } break; case 5: switch (_$$5.tag) { case 5: { const fresh = Lib_Types_VVar(_$$5.h0, Prelude_length$27(null, _), Prelude_Lin(null)); return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Eval_eval(Prelude__$3A$3A_(null, fresh, _$$5.h5.h0), _$$5.h5.h1), ( xb ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Eval_eval(Prelude__$3A$3A_(null, fresh, _$$6.h5.h0), _$$6.h5.h1), ( xb$27 ) => (Lib_Types_Prelude_Applicative$20Lib_Types_M$2C_$3C$2A$3E_(null, null, Lib_Types_Prelude_Functor$20Lib_Types_M$2Cmap(null, null, ( eta ) => (( eta1 ) => (Lib_Elab_Prelude_Semigroup$20Lib_Elab_UnifyResult$2C_$3C$2B$3E_(eta, eta1))), Lib_Elab_unify(_, _1, _$$5.h4, _$$6.h4)), Lib_Elab_unify(Prelude__$3A$3A_(null, fresh, _), _1, xb, xb$27)))))); break; } default: return Lib_Types_MkM(null, ( _5 ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(Lib_Types_getValFC(_$$5), (((((("unify failed ") + (Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow(_$$5))) + (" =?= ")) + (Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow(_$$6))) + (" \n  env is ")) + (Prelude_joinBy(", ", Prelude_Prelude_Functor$20Prelude_List$2Cmap(null, null, Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow, _)))) + (""))), eta)))); } break; default: return Lib_Types_MkM(null, ( _5 ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(Lib_Types_getValFC(_$$5), (((((("unify failed ") + (Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow(_$$5))) + (" =?= ")) + (Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow(_$$6))) + (" \n  env is ")) + (Prelude_joinBy(", ", Prelude_Prelude_Functor$20Prelude_List$2Cmap(null, null, Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow, _)))) + (""))), eta)))); } };
 const Lib_Types_getValFC = ( _$$0 ) => { switch (_$$0.tag) { case 10: return _$$0.h0; case 9: return _$$0.h0; case 8: return _$$0.h0; case 7: return _$$0.h0; case 6: return _$$0.h0; case 5: return _$$0.h0; case 4: return _$$0.h0; case 3: return _$$0.h0; case 2: return _$$0.h0; case 1: return _$$0.h0; case 0: return _$$0.h0; } };
 const Lib_Elab_Prelude_Semigroup$20Lib_Elab_UnifyResult$2C_$3C$2B$3E_ = ( _$$0, _$$1 ) => (Lib_Elab_MkResult(Prelude_Prelude_Concat$20$28Prelude_List$20BND$3A0$29$2C_$2B$2B_(null, _$$0.h0, _$$1.h0)));
@@ -759,15 +759,15 @@ const Lib_TopContext_addError = ( _$$0 ) => (Lib_Types_Prelude_Monad$20Lib_Types
 const Lib_ProcessDecl_processDecl = ( _$$0, _$$1 ) => { switch (_$$1.tag) { case 10: return Lib_ProcessDecl_processRecord(_$$0, _$$1.h0, _$$1.h1, _$$1.h2, _$$1.h3, _$$1.h4); case 9: return Lib_ProcessDecl_processInstance(_$$0, _$$1.h0, _$$1.h1, _$$1.h2); case 8: return Lib_ProcessDecl_processClass(_$$0, _$$1.h0, _$$1.h1, _$$1.h2, _$$1.h3); case 7: return Lib_Types_Prelude_Applicative$20Lib_Types_M$2Creturn(null, 0); case 6: return Lib_ProcessDecl_processPrimFn(_$$0, _$$1.h0, _$$1.h1, _$$1.h2, _$$1.h3, _$$1.h4); case 5: return Lib_ProcessDecl_processPrimType(_$$0, _$$1.h0, _$$1.h1, _$$1.h2); case 4: return Lib_ProcessDecl_processShortData(_$$0, _$$1.h0, _$$1.h1, _$$1.h2); case 3: return Lib_ProcessDecl_processData(_$$0, _$$1.h0, _$$1.h1, _$$1.h2, _$$1.h3); case 2: return Lib_ProcessDecl_processCheck(_$$0, _$$1.h0, _$$1.h1, _$$1.h2); case 1: return Lib_ProcessDecl_processDef(_$$0, _$$1.h0, _$$1.h1, _$$1.h2); case 0: return Lib_ProcessDecl_processTypeSig(_$$0, _$$1.h0, _$$1.h1, _$$1.h2); } };
 const Lib_ProcessDecl_processTypeSig = ( _$$0, _$$1, _$$2, _$$3 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_log(1, ( _ ) => ("-----")), ( _ ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_getTop, ( top ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Prelude_Prelude_Traversable$20Prelude_List$2Ctraverse(null, null, null, Lib_Types_Prelude_Applicative$20Lib_Types_M, ( eta ) => (Lib_ProcessDecl_checkAlreadyDef(_$$1, eta)), _$$2), ( _1 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Elab_check(Lib_Types_MkCtx(0, Prelude_Nil(null), Prelude_Nil(null), Prelude_Nil(null), _$$1), _$$3, Lib_Types_VU(_$$1)), ( ty ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_log(1, ( _2 ) => ((((("TypeSig ") + (Prelude_joinBy(" ", _$$2))) + (" : ")) + (Lib_Prettier_layout(Lib_Prettier_best(90, 0, Lib_Prettier_noAlt(Lib_Types_pprint$27(0, Prelude_Nil(null), ty))), Prelude_Lin(null)))) + (""))), ( _2 ) => (Lib_Types_Prelude_Functor$20Lib_Types_M$2Cmap(null, null, ( _$$31 ) => (0), Prelude_for(null, null, Prelude_Prelude_Traversable$20Prelude_List, Lib_Types_Prelude_Applicative$20Lib_Types_M, null, null, _$$2, ( nm ) => (Lib_TopContext_setDef(Lib_Common_QN(_$$0, nm), _$$1, ty, Lib_Types_Axiom, Prelude_Nil(null))))))))))))))));
 const Lib_Types_Axiom = { tag: 0 };
-const Lib_TopContext_setDef = ( _$$0, _$$1, _$$2, _$$3, _$$4 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_getTop, ( top ) => { const sc$$6 = Data_SortedMap_lookupMap$27(null, null, _$$0, top.h4); switch (sc$$6.tag) { case 1: return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_getTop, ( tc ) => { const defs = Data_SortedMap_updateMap(null, null, _$$0, Lib_Types_MkEntry(_$$1, _$$0, _$$2, _$$3, _$$4), top.h4); return Lib_Types_putTop(Lib_Types_MkTop(tc.h0, tc.h1, tc.h2, tc.h3, defs, tc.h5, tc.h6, tc.h7, tc.h8)); }); case 0: return Lib_Types_MkM(null, ( _ ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(_$$1, (((("") + (Lib_Common_Prelude_Show$20Lib_Common_QName$2Cshow(_$$0))) + (" is already defined at ")) + (Lib_Common_Prelude_Show$20Lib_Common_FC$2Cshow(sc$$6.h1.h0))) + (""))), eta)))); } }));
+const Lib_TopContext_setDef = ( _$$0, _$$1, _$$2, _$$3, _$$4 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_getTop, ( top ) => { const sc$$6 = Data_SortedMap_lookupMap$27(null, null, _$$0, top.h4); switch (sc$$6.tag) { case 1: return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_getTop, ( tc ) => (Lib_Types_putTop(Lib_Types_MkTop(tc.h0, tc.h1, tc.h2, tc.h3, Data_SortedMap_updateMap(null, null, _$$0, Lib_Types_MkEntry(_$$1, _$$0, _$$2, _$$3, _$$4), tc.h4), tc.h5, tc.h6, tc.h7, tc.h8)))); case 0: return Lib_Types_MkM(null, ( _ ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(_$$1, (((("") + (Lib_Common_Prelude_Show$20Lib_Common_QName$2Cshow(_$$0))) + (" is already defined at ")) + (Lib_Common_Prelude_Show$20Lib_Common_FC$2Cshow(sc$$6.h1.h0))) + (""))), eta)))); } }));
 const Lib_Types_MkEntry = ( h0, h1, h2, h3, h4 ) => ({ tag: 0,  h0: h0,  h1: h1,  h2: h2,  h3: h3,  h4: h4 });
 const Lib_ProcessDecl_checkAlreadyDef = ( _$$0, _$$1 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_getTop, ( top ) => { const sc$$3 = Lib_TopContext_lookupRaw(_$$1, top); switch (sc$$3.tag) { case 1: return Lib_Types_Prelude_Applicative$20Lib_Types_M$2Creturn(null, 0); case 0: return Lib_Types_MkM(null, ( _ ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(_$$0, (((("") + (_$$1)) + (" is already defined at ")) + (Lib_Common_Prelude_Show$20Lib_Common_FC$2Cshow(sc$$3.h1.h0))) + (""))), eta)))); } }));
 const Lib_ProcessDecl_processDef = ( _$$0, _$$1, _$$2, _$$3 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_log(1, ( _ ) => ("-----")), ( _ ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_log(1, ( _1 ) => ((("Def ") + (_$$2)) + (""))), ( _1 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_getTop, ( top ) => { const sc$$8 = Lib_TopContext_lookupRaw(_$$2, top); switch (sc$$8.tag) { case 1: return Lib_Types_MkM(null, ( _2 ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(_$$1, (("No declaration for ") + (_$$2)) + (""))), eta)))); case 0: switch (sc$$8.h1.h3.tag) { case 0: return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_log(1, ( _2 ) => ((((("check ") + (_$$2)) + (" at ")) + (Lib_Prettier_layout(Lib_Prettier_best(90, 0, Lib_Prettier_noAlt(Lib_Types_pprint$27(0, Prelude_Nil(null), sc$$8.h1.h2))), Prelude_Lin(null)))) + (""))), ( _2 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Eval_eval(Prelude_Nil(null), sc$$8.h1.h2), ( vty ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_log(2, ( _3 ) => ((((("") + (_$$2)) + (" vty is ")) + (Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow(vty))) + (""))), ( _3 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Prelude_Prelude_Traversable$20Prelude_List$2Ctraverse(null, null, null, Lib_Types_Prelude_Applicative$20Lib_Types_M, Lib_Elab_makeClause, _$$3), ( clauses$27 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Elab_buildTree(Lib_Types_MkCtx(0, Prelude_Nil(null), Prelude_Nil(null), Prelude_Nil(null), sc$$8.h1.h0), Lib_Elab_MkProb(clauses$27, vty)), ( tm ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Elab_solveAutos, ( _4 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_log(2, ( _5 ) => ((((((("Add def ") + (_$$2)) + (" ")) + (Lib_Prettier_layout(Lib_Prettier_best(90, 0, Lib_Prettier_noAlt(Lib_Types_pprint$27(0, Prelude_Nil(null), tm))), Prelude_Lin(null)))) + (" : ")) + (Lib_Prettier_layout(Lib_Prettier_best(90, 0, Lib_Prettier_noAlt(Lib_Types_pprint$27(0, Prelude_Nil(null), sc$$8.h1.h2))), Prelude_Lin(null)))) + (""))), ( _5 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_TopContext_updateDef(Lib_Common_QN(_$$0, _$$2), sc$$8.h1.h0, sc$$8.h1.h2, Lib_Types_Fn(tm)), ( _6 ) => { const name = Lib_Common_Prelude_Show$20Lib_Common_QName$2Cshow(Lib_Common_QN(_$$0, _$$2)); const sc$$26 = Prelude__$7C$7C_(Prelude_Prelude_Eq$20Prelude_Ordering$2C_$3D$3D_(Prelude_jsCompare(null, Lib_ProcessDecl_complexity(tm), 15), 0), Prelude__$7C$7C_(Prelude_jsEq(null, name, "Prelude.Prelude.Monad Prelude.IO,bind"), Prelude_jsEq(null, name, "Prelude._>>=_"))); switch (sc$$26) { case 1: return Lib_Types_Prelude_Applicative$20Lib_Types_M$2Creturn(null, 0); case 0: return Lib_TopContext_setFlag(Lib_Common_QN(_$$0, _$$2), sc$$8.h1.h0, 1); } }))))))))))))))); default: return Lib_Types_MkM(null, ( _2 ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(_$$1, (((("") + (_$$2)) + (" already defined at ")) + (Lib_Common_Prelude_Show$20Lib_Common_FC$2Cshow(sc$$8.h1.h0))) + (""))), eta)))); } break; } }))))));
-const Lib_TopContext_setFlag = ( _$$0, _$$1, _$$2 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_getTop, ( top ) => { const sc$$4 = Data_SortedMap_lookupMap$27(null, null, _$$0, top.h4); switch (sc$$4.tag) { case 1: return Lib_Types_MkM(null, ( _ ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(_$$1, (("") + (Lib_Common_Prelude_Show$20Lib_Common_QName$2Cshow(_$$0))) + (" not declared"))), eta)))); case 0: return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_getTop, ( tc ) => { const defs = Data_SortedMap_updateMap(null, null, _$$0, Lib_Types_MkEntry(sc$$4.h1.h0, _$$0, sc$$4.h1.h2, sc$$4.h1.h3, Prelude__$3A$3A_(null, _$$2, sc$$4.h1.h4)), tc.h4); return Lib_Types_putTop(Lib_Types_MkTop(tc.h0, tc.h1, tc.h2, tc.h3, defs, tc.h5, tc.h6, tc.h7, tc.h8)); }); } }));
+const Lib_TopContext_setFlag = ( _$$0, _$$1, _$$2 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_getTop, ( top ) => { const sc$$4 = Data_SortedMap_lookupMap$27(null, null, _$$0, top.h4); switch (sc$$4.tag) { case 1: return Lib_Types_MkM(null, ( _ ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(_$$1, (("") + (Lib_Common_Prelude_Show$20Lib_Common_QName$2Cshow(_$$0))) + (" not declared"))), eta)))); case 0: return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_getTop, ( tc ) => (Lib_Types_putTop(Lib_Types_MkTop(tc.h0, tc.h1, tc.h2, tc.h3, Data_SortedMap_updateMap(null, null, _$$0, Lib_Types_MkEntry(sc$$4.h1.h0, _$$0, sc$$4.h1.h2, sc$$4.h1.h3, Prelude__$3A$3A_(null, _$$2, sc$$4.h1.h4)), tc.h4), tc.h5, tc.h6, tc.h7, tc.h8)))); } }));
 const Lib_ProcessDecl_complexity = ( _$$0 ) => { switch (_$$0.tag) { case 10: return 0; case 7: switch (_$$0.h2.tag) { case 1: switch (_$$0.h2.h1.tag) { case 1: switch (_$$0.h2.h2.tag) { case 0: return ((1) + (Lib_ProcessDecl_complexity(_$$0.h1))) + (Lib_ProcessDecl_complexity(_$$0.h2.h1.h2)); default: return 100; } break; default: return 100; } break; default: return 100; } break; case 5: return 0; case 4: return Lib_ProcessDecl_complexity_go(_$$0, _$$0.h0, _$$0.h1, _$$0.h2, null, _$$0.h1, Lib_ProcessDecl_complexity(_$$0.h2)); case 3: return (1) + (Lib_ProcessDecl_complexity(_$$0.h4)); case 2: return 1; case 1: return 1; case 0: return 1; default: return 100; } };
 const Lib_ProcessDecl_complexity_go = ( _, _1, _2, _3, _4, _$$5, _$$6 ) => (bouncer(Lib_ProcessDecl_REC_complexity_go, { tag: 1,  h0: _,  h1: _1,  h2: _2,  h3: _3,  h4: _4,  h5: _$$5,  h6: _$$6 }));
 const Lib_ProcessDecl_REC_complexity_go = ( arg ) => { switch (arg.h5.tag) { case 4: return { tag: 1,  h0: arg.h0,  h1: arg.h1,  h2: arg.h2,  h3: arg.h3,  h4: arg.h4,  h5: arg.h5.h1,  h6: (arg.h6) + (Lib_ProcessDecl_complexity(arg.h5.h2)) }; case 2: return { tag: 0,  h0: 1 }; default: return { tag: 0,  h0: (arg.h6) + (Lib_ProcessDecl_complexity(arg.h5)) }; } };
-const Lib_TopContext_updateDef = ( _$$0, _$$1, _$$2, _$$3 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_getTop, ( top ) => { const sc$$5 = Data_SortedMap_lookupMap$27(null, null, _$$0, top.h4); switch (sc$$5.tag) { case 1: return Lib_Types_MkM(null, ( _ ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(_$$1, (("") + (Lib_Common_Prelude_Show$20Lib_Common_QName$2Cshow(_$$0))) + (" not declared"))), eta)))); case 0: return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_getTop, ( tc ) => { const defs = Data_SortedMap_updateMap(null, null, _$$0, Lib_Types_MkEntry(sc$$5.h1.h0, _$$0, _$$2, _$$3, sc$$5.h1.h4), tc.h4); return Lib_Types_putTop(Lib_Types_MkTop(tc.h0, tc.h1, tc.h2, tc.h3, defs, tc.h5, tc.h6, tc.h7, tc.h8)); }); } }));
+const Lib_TopContext_updateDef = ( _$$0, _$$1, _$$2, _$$3 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_getTop, ( top ) => { const sc$$5 = Data_SortedMap_lookupMap$27(null, null, _$$0, top.h4); switch (sc$$5.tag) { case 1: return Lib_Types_MkM(null, ( _ ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(_$$1, (("") + (Lib_Common_Prelude_Show$20Lib_Common_QName$2Cshow(_$$0))) + (" not declared"))), eta)))); case 0: return Lib_Types_putTop(Lib_Types_MkTop(top.h0, top.h1, top.h2, top.h3, Data_SortedMap_updateMap(null, null, _$$0, Lib_Types_MkEntry(sc$$5.h1.h0, _$$0, _$$2, _$$3, sc$$5.h1.h4), top.h4), top.h5, top.h6, top.h7, top.h8)); } }));
 const Lib_ProcessDecl_processCheck = ( _$$0, _$$1, _$$2, _$$3 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_log(1, ( _ ) => ("----- DCheck")), ( _ ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_getTop, ( top ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_info(_$$1, (((("check ") + (Lib_Syntax_Prelude_Show$20Lib_Syntax_Raw$2Cshow(_$$2))) + (" at ")) + (Lib_Syntax_Prelude_Show$20Lib_Syntax_Raw$2Cshow(_$$3))) + ("")), ( _1 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Elab_check(Lib_Types_MkCtx(0, Prelude_Nil(null), Prelude_Nil(null), Prelude_Nil(null), _$$1), _$$3, Lib_Types_VU(_$$1)), ( ty$27 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_Prelude_HasIO$20Lib_Types_M$2CliftIO(null, Prelude_primPutStrLn((("  got type ") + (Lib_Prettier_layout(Lib_Prettier_best(90, 0, Lib_Prettier_noAlt(Lib_Types_pprint$27(0, Prelude_Nil(null), ty$27))), Prelude_Lin(null)))) + (""))), ( _2 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Eval_eval(Prelude_Nil(null), ty$27), ( vty ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Elab_check(Lib_Types_MkCtx(0, Prelude_Nil(null), Prelude_Nil(null), Prelude_Nil(null), _$$1), _$$2, vty), ( res ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_Prelude_HasIO$20Lib_Types_M$2CliftIO(null, Prelude_primPutStrLn((("  got ") + (Lib_Prettier_layout(Lib_Prettier_best(90, 0, Lib_Prettier_noAlt(Lib_Types_pprint$27(0, Prelude_Nil(null), res))), Prelude_Lin(null)))) + (""))), ( _3 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Eval_eval(Prelude_Nil(null), res), ( eta ) => (Lib_Eval_quote(Prelude_length$27(null, Prelude_Nil(null)), eta))), ( norm ) => (Lib_Types_Prelude_HasIO$20Lib_Types_M$2CliftIO(null, Prelude_primPutStrLn((("  NF ") + (Lib_Prettier_layout(Lib_Prettier_best(90, 0, Lib_Prettier_noAlt(Lib_Types_pprint$27(0, Prelude_Nil(null), norm))), Prelude_Lin(null)))) + (""))))))))))))))))))))));
 const Lib_ProcessDecl_processData = ( _$$0, _$$1, _$$2, _$$3, _$$4 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_log(1, ( _ ) => ("-----")), ( _ ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_log(1, ( _1 ) => ((("Data ") + (_$$2)) + (""))), ( _1 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_getTop, ( top ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Elab_check(Lib_Types_MkCtx(0, Prelude_Nil(null), Prelude_Nil(null), Prelude_Nil(null), _$$1), _$$3, Lib_Types_VU(_$$1)), ( tyty ) => { const sc$$12 = Lib_TopContext_lookupRaw(_$$2, top); switch (sc$$12.tag) { case 1: return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_TopContext_setDef(Lib_Common_QN(_$$0, _$$2), _$$1, tyty, Lib_Types_Axiom, Prelude_Nil(null)), ( _2 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_Prelude_Functor$20Lib_Types_M$2Cmap(null, null, ( _$$31 ) => (Prelude_Prelude_Monad$20Prelude_List$2Cbind(null, null, _$$31, ( _$$11 ) => (_$$11))), Prelude_for(null, null, Prelude_Prelude_Traversable$20Prelude_List, Lib_Types_Prelude_Applicative$20Lib_Types_M, null, null, Prelude_enumerate(null, _$$4), ( x ) => { switch (x.h3.tag) { case 0: return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Prelude_Prelude_Traversable$20Prelude_List$2Ctraverse(null, null, null, Lib_Types_Prelude_Applicative$20Lib_Types_M, ( eta ) => (Lib_ProcessDecl_checkAlreadyDef(x.h3.h0, eta)), x.h3.h1), ( _3 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_log(2, ( _4 ) => ((((("check dcon ") + (Prelude_joinBy(", ", Prelude_Prelude_Functor$20Prelude_List$2Cmap(null, null, Prelude_Prelude_Show$20Prim_String$2Cshow, x.h3.h1)))) + (" ")) + (Lib_Syntax_Prelude_Show$20Lib_Syntax_Raw$2Cshow(x.h3.h2))) + (""))), ( _4 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Elab_check(Lib_Types_MkCtx(0, Prelude_Nil(null), Prelude_Nil(null), Prelude_Nil(null), x.h3.h0), x.h3.h2, Lib_Types_VU(x.h3.h0)), ( dty ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_log(2, ( _5 ) => ((((("dty ") + (Prelude_joinBy(", ", Prelude_Prelude_Functor$20Prelude_List$2Cmap(null, null, Prelude_Prelude_Show$20Prim_String$2Cshow, x.h3.h1)))) + (" is ")) + (Lib_Prettier_layout(Lib_Prettier_best(90, 0, Lib_Prettier_noAlt(Lib_Types_pprint$27(0, Prelude_Nil(null), dty))), Prelude_Lin(null)))) + (""))), ( _5 ) => { const sc$$26 = Lib_Util_splitTele(dty); const tnames = Prelude_reverse(null)(Prelude_Prelude_Functor$20Prelude_List$2Cmap(null, null, ( eta ) => (Lib_ProcessDecl_processData_binderName(_$$0, _$$1, _$$2, _$$3, _$$4, null, eta)), sc$$26.h3)); const sc$$32 = Lib_Util_funArgs(sc$$26.h2); switch (sc$$32.h2.tag) { case 1: return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Prelude_when(null, Lib_Types_Prelude_Applicative$20Lib_Types_M, Prelude_not(Lib_Common_Prelude_Eq$20Lib_Common_QName$2C_$3D$3D_(sc$$32.h2.h1, Lib_Common_QN(_$$0, _$$2))), ( _6 ) => (Lib_Types_MkM(null, ( _7 ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(Lib_Types_Lib_Common_HasFC$20Lib_Types_Tm$2CgetFC(sc$$26.h2), (((("Constructor codomain is ") + (Lib_Prettier_layout(Lib_Prettier_best(90, 0, Lib_Prettier_noAlt(Lib_Types_pprint$27(0, tnames, sc$$26.h2))), Prelude_Lin(null)))) + (" rather than ")) + (_$$2)) + (""))), eta)))))), ( _6 ) => (Lib_Types_Prelude_Applicative$20Lib_Types_M$2Creturn(null, Prelude_Prelude_Functor$20Prelude_List$2Cmap(null, null, ( nm$27 ) => (Lib_Types_MkEntry(x.h3.h0, Lib_Common_QN(_$$0, nm$27), dty, Lib_Types_DCon(x.h2, 0, Lib_Elab_getArity(dty), sc$$32.h2.h1), Prelude_Nil(null))), x.h3.h1)))); default: return Lib_Types_MkM(null, ( _6 ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(Lib_Types_Lib_Common_HasFC$20Lib_Types_Tm$2CgetFC(sc$$32.h2), (((("expected ") + (_$$2)) + (" got ")) + (Lib_Prettier_layout(Lib_Prettier_best(90, 0, Lib_Prettier_noAlt(Lib_Types_pprint$27(0, tnames, sc$$32.h2))), Prelude_Lin(null)))) + (""))), eta)))); } }))))))); default: return Lib_Types_MkM(null, ( _3 ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(Lib_Syntax_Lib_Common_HasFC$20Lib_Syntax_Decl$2CgetFC(x.h3), "expected constructor declaration")), eta)))); } })), ( entries ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Elab_solveAutos, ( _3 ) => { const entries1 = Lib_ProcessDecl_populateConInfo(entries); return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Prelude_for(null, null, Prelude_Prelude_Traversable$20Prelude_List, Lib_Types_Prelude_Applicative$20Lib_Types_M, null, null, entries1, ( $$case ) => (Lib_TopContext_setDef($$case.h1, $$case.h0, $$case.h2, $$case.h3, $$case.h4))), ( _4 ) => { const cnames = Prelude_Prelude_Functor$20Prelude_List$2Cmap(null, null, ( x ) => (x.h1), entries1); return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_log(1, ( _5 ) => ((((("setDef ") + (_$$2)) + ("  TCon ")) + (Prelude_joinBy(", ", Prelude_Prelude_Functor$20Prelude_List$2Cmap(null, null, Lib_Common_Prelude_Show$20Lib_Common_QName$2Cshow, cnames)))) + (""))), ( _5 ) => { const arity = Prelude_natToInt(Lib_Util_piArity(tyty)); return Lib_TopContext_updateDef(Lib_Common_QN(_$$0, _$$2), _$$1, tyty, Lib_Types_TCon(arity, cnames)); }); }); }))))); case 0: switch (sc$$12.h1.h3.tag) { case 0: return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Eval_eval(Prelude_Nil(null), tyty), ( tyty$27 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Eval_eval(Prelude_Nil(null), sc$$12.h1.h2), ( type$27 ) => (Lib_Elab_unifyCatch(_$$1, Lib_Types_MkCtx(0, Prelude_Nil(null), Prelude_Nil(null), Prelude_Nil(null), _$$1), tyty$27, type$27))))), ( _2 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_Prelude_Functor$20Lib_Types_M$2Cmap(null, null, ( _$$31 ) => (Prelude_Prelude_Monad$20Prelude_List$2Cbind(null, null, _$$31, ( _$$11 ) => (_$$11))), Prelude_for(null, null, Prelude_Prelude_Traversable$20Prelude_List, Lib_Types_Prelude_Applicative$20Lib_Types_M, null, null, Prelude_enumerate(null, _$$4), ( x ) => { switch (x.h3.tag) { case 0: return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Prelude_Prelude_Traversable$20Prelude_List$2Ctraverse(null, null, null, Lib_Types_Prelude_Applicative$20Lib_Types_M, ( eta ) => (Lib_ProcessDecl_checkAlreadyDef(x.h3.h0, eta)), x.h3.h1), ( _3 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_log(2, ( _4 ) => ((((("check dcon ") + (Prelude_joinBy(", ", Prelude_Prelude_Functor$20Prelude_List$2Cmap(null, null, Prelude_Prelude_Show$20Prim_String$2Cshow, x.h3.h1)))) + (" ")) + (Lib_Syntax_Prelude_Show$20Lib_Syntax_Raw$2Cshow(x.h3.h2))) + (""))), ( _4 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Elab_check(Lib_Types_MkCtx(0, Prelude_Nil(null), Prelude_Nil(null), Prelude_Nil(null), x.h3.h0), x.h3.h2, Lib_Types_VU(x.h3.h0)), ( dty ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_log(2, ( _5 ) => ((((("dty ") + (Prelude_joinBy(", ", Prelude_Prelude_Functor$20Prelude_List$2Cmap(null, null, Prelude_Prelude_Show$20Prim_String$2Cshow, x.h3.h1)))) + (" is ")) + (Lib_Prettier_layout(Lib_Prettier_best(90, 0, Lib_Prettier_noAlt(Lib_Types_pprint$27(0, Prelude_Nil(null), dty))), Prelude_Lin(null)))) + (""))), ( _5 ) => { const sc$$26 = Lib_Util_splitTele(dty); const tnames = Prelude_reverse(null)(Prelude_Prelude_Functor$20Prelude_List$2Cmap(null, null, ( eta ) => (Lib_ProcessDecl_processData_binderName(_$$0, _$$1, _$$2, _$$3, _$$4, null, eta)), sc$$26.h3)); const sc$$32 = Lib_Util_funArgs(sc$$26.h2); switch (sc$$32.h2.tag) { case 1: return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Prelude_when(null, Lib_Types_Prelude_Applicative$20Lib_Types_M, Prelude_not(Lib_Common_Prelude_Eq$20Lib_Common_QName$2C_$3D$3D_(sc$$32.h2.h1, Lib_Common_QN(_$$0, _$$2))), ( _6 ) => (Lib_Types_MkM(null, ( _7 ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(Lib_Types_Lib_Common_HasFC$20Lib_Types_Tm$2CgetFC(sc$$26.h2), (((("Constructor codomain is ") + (Lib_Prettier_layout(Lib_Prettier_best(90, 0, Lib_Prettier_noAlt(Lib_Types_pprint$27(0, tnames, sc$$26.h2))), Prelude_Lin(null)))) + (" rather than ")) + (_$$2)) + (""))), eta)))))), ( _6 ) => (Lib_Types_Prelude_Applicative$20Lib_Types_M$2Creturn(null, Prelude_Prelude_Functor$20Prelude_List$2Cmap(null, null, ( nm$27 ) => (Lib_Types_MkEntry(x.h3.h0, Lib_Common_QN(_$$0, nm$27), dty, Lib_Types_DCon(x.h2, 0, Lib_Elab_getArity(dty), sc$$32.h2.h1), Prelude_Nil(null))), x.h3.h1)))); default: return Lib_Types_MkM(null, ( _6 ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(Lib_Types_Lib_Common_HasFC$20Lib_Types_Tm$2CgetFC(sc$$32.h2), (((("expected ") + (_$$2)) + (" got ")) + (Lib_Prettier_layout(Lib_Prettier_best(90, 0, Lib_Prettier_noAlt(Lib_Types_pprint$27(0, tnames, sc$$32.h2))), Prelude_Lin(null)))) + (""))), eta)))); } }))))))); default: return Lib_Types_MkM(null, ( _3 ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(Lib_Syntax_Lib_Common_HasFC$20Lib_Syntax_Decl$2CgetFC(x.h3), "expected constructor declaration")), eta)))); } })), ( entries ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Elab_solveAutos, ( _3 ) => { const entries1 = Lib_ProcessDecl_populateConInfo(entries); return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Prelude_for(null, null, Prelude_Prelude_Traversable$20Prelude_List, Lib_Types_Prelude_Applicative$20Lib_Types_M, null, null, entries1, ( $$case ) => (Lib_TopContext_setDef($$case.h1, $$case.h0, $$case.h2, $$case.h3, $$case.h4))), ( _4 ) => { const cnames = Prelude_Prelude_Functor$20Prelude_List$2Cmap(null, null, ( x ) => (x.h1), entries1); return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_log(1, ( _5 ) => ((((("setDef ") + (_$$2)) + ("  TCon ")) + (Prelude_joinBy(", ", Prelude_Prelude_Functor$20Prelude_List$2Cmap(null, null, Lib_Common_Prelude_Show$20Lib_Common_QName$2Cshow, cnames)))) + (""))), ( _5 ) => { const arity = Prelude_natToInt(Lib_Util_piArity(tyty)); return Lib_TopContext_updateDef(Lib_Common_QN(_$$0, _$$2), _$$1, tyty, Lib_Types_TCon(arity, cnames)); }); }); }))))); default: return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_MkM(null, ( _2 ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(_$$1, (("") + (_$$2)) + (" already declared"))), eta)))), ( _2 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_Prelude_Functor$20Lib_Types_M$2Cmap(null, null, ( _$$31 ) => (Prelude_Prelude_Monad$20Prelude_List$2Cbind(null, null, _$$31, ( _$$11 ) => (_$$11))), Prelude_for(null, null, Prelude_Prelude_Traversable$20Prelude_List, Lib_Types_Prelude_Applicative$20Lib_Types_M, null, null, Prelude_enumerate(null, _$$4), ( x ) => { switch (x.h3.tag) { case 0: return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Prelude_Prelude_Traversable$20Prelude_List$2Ctraverse(null, null, null, Lib_Types_Prelude_Applicative$20Lib_Types_M, ( eta ) => (Lib_ProcessDecl_checkAlreadyDef(x.h3.h0, eta)), x.h3.h1), ( _3 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_log(2, ( _4 ) => ((((("check dcon ") + (Prelude_joinBy(", ", Prelude_Prelude_Functor$20Prelude_List$2Cmap(null, null, Prelude_Prelude_Show$20Prim_String$2Cshow, x.h3.h1)))) + (" ")) + (Lib_Syntax_Prelude_Show$20Lib_Syntax_Raw$2Cshow(x.h3.h2))) + (""))), ( _4 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Elab_check(Lib_Types_MkCtx(0, Prelude_Nil(null), Prelude_Nil(null), Prelude_Nil(null), x.h3.h0), x.h3.h2, Lib_Types_VU(x.h3.h0)), ( dty ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_log(2, ( _5 ) => ((((("dty ") + (Prelude_joinBy(", ", Prelude_Prelude_Functor$20Prelude_List$2Cmap(null, null, Prelude_Prelude_Show$20Prim_String$2Cshow, x.h3.h1)))) + (" is ")) + (Lib_Prettier_layout(Lib_Prettier_best(90, 0, Lib_Prettier_noAlt(Lib_Types_pprint$27(0, Prelude_Nil(null), dty))), Prelude_Lin(null)))) + (""))), ( _5 ) => { const sc$$26 = Lib_Util_splitTele(dty); const tnames = Prelude_reverse(null)(Prelude_Prelude_Functor$20Prelude_List$2Cmap(null, null, ( eta ) => (Lib_ProcessDecl_processData_binderName(_$$0, _$$1, _$$2, _$$3, _$$4, null, eta)), sc$$26.h3)); const sc$$32 = Lib_Util_funArgs(sc$$26.h2); switch (sc$$32.h2.tag) { case 1: return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Prelude_when(null, Lib_Types_Prelude_Applicative$20Lib_Types_M, Prelude_not(Lib_Common_Prelude_Eq$20Lib_Common_QName$2C_$3D$3D_(sc$$32.h2.h1, Lib_Common_QN(_$$0, _$$2))), ( _6 ) => (Lib_Types_MkM(null, ( _7 ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(Lib_Types_Lib_Common_HasFC$20Lib_Types_Tm$2CgetFC(sc$$26.h2), (((("Constructor codomain is ") + (Lib_Prettier_layout(Lib_Prettier_best(90, 0, Lib_Prettier_noAlt(Lib_Types_pprint$27(0, tnames, sc$$26.h2))), Prelude_Lin(null)))) + (" rather than ")) + (_$$2)) + (""))), eta)))))), ( _6 ) => (Lib_Types_Prelude_Applicative$20Lib_Types_M$2Creturn(null, Prelude_Prelude_Functor$20Prelude_List$2Cmap(null, null, ( nm$27 ) => (Lib_Types_MkEntry(x.h3.h0, Lib_Common_QN(_$$0, nm$27), dty, Lib_Types_DCon(x.h2, 0, Lib_Elab_getArity(dty), sc$$32.h2.h1), Prelude_Nil(null))), x.h3.h1)))); default: return Lib_Types_MkM(null, ( _6 ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(Lib_Types_Lib_Common_HasFC$20Lib_Types_Tm$2CgetFC(sc$$32.h2), (((("expected ") + (_$$2)) + (" got ")) + (Lib_Prettier_layout(Lib_Prettier_best(90, 0, Lib_Prettier_noAlt(Lib_Types_pprint$27(0, tnames, sc$$32.h2))), Prelude_Lin(null)))) + (""))), eta)))); } }))))))); default: return Lib_Types_MkM(null, ( _3 ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(Lib_Syntax_Lib_Common_HasFC$20Lib_Syntax_Decl$2CgetFC(x.h3), "expected constructor declaration")), eta)))); } })), ( entries ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Elab_solveAutos, ( _3 ) => { const entries1 = Lib_ProcessDecl_populateConInfo(entries); return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Prelude_for(null, null, Prelude_Prelude_Traversable$20Prelude_List, Lib_Types_Prelude_Applicative$20Lib_Types_M, null, null, entries1, ( $$case ) => (Lib_TopContext_setDef($$case.h1, $$case.h0, $$case.h2, $$case.h3, $$case.h4))), ( _4 ) => { const cnames = Prelude_Prelude_Functor$20Prelude_List$2Cmap(null, null, ( x ) => (x.h1), entries1); return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_log(1, ( _5 ) => ((((("setDef ") + (_$$2)) + ("  TCon ")) + (Prelude_joinBy(", ", Prelude_Prelude_Functor$20Prelude_List$2Cmap(null, null, Lib_Common_Prelude_Show$20Lib_Common_QName$2Cshow, cnames)))) + (""))), ( _5 ) => { const arity = Prelude_natToInt(Lib_Util_piArity(tyty)); return Lib_TopContext_updateDef(Lib_Common_QN(_$$0, _$$2), _$$1, tyty, Lib_Types_TCon(arity, cnames)); }); }); }))))); } break; } }))))))));
 const Lib_Types_TCon = ( h0, h1 ) => ({ tag: 1,  h0: h0,  h1: h1 });
@@ -827,7 +827,7 @@ const Lib_ProcessDecl_REC_processInstance_getFields_tenv_mkRHS = ( arg ) => { sw
 const Lib_ProcessDecl_processInstance_getFields = ( _, _1, _2, _3, _4, _$$5, _$$6, _$$7 ) => { switch (_$$5.tag) { case 5: switch (_$$5.h2) { case 1: return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_Prelude_Functor$20Lib_Types_M$2Cmap(null, null, ( eta ) => (Lib_Util_MkBinder(_$$5.h0, _$$5.h1, 1, _$$5.h3, eta)), Lib_Eval_quote(Prelude_length$27(null, _$$6), _$$5.h4)), ( bnd ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Eval_eval(Prelude__$3A$3A_(null, Lib_Types_VVar(_$$5.h0, Prelude_length$27(null, _$$6), Prelude_Lin(null)), _$$5.h5.h0), _$$5.h5.h1), ( appsc ) => (Lib_ProcessDecl_processInstance_getFields(_, _1, _2, _3, _4, appsc, _$$6, Prelude__$3A$3A_(null, bnd, _$$7)))))); default: return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Eval_eval(Prelude__$3A$3A_(null, Lib_Types_VVar(_$$5.h0, Prelude_length$27(null, _$$6), Prelude_Lin(null)), _$$5.h5.h0), _$$5.h5.h1), ( appsc ) => (Lib_ProcessDecl_processInstance_getFields(_, _1, _2, _3, _4, appsc, _$$6, _$$7))); } break; default: return Lib_Types_Prelude_Applicative$20Lib_Types_M$2Creturn(null, Prelude_reverse(null)(_$$7)); } };
 const Lib_ProcessDecl_processInstance_getFields_tenv_mkRHS_apply = ( _, _1, _2, _3, _4, _5, _6, _7, _$$8, _$$9 ) => { switch (_$$9.tag) { case 1: switch (_$$8.tag) { case 5: return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Eval_eval(Prelude__$3A$3A_(null, _$$9.h1, _$$8.h5.h0), _$$8.h5.h1), ( bx ) => (Lib_ProcessDecl_processInstance_getFields_tenv_mkRHS_apply(_, _1, _2, _3, _4, _5, _6, _7, bx, _$$9.h2))); default: return Lib_Types_MkM(null, ( _8 ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(_1, (("expected pi type ") + (Lib_Types_Prelude_Show$20Lib_Types_Val$2Cshow(_$$8))) + (""))), eta)))); } break; case 0: return Lib_Types_Prelude_Applicative$20Lib_Types_M$2Creturn(null, _$$8); } };
 const Lib_Types_showTm = Lib_Types_Prelude_Show$20Lib_Types_Tm$2Cshow;
-const Lib_TopContext_addHint = ( _$$0 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_getTop, ( top ) => { const sc$$2 = Lib_TopContext_lookup(_$$0, top); switch (sc$$2.tag) { case 1: return Lib_Types_Prelude_Applicative$20Lib_Types_M$2Creturn(null, 0); case 0: { const sc$$5 = Lib_TopContext_typeName(sc$$2.h1.h2); switch (sc$$5.tag) { case 1: return Lib_Types_MkM(null, ( _ ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(sc$$2.h1.h0, (("can't find tcon name for ") + (Lib_Common_Prelude_Show$20Lib_Common_QName$2Cshow(_$$0))) + (""))), eta)))); case 0: { const xs = Prelude_fromMaybe(null, Prelude_Nil(null), Data_SortedMap_lookupMap$27(null, null, sc$$5.h1, top.h2)); const hints = Data_SortedMap_updateMap(null, null, sc$$5.h1, Prelude__$3A$3A_(null, Prelude__$2C_(null, null, _$$0, sc$$2.h1.h2), xs), top.h2); return Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_putTop(Lib_Types_MkTop(top.h0, top.h1, hints, top.h3, top.h4, top.h5, top.h6, top.h7, top.h8)), ( _ ) => (Lib_Types_Prelude_Applicative$20Lib_Types_M$2Creturn(null, 0))); break; } } break; } } }));
+const Lib_TopContext_addHint = ( _$$0 ) => (Lib_Types_Prelude_Monad$20Lib_Types_M$2Cbind(null, null, Lib_Types_getTop, ( top ) => { const sc$$2 = Lib_TopContext_lookup(_$$0, top); switch (sc$$2.tag) { case 1: return Lib_Types_Prelude_Applicative$20Lib_Types_M$2Creturn(null, 0); case 0: { const sc$$5 = Lib_TopContext_typeName(sc$$2.h1.h2); switch (sc$$5.tag) { case 1: return Lib_Types_MkM(null, ( _ ) => (( eta ) => (Prelude_MkIORes(null, Prelude_Left(null, null, Lib_Common_E(sc$$2.h1.h0, (("can't find tcon name for ") + (Lib_Common_Prelude_Show$20Lib_Common_QName$2Cshow(_$$0))) + (""))), eta)))); case 0: { const xs = Prelude_fromMaybe(null, Prelude_Nil(null), Data_SortedMap_lookupMap$27(null, null, sc$$5.h1, top.h2)); const hints = Data_SortedMap_updateMap(null, null, sc$$5.h1, Prelude__$3A$3A_(null, Prelude__$2C_(null, null, _$$0, sc$$2.h1.h2), xs), top.h2); return Lib_Types_putTop(Lib_Types_MkTop(top.h0, top.h1, hints, top.h3, top.h4, top.h5, top.h6, top.h7, top.h8)); break; } } break; } } }));
 const Lib_TopContext_typeName = ( _$$0 ) => (bouncer(Lib_TopContext_REC_typeName, { tag: 1,  h0: _$$0 }));
 const Lib_TopContext_REC_typeName = ( arg ) => { switch (arg.h0.tag) { case 6: switch (arg.h0.h2) { case 1: return { tag: 0,  h0: Prelude_Nothing(null) }; default: return { tag: 1,  h0: arg.h0.h5 }; } break; case 4: return { tag: 1,  h0: arg.h0.h1 }; case 1: return { tag: 0,  h0: Prelude_Just(null, arg.h0.h1) }; default: return { tag: 0,  h0: Prelude_Nothing(null) }; } };
 const Lib_Util_Prelude_Show$20Lib_Util_Binder$2Cshow = ( _$$0 ) => ((((((("[") + (Lib_Types_Prelude_Show$20Lib_Types_Quant$2Cshow(_$$0.h3))) + ("")) + (_$$0.h1)) + (" ")) + (Lib_Types_Prelude_Show$20Lib_Types_Icit$2Cshow(_$$0.h2))) + (" : ...]"));