Constructors as first-class citizen

[abooij]

module test where
import nat
suc' : nat -> nat = suc

yields:

Type checking failed: expected a data type for the constructor suc but got Pi (nat) ((\(_ : nat) -> nat))

The workaround is to lambda-abstract suc:

suc' : nat -> nat = \(n : nat) -> suc n

File loaded.

I tried to end this message in a pun about "pointless" but I can't seem to hit the spot.

[mortberg]

I implemented this for an earlier version of cubical where abstractions were not typed simply by eta-expanding the constructors sufficiently much. This was really easy to implement as I only needed to know how many arguments were missing in the application of the constructor. However with typed abstraction this becomes a little bit more complicated as I need to know what types are expected for the abstractions that I create while eta expanding (and this might be tricky to get right in the presence of dependent types...). Because of this I never bothered implementing this for cubicaltt. So for now the user has to eta expand by hand when necessary.

A possible way for solving this would be to do typed conversion. This would have the additional benefit that we can have untyped applications again and my old code for eta-expanding constructors should work.

[mortberg]

Oh, one more thing. My previous solution for this was for a version without any HITs and I'm not sure if the presence of path constructors could complicate things...