compiler: core/infer: insert Promote terms underneath Con

[amosr]

@zilinc @liamoc

My understanding of the Core type system is that all subtyping requires an explicit Promote term. I believe there is no implicit subsumption.

In the formalisation, the rule for variants is something like the following, and it requires the expression type to be strictly equal to the type for the tag in the variant type:

     ... |-  e : ts[tag]
---------------------------------
 ... |-   Con tag e ts : TSum ts

However, the compiler is currently generating core code that allows subtyping underneath a Con, which would correspond to something like the following rule:

 ... |-  e : t'           t' <= ts[tag]
----------------------------------------
 ... |-   Con tag e ts : TSum ts

I think this is just a bug in the implementation of infer, as it was not adding promote nodes everywhere that it should. I have added the following test case, but unfortunately it compiles either way. I'm not sure whether there's a way to require that a test case results in particular core code.

Test case: these two functions should result in the same output core.

-- The given value is a subtype of the variant's payload. The payload should be promoted.
implicit_promote : () -> ()
implicit_promote _
  = let x = #{f1=1, f2=2}
    and y : <A (#{f1 : U8, f2 : U8} take (f1,f2))> = A x
    in ()

-- The given value is a subtype of the variant's payload. We explicitly promote the payload.
explicit_promote : () -> ()
explicit_promote _
  = let x = #{f1=1, f2=2}
    and y : <A (#{f1 : U8, f2 : U8} take (f1,f2))> = A (x : (#{f1 : U8, f2 : U8} take (f1,f2)))
    in ()

[vjackson725]

N.B. the proofs did some pseudo-subtyping before, which was a hold-over from the pre-subtyping Promote terms. Removing this makes the rule much cleaner, and as Amos has said, it would be better for the compiler to produce an explicit Promote now.

[amosr]

Cool, thanks. Will merge. I don't know how important the test is. It'd be nice if it's easy with the current setup. If there's a set of tests for the type proof generation, it's probably enough for this to go in there? (There might already be such a test, I don't know)