remove Typeable constraint on Predicate

[chessai]

No description provided.

[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.

[raehik]

Ping @chessai @nikita-volkov . I'd still be keen on solving this one way or another.

• rerefined solves it "for good" but has a completely different design (predicateName is now type PredicateName)
• move Typeable constraint on predicate kind to class #98 is a good fix
• alternatively, you could remove support for polykinded predicates. (I've stopped using them personally, plus they don't work with my predicate simplifier in rerefined.)

[chessai]

This is solved now by @raehik's work :)