module Language.Haskell.Tools.Refactor.Builtin.ExtensionOrganizer.Checkers.UndecidableInstancesChecker where
import Name
import CoAxiom
import FamInstEnv
import InstEnv
import TcType
import GHC hiding (Module, ClassDecl, ClosedTypeFamily)
import Data.Maybe (isJust)
import Control.Reference ((^.))
import Control.Monad.Trans.Maybe (MaybeT(..))
import Language.Haskell.Tools.AST
import Language.Haskell.Tools.Refactor
import Language.Haskell.Tools.Refactor.Builtin.ExtensionOrganizer.ExtMonad
import Language.Haskell.Tools.Refactor.Builtin.ExtensionOrganizer.Utils.GHCHelpers
gblChkUndecidableInstances :: CheckNode Module
gblChkUndecidableInstances = conditional gblChkUndecidableInstances' UndecidableInstances
gblChkUndecidableInstances' :: CheckNode Module
gblChkUndecidableInstances' m = do
(clsInsts, famInsts) <- getInstances [semanticsModule m]
mapM_ chkClsInst clsInsts
mapM_ chkFamInst famInsts
return m
chkClsInst :: ClsInst -> ExtMonad ()
chkClsInst inst = when (clsInstNeedsUD inst)
(addEvidenceLoc UndecidableInstances (getSrcSpan inst))
clsInstNeedsUD :: ClsInst -> Bool
clsInstNeedsUD inst = checkInstTermination args theta
where (_, theta, _, args) = instanceSig inst
chkFamInst :: FamInst -> ExtMonad ()
chkFamInst inst = when (famInstNeedsUD inst)
(addEvidenceLoc UndecidableInstances (getSrcSpan inst))
famInstNeedsUD :: FamInst -> Bool
famInstNeedsUD inst
| isTyFamInst inst
, lhs <- fi_tys inst
, rhs <- tcTyFamInsts . fi_rhs $ inst
= checkFamEq lhs rhs
| otherwise = False
chkUndecidableInstancesDecl :: CheckNode Decl
chkUndecidableInstancesDecl = conditional chkUndecidableInstancesDecl' UndecidableInstances
chkUndecidableInstancesDecl' :: CheckNode Decl
chkUndecidableInstancesDecl' d = do
mDecl <- runMaybeT (chkUndecidableInstancesDeclMaybe d)
maybe (addEvidence UndecidableInstances d) return mDecl
chkUndecidableInstancesDeclMaybe :: Decl -> MaybeT ExtMonad Decl
chkUndecidableInstancesDeclMaybe d@(ClassDecl mCtx _ _ _)
| isJust (mCtx ^. annMaybe) = do
ctx <- liftMaybe $ mCtx ^. annMaybe
let assert = ctx ^. contextAssertion
names = assertionQNames assert
types <- mapM lookupTypeFromId names
if any hasTyFunHead types then addEvidence UndecidableInstances d
else return d
| otherwise = return d
chkUndecidableInstancesDeclMaybe d@(ClosedTypeFamily dh _ _) = do
tyFam <- lookupClosedTyFam dh
let brs = fromBranches . coAxiomBranches $ tyFam
famEqs = map ((,) <$> coAxBranchLHS <*> tcTyFamInsts . coAxBranchRHS) brs
mapM_ (lift . uncurry chkFamEqM) famEqs >> return d
where
chkFamEqM :: [GHC.Type] -> [(GHC.TyCon, [GHC.Type])] -> ExtMonad ()
chkFamEqM lhs rhs = when (checkFamEq lhs rhs)
(addEvidence_ UndecidableInstances d)
chkUndecidableInstancesDeclMaybe d = return d