Re: [isabelle] Malformed dependency error with overloading



On 05/27/2016 01:18 PM, OndÅej KunÄar wrote:
Therefore we impose an additional restriction that makes the problem
quadratic. I call the restriction composability:
for all  d_\tau == ... and
         c == ... d_\sigma ...
\sigma must be an instance of \tau or \tau must be an instance of \sigma.
(More can be found in my PhD thesis (chapter 3.5)).

Of course, I missed one case.
\sigma must be an instance of \tau or \tau must be an instance of \sigma *or they are not unifiable*.

That said, composability wants to rule out the case that the two types have a non-trivial common instance.




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.