spec: subtype checking only for reference types

Open chenyan-dfinity opened this issue 4 years ago • 2 comments

Fix #295

Jan 12 '22 01:01 chenyan-dfinity

#316 has early explorations of updating the Coq proof for this, but stuck at various technicalities right now. For example

Lemma coerce_roundtrip:
  forall t1 v1,
  v1 :: t1 ->
  coerce t1 t1 v1 = Some v1.

doesn't work with our “untyped values” in the formalization because :: allows any reference value at any type.

Feb 10 '22 11:02 nomeata

Oh, this hasn't landed yet? Completely forgot… I guess we are waiting for all implementations to catch up?

Oct 07 '22 14:10 nomeata

Oh, this hasn't landed yet? Completely forgot… I guess we are waiting for all implementations to catch up?

@chenyan-dfinity is working on it. Motoko is hopefully ready to go (though I'm worried even I don't understand that implementation any more).

Oct 26 '22 19:10 crusso

🥳

I have released haskell-candid 0.4 with the corresponding changes (https://github.com/nomeata/haskell-candid/pull/20).

~Maybe someone can help me with https://github.com/dfinity/ic-hs/pull/118?~

Dec 05 '22 08:12 nomeata