{-# LANGUAGE OverloadedStrings #-}

module Rerefined.Predicate.Fail where

import Rerefined.Predicate.Common

-- | Always fails.
data Fail
instance Predicate Fail where type PredicateName d Fail = "⊥"
instance Refine Fail a where validate :: Proxy# Fail -> a -> Maybe RefineFailure
validate Proxy# Fail
p a
_ = Proxy# Fail -> Builder -> [RefineFailure] -> Maybe RefineFailure
forall {k} (p :: k).
(Predicate p, KnownPredicateName p) =>
Proxy# p -> Builder -> [RefineFailure] -> Maybe RefineFailure
validateFail Proxy# Fail
p Builder
"fail" []