remove Typeable constraint on Predicate

[nikita-volkov]

Why was it introduced?

[raehik]

Typeable is used for lots of predicate failure code, via calling typeRep on the predicate (passed around in a Proxy p). It's very useful for the base predicates where meaning is obvious from names and type arguments. Though you might be able to replace it with an associated type class and function to allow "opting out" of the Typeable constraint.

Alternatively, do you mean to clear up the placement of Typeable constraints? A change I made in #83 meant adding more constraints to instances. #98 resolves (and fixes an oversight).

[raehik]

See how my refined rewrite rerefined resolves this:

class Predicate p where
    -- | The predicate name, as a 'Show'-like (for nice bracketing).
    predicateName :: Proxy# p -> Int -> ShowS

-- | Fill out predicate metadata using its 'Typeable' instance.
--
-- Do not use this for combinator predicates. Doing so will incur
-- insidious 'Typeable' contexts for the wrapped predicate(s).
instance Typeable a => Predicate (Typeably a) where
    predicateName _ d = showsPrec d (typeRep (Proxy @a))

class Predicate p => Refine p a where
    validate :: Proxy# p -> a -> Maybe (RefineFailure String)

-- ...

-- simplified
instance (Predicate l, Predicate r)
  => Predicate (And l r) where
    predicateName _ d = showParen (d > 10) $
          showString "And "
        . predicateName (proxy# @l) 11 . showChar ' '
        . predicateName (proxy# @r) 11

This way, we can continue to use Typeable for convenience for non-combinator predicates, while not incurring insidious Typeable constraints, and retain more control over pretty predicate display in general. Also, TypeReps print inferred/hidden kinds (e.g. And (l :: k1) (r :: k2)), which we can omit.

[raehik]

Ping. I've rewritten my refined-heavy library binrep to use rerefined which effectively implements the above (except predicate names are calculated type-level) with no issues.