Forcing predicate value throws `undefined`

[ChickenProp]

If I have the predicate

data FiniteP = FiniteP
instance RealFloat n => Refined.Predicate FiniteP n where
  validate FiniteP n =
    when (isNaN n || isInfinite n) $ Refined.throwRefineOtherException
      (typeOf FiniteP)
      "NaN or +/- Infinity"

then $$(refineTH 0.0) :: Refined FiniteP Double gives a compile-time undefined pointing to https://github.com/nikita-volkov/refined/blob/v0.4.4/src/Refined/Internal.hs#L299 . If I replace the function pattern match with validate _ n =, the error goes away. I haven't specifically tried refine 0.0, but presumably it does the same.

I guess related to #12, in that in earlier versions the predicate could only ever be undefined, and now they might not be undefined but refined still expects them to be.

[chessai]

There is no easy way to fix this without some egregious hacks involving unsafePerformIO and/or changing the API quite a bit. I think the best that can be done (for now) is to document it. I will keep this issue open though, to think about alternative solutions.

[chessai]

addressed in 1621a83

[chessai]

Actually, I think the easiest thing to do is to just change the signature of validate to

validate :: Proxy p -> x -> Maybe RefineException

Since no valid instance of Predicate could be casing on its first argument anyway, this shouldn't cause any breakage in practise.

Don't know why I didn't think of this the other day.

[chessai]

Ah, this definitely makes the UX around natVal worse. Consider:

data Equal (n :: Nat) = Equal

instance (Eq x, Num x, KnownNat n) => Predicate (Equal n) x where
  validate p@Proxy x = do
  let x' = fromIntegral (natVal p)
  ... some other stuff ...

This will give an error since natVal expects an argument of kind Nat -> Type, but here we have an outer layer Proxy :: Type -> Type (since we have Proxy (Equal n))

[chessai]

@symbiont-sam-halliday how much of your code would this (the Proxy change) break?

[symbiont-sam-halliday]

not much, it's well within my tolerances for a breaking change; thanks for asking!