{-# 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