T13910 is broken in optasm
Compile failed (exit code 1) errors were:
*** Core Lint errors : in result of Simplifier ***
<no location info>: warning:
In the type ‘forall t (from :: t) (to :: t) (p :: t -> *).
App t (':->) * (p |> Sym (D:R:Funk1:->k2[0] <t>_N <*>_N)) from
-> (from :~: to)
-> WhyReplacePoly
(':->)
from
(p |> Sym (D:R:Funk1:->k2[0] <t>_N <*>_N))
to
('Refl |> ((:~:) <t>_N <from>_N (Sym co_a5yh))_N)’
co_a5yh :: to_a5vA ~# from_a5vz
[LclId[CoVarId]] is out of scope
*** Offending Program ***
...
Edited by Ben Gamari