{-# LANGUAGE OverloadedStrings #-} {-# OPTIONS_GHC -Wall -fno-warn-tabs #-} module Plugin.TypeCheck.Nat.Simple.UnNomEq (unNomEq) where import Constraint (Ct, ctEvidence, ctEvPred) import Type (Type) import Predicate(Pred(..), EqRel(..), classifyPredType) import Outputable (ppr, text, (<+>)) import Control.Monad.Try (Try, throw) import Data.Log (IsSDoc, fromSDoc) unNomEq :: (Monoid w, IsSDoc e) => Ct -> Try e w (Type, Type) unNomEq :: Ct -> Try e w (Type, Type) unNomEq Ct ct = case Type -> Pred classifyPredType (Type -> Pred) -> (CtEvidence -> Type) -> CtEvidence -> Pred forall b c a. (b -> c) -> (a -> b) -> a -> c . CtEvidence -> Type ctEvPred (CtEvidence -> Pred) -> CtEvidence -> Pred forall a b. (a -> b) -> a -> b $ Ct -> CtEvidence ctEvidence Ct ct of EqPred EqRel NomEq Type l Type r -> (Type, Type) -> Try e w (Type, Type) forall (f :: * -> *) a. Applicative f => a -> f a pure (Type l, Type r) Pred _ -> e -> Try e w (Type, Type) forall w e a. Monoid w => e -> Try e w a throw (e -> Try e w (Type, Type)) -> (SDoc -> e) -> SDoc -> Try e w (Type, Type) forall b c a. (b -> c) -> (a -> b) -> a -> c . SDoc -> e forall s. IsSDoc s => SDoc -> s fromSDoc (SDoc -> Try e w (Type, Type)) -> SDoc -> Try e w (Type, Type) forall a b. (a -> b) -> a -> b $ String -> SDoc text String "unNomEq: no match to EqPred NomEq l r:" SDoc -> SDoc -> SDoc <+> Ct -> SDoc forall a. Outputable a => a -> SDoc ppr Ct ct