Hi all,
every once in a while, I manage to create a goal state which contains
type variables with the empty sort (for example in f x = 0, x is of
type 'b :: {}, if there are no additional constraints on f. Some tools
don't like this (e.g. metis omits a warning, SMT fails altogether) and
it
On Wed, 29 Jun 2011, Lars Noschinski wrote:
every once in a while, I manage to create a goal state which contains
type variables with the empty sort (for example in f x = 0, x is of
type 'b :: {}, if there are no additional constraints on f. Some tools
don't like this (e.g. metis omits a
Yes, it is a problem of unintended generality. The question remains: are
there known situations where it is intended, or could one restrict the
generated type variables in the same way as the explicitly stated ones.
Tobias
Am 29/06/2011 17:23, schrieb Makarius:
On Wed, 29 Jun 2011, Lars