G. Allais

Yet another one using a distinct instance of the `Erased` issue: ```idris %default total data F : Type where MkFix : ((0 g : Type -> Type) -> g ===...

For the record: all but the `Wrap` example are now fixed. `Wrap` would need not just parameter but also variance tracking in the core.

I think this may be a duplicate of #2250

Shrunk: ```idris %default total boom : Nat -> Void boom (S x) = boom x boom x = boom x ``` Edit: looks like we're happy as soon as we...

Linter, please stop victimising us :sob:

I don't think it makes sense to remove it entirely: people will just write `_

wth is going on ```idris %default total data Tuple a = MkTuple a a ohno : Void ohno = (if True then MkTuple () else MkTuple ()) () ```

This bit of the parser is responsible: once we have seen `let` we commit to either a block of let-binders or a block of local definitions. We could instead allow...

Fighting the type errors but I have good hope I'll have something soon.

Isn't the problem under-constrained? There is no way to infer `a` from the type `x` ought to have.