typechecker forgetful?

[zilinc]

As in the file below, None _ fails because the compiler cannot infer what the type _ has. However it should know it's casing on an Option Ext2DirEnt type where None () is the type. In fact, if you tell the compiler that _ has some type, it always believes.

[zilinc]

This symptom was uncovered due to 680597da9ae1f

[liamoc]

This is generally a problem I noted a while ago. We don't deal with cases where the number of parameters of option types differs.

Or is their Option defined with a pointless () in there?

[liamoc]

If Option is defined with a (), this is a bug.

[zilinc]

No. type Option a = <None|Some a>

[liamoc]

OK, and, to be clear, if you just remove the _ it compiles right?

This should be an error, but the error has to be better than what it currently is..

[zilinc]

Yes. Well, None _ means None (), if it stays the same as I implemented it. If I wrote None a -> a where a is the top-level return value, and a has type U16, it also compiled.

[zilinc]

So it seems that, as long as it can know from somewhere what the type of _ is, no matter what, it's happy.

[liamoc]

OK, It should be rejecting such programs because you could pretty easily break soundness this way.

undefined : all a. () -> a
undefined () = None 
   | None x -> x

I'll look into fixing this bug soon. Currently very busy with personal matters, but I'll be back soon I hope.

[zilinc]

If None means None () then it will be rejected. Currently it's rejected due to leftover constraint because None has type None a for any a.

[liamoc]

None doesn't mean None () (except after desugaring). But None shouldn't mean None a for any a.

[zilinc]

Oddly enough to me, if I compile

undefined : all a. () -> a
undefined () = None ()
   | None x -> x

I get

Leftover constraint!
Exhaustive ?0 [None x]
   when checking that the expression at ("pass_undefined-2.cogent" (line 4, column 16))
      (None ())
      | None x -> x
   has type
      a
   in the 1st alternative ()
   in the definition at ("pass_undefined-2.cogent" (line 3, column 1))
   for the function undefined

which is rightly rejected but for wrong reason.

[zilinc]

None doesn't mean None () (except after desugaring). But None shouldn't mean None a for any a.

Can we make it so even in the surface language? (As it was introduced solely as a sugar)

[liamoc]

Yeah, so I think in the old TC we had some weird syntactic thing where it would automatically assume all variant constructor had exactly one parameter even though we accepted n-ary syntax. Now I've made it so that constructors can have zero, one, or more arguments. I'll make the desugarer make them unary again.

[zilinc]

Well we can keep them n-ary if it doesn't make everything too much more difficult. For the surface we can just check that the number of arguments be the same, then None means None and nothing else.

[liamoc]

Right, that's my plan. But in the core, we'll desugar them to units/tuples like before. I don't think it'd be wise to complicate the core language: the less changes we make to that the easier time we'll have in Isabelle.

[zilinc]

Cool, that I'll need to walk through the file systems once more, but it will make things cleaner eventually.

[liamoc]

The file systems right now are using tuples in the variants all the time. It's OK to leave them like that, but we can simplify some cases sure.

[zilinc]

Ah sure. I meant I need to remove or add ()s to make them compile.

[liamoc]

I've made it an error now to invoke constructors with different numbers of arguments.