search

nick8325 / quickspec

Equational laws for free
BSD 3-Clause "New" or "Revised" License
250 stars 24 forks source link

Bug: QuickCheck output doesn't give types to polymorphic terms #64

Open isovector opened 4 years ago

isovector commented 4 years ago

Consider the following signature:

quickSpec $ signature
  [ con "zero" $ liftC @(Num A) $ zero @A
  , con "0" $ liftC @(Num A) $ (0 :: A)
  , instanceOf @(Num Int)
  , withPrintStyle ForQuickCheck
  ]

which produces the following output:

quickspec_laws :: [(String, Property)]
quickspec_laws =
  [ ( "zero = 0" , property $ zero =~= 0)
  ]

But uh oh! This code is ambiguous in a!

I think the solution is to give an explicit type to any term that isn't applied to a quantified variable (variables always get types when bound in the lambda.)

isovector commented 4 years ago

This is actually quite a blocker on my book; I'll see about implementing a solution today, but would love any insight you might have here, Nick!

nick8325 commented 4 years ago

Reopening, because this is also an issue when printing equations in "normal" mode.

I think if we want to solve this in all cases, we have to take the generated equation (without type annotations) and do type inference on it. Then add extra type annotations so that the inferred type matches up with the actual type of the discovered law.