Re: [isabelle] primrec - error: Variable 'a::{} not of sort type



On 19.08.2014 13:29, Peter Lammich wrote:
> Hi all.
>
> If I issue the following definition:
>
>   primrec f where "f g v (a,b) = (g v a, b)"
>
> I get:
>
> Type unification failed: Variable 'a::{} not of sort type
>
> Type error in application: incompatible operand type
>
> Operator:  old.rec_prod :: ('b ⇒ 'd ⇒ ??'a) ⇒ 'b × 'd ⇒ ??'a
> Operand:   λa b g v. (g v a, b) ::
>   'b ⇒ 'd ⇒ ('a ⇒ 'b ⇒ 'c) ⇒ 'a ⇒ 'c × 'd
>
>
> Although I would have expected the definition to go through. What is
> going wrong here?
This has nothing to do with primrec. If you inspect

    term "f g v (a,b) = (g v a, b)"

or the even simpler

    term "h x"

you will see that the first argument to g has the empty sort, as has x.
This is a shortcoming of our type-inference:
If the type of a variable is fully unconstrained (like the first
argument of g), the type inference fails to insert the default sort
("type", in the case of HOL) for the corresponding type variable.

The workaround is to add sufficient type annotations.

  -- Lars





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