Re: [isabelle] Bizarre type unification error



On Tue, Apr 29, 2008 at 11:00 AM, Tobias Nipkow <nipkow at in.tum.de> wrote:
> The problem was that you did something like this:
>
> fix x :: 'a set
> assume "x = {{}}"
>
> where x should really be of type 'a set set. But when you write down a type
> variable in a fix, it really is fixed. Hence the type unification error.
> Solution for fix/assume: either no types at all (in which case type
> inference solves the problem in most cases) or full types.

Removing the type annotation fixed my problem, thanks.

Is the cause one of impredicative instantiation?  Is that what you
mean by "once you write down a type variable in a fix, it really is
fixed"?

--
 Denis



-- 
 Denis





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