search

MartyO256 / mechanizing-standard-ml

Mechanizing the metatheory of Standard ML in Beluga using Harpoon
0 stars 0 forks source link

Ill-typed term errors where the expected type matches the inferred type #3

Closed MartyO256 closed 4 years ago

MartyO256 commented 4 years ago

Harpoon throws "Ill-typed term" errors in the following four cases, but the actual error messages seem to indicate that those terms are well-typed.

The technical details of each case is inline, in "FIXME" comments in the issue3 branch.

In the kd-equiv-reg/2 theorem, kd-equiv/sigma branch,

[_|-kd-wf/sigma Dwf2a (\a. \da. Dwf2b[.., <a;Dof1[.., <_;da>]>])]

is expected to be well-typed. https://github.com/MartyO256/mechanizing-standard-ml/blob/07d71cd2cbed485449235ad22075701c475b96dc/src/safety/regularity.thm#L106-L144 In the kd-equiv-reg/2 theorem, kd-equiv/pi branch,

[_|-kd-wf/pi Dwf2a (\a. \da. Dwf2b[.., <a;Dof1[.., <_;da>]>])]

is expected to be well-typed. https://github.com/MartyO256/mechanizing-standard-ml/blob/07d71cd2cbed485449235ad22075701c475b96dc/src/safety/regularity.thm#L145-L183 In the cn-equiv-reg/cn-of2 theorem, cn-equiv/rec branch,

[_|-cn-of/rec DwfK2 (\a. \d. \b. \e. DofC2[.., <a;Dof1[.., <_;d>]>, <b;Dof2[.., <_;e>]>]) DofD2']

is expected to be well-typed. https://github.com/MartyO256/mechanizing-standard-ml/blob/07d71cd2cbed485449235ad22075701c475b96dc/src/safety/regularity.thm#L1094-L1163 In the cn-equiv-reg/cn-of2 theorem, cn-equiv/lam branch,

cn-of/equiv/conbind-reg [_|-cn-of/lam Dwf2a (\a. \da. Dof2b[.., <a;Dof1[.., <_;da>]>])] [_|-kd-equiv/pi DequivA' (\a. \da. DwfB[.., <a;Dof1[.., <_;da>]>])]

is expected to be well-typed. https://github.com/MartyO256/mechanizing-standard-ml/blob/07d71cd2cbed485449235ad22075701c475b96dc/src/safety/regularity.thm#L1253-L1315