What does the dafny error "type error mismatch (function expects H, got H)" mean?

user_2507257 0
Viewed 138

I am using Dafny 17.2 in VS code

type H
 predicate Pfo(k:H)
lemma  fo<H> (h:H) 
  ensures forall k:H :: Pfo(k)

I cannot understand the error message

type mismatch for argument (function expects H, got H)

Any help appreciated david

Added example:

type H
 predicate Pfo(y:H,x:H)
lemma  fo<H> (h:H) 
  ensures forall k :: Pfo(k,h)

Very similar error message

type mismatch for argument 1 (function expects H, got H)

but this time I have attempted to follow the solution given for the initial example and delete occurrences of ":H" but could not find any solution.

dafny types
2 Answers

The type parameter H declared in the angle brackets shadows the global declaration of H. So when you say forall k:H you are saying "for all k that have type given the type parameter, Pfo(k) is true". But that doesn't make sense, because Pfo expects an argument whose type is the globally declared H.

Easy fix is to just delete the :H type annotation on k, since Dafny will then correctly infer that k should have the global H type.

The error message is admittedly confusing. You could file a github issue to see if anyone is interested in improving it. I guess one idea would be to make Dafny print the location in the source file where each H is declared, so that it's clear they are different.

In your second example, the only solution I know of would be to manually rename the type parameter H so that its name does not clash with the global H. Then you can refer to the correct one by name.

user_4382670

My error was to add type parameters to the lemmas lemma fo<H> should have been lemma fo.

type H
 predicate Pfo(y:H)
lemma  fo (h:H) 
  ensures forall k:H :: Pfo(k)  
predicate Qfo(x:H,y:H)
lemma  foo (h:H) 
  ensures forall k :: Qfo(k,h)

In my defence the error message was not easy to understand but having a better understanding I wont make the same mistake.

user_25072570
Related