Dougal Maclaurin

With the recent rewrite of the Imp lowering to use type-determined representations (#1173), this is shouldn't be too hard. The runtime representation of simplified types (base types, sums, products, dependent...

Yes, let's do it. I suggest we make it more like Haskell's "standalone deriving" at first because it will be simpler to implement if the compiler isn't responsible for figuring...

This is a good idea and we should do it. Especially now that our class hierarchies are growing deeper, with the recent addition of the `Data` class. Let's implement the...

I'd be happy to get rid of the function composition operator. We're leaning into a more pointful style anyway. But it's a bad error regardless. I think we shouldn't do...

Nice! > But it was a little sad adding extra type annotations. Sorry about that. Right now I'm trying to simplify the implementation above all else, which means cutting features....

It no longer crashes the compiler but it parses to something very unexpected: ``` def f : _ 0 \x. y = x y n = 0 > Error: variable...

I say let's do it!

> Pleasant generality or too confusing? I was wondering about this too. On the one hand, I could see it being especially useful in a repl setting where you've just...

Here's an implementation plan: we make a new construct at the grouping level, say `CDecl = .... | CPrevValue Group`, and we desugar `CExpr` followed by `CPrevValue` to `ULet` in...

I discussed this offline with @xnning and she helped me understand the problem. The effect rules we use during inference, which are stricter than the ones we use during checking,...