feat!: saturated constructors

[brprice]

We enforce all (value) constructors must be fully-saturated. They will no longer carry their indices, i.e. we will have Just True rather than Just @Bool True. This implies that their typing rules must change, since we currently use these indices to infer types.

This change will introduce much symmetry between constructions and pattern matching of ADTs. It will also make some expressions much more concise (especially lists) due to not having type applications.

[brprice]

(I'll grab this comment as a todo list/current status, leaving the OP as an overview of the PR).

Status: nothing to see here code-wise, just opening a PR for a place to put some notes whilst this is in development. This PR is work towards #870

Note to self: some messy wip is at https://github.com/hackworthltd/primer/tree/brprice/wip/saturated-constructors

Todo (perhaps some of this should go in the FR #870):

• Implementation:
  • I have done foldl' (TApp ()) t ts or foldlM tapp t ts a few times, when I should have used foldTApp or maybe mkTAppCon
• Ensure that writing foo : ? = Just 5 works
• Then ensure that refining the type hole works thus: foo : Maybe ? = Just 5 and then foo : Maybe Bool = Just {? 5 ?}
• If a student is playing with match expressions to understand them and writes match (Just 5 : ?) with ..., we'll automatically insert the annotation (assuming that constructors are checkable only), but can we do better than an empty hole? (Perhaps in the future, as there are other places we may want to do the same -- does this change make anything along these lines harder?)
• The easy rule is checkable-only:

      A ∋ t
----------------
Maybe A ∋ Just t

but it would be interesting to explore (for UX reasons) the synthesising rules

     ? ∋ t                   e ∈ S
----------------   or   ----------------
Just t ∈ Maybe ?        Just e ∈ Maybe S

both from a "hack this up for UX" and a "do it properly with decent metatheory" perspectives

• There are some things to explore around extra actions to provide (and these will be easier to think about when we have a prototype of this feature!):
  • A way to insert an eta-expanded ctor: λx. Just x, λx xs. Cons x xs
  • But that does not help to insert λxs. Cons 1 xs
  • Perhaps a generic λ-lift a hole: ...?... ~> λx. ...x... would be a nice abstraction, then one can insert a constructor to get Cons ? ? and then λ-lift each argument.
• What happens if one inserts a constructor inside a non-empty hole: this is a synthesisable position (why?), but constructors may only be checkable -- it would be bad UX to not offer the option there!

Roadmap:

• (Option 1a) modify the API first (have a special case that detects constructor-headed spines -- this would not ensure fully-saturated-ness, but this is only a temporary stopping point)
  • mostly done -- currently this PR, but CI fails
• Constructors can have (type and term) arguments, but not needed to be fully saturated, and still synthesisable. Expr = ... | Con Name [Type] [Expr], where Con "C" A x is equivalent to the tree (C @ A) $ x. Perhaps this can be added under a new name, with a pattern synonym for the old form, and this may help split the testsuite changes (although this is speculative).
  • mostly done -- see https://github.com/hackworthltd/primer/tree/brprice/wip/saturated-constructors, but needs cleaning up
• Enforce constructors being fully-saturated (but still synthesisable) -- this is mostly a TC change, but will have knock-on effects on documentation and the testsuite. It will also require the "insert a bare constructor" action to be removed -- (possibly the action change can happen up front, before the core is changed?).
  • mostly done -- see see https://github.com/hackworthltd/primer/tree/brprice/wip/saturated-constructors-fully, but needs cleaning up, and editing the FR to account for the newly-discovered actions (enter/exit constructor arguments)
• Enforce constructors being checkable, but still have type arguments. This is mostly a TC and Eval change, with knock-on effects on the testsuite and documentation. It will also require the "insert a saturated constructor" action to be offered in fewer places (although this too could happen up front).
  • mostly done -- see https://github.com/hackworthltd/primer/tree/brprice/wip/saturated-constructors-checkable, with similar caveats as above
  • I should do the eval changes for "scrutinees must have an annotation" in this stage. In my current wip branch it is lumped in the next stage.
• Drop the type arguments Expr = ... | Con Name [Expr]. This should be a simple change, but with a lot of churn.
  • mostly done -- see https://github.com/hackworthltd/primer/tree/brprice/wip/saturated-constructors-no-indices
• (Option 1b) modify the API last (render Cons x xs as a tree headed by APP -- we should have all the type information available from the TC, and can always put holes in the types if needed.)

[brprice]

Note that a polished version of this PR has been opened in the following 5 PRs: #958 #959 #960 #961 #962