{- |
    Module      :  $Header$
    Description :  Checks instances
    Copyright   :  (c)        2016 Finn Teegen
    License     :  BSD-3-clause

    Maintainer  :  bjp@informatik.uni-kiel.de
    Stability   :  experimental
    Portability :  portable

   Before type checking, the compiler checks for every instance declaration
   that all necessary super class instances exist. Furthermore, the compiler
   infers the contexts of the implicit instance declarations introduced by
   deriving clauses in data and newtype declarations. The instances declared
   explicitly and automatically derived by the compiler are added to the
   instance environment . It is also checked that there are no duplicate
   instances and that all types specified in a default declaration are
   instances of the Num class.
-}
module Checks.InstanceCheck (instanceCheck) where

import           Control.Monad.Extra        (concatMapM, whileM, unless)
import qualified Control.Monad.State as S   (State, execState, gets, modify)
import           Data.List                  (nub, partition, sortBy)
import qualified Data.Map            as Map
import qualified Data.Set.Extra      as Set

import Curry.Base.Ident
import Curry.Base.Pretty
import Curry.Base.SpanInfo
import Curry.Syntax hiding (impls)
import Curry.Syntax.Pretty

import Base.CurryTypes
import Base.Messages (Message, spanInfoMessage, message, internalError)
import Base.SCC (scc)
import Base.TypeExpansion
import Base.Types
import Base.TypeSubst
import Base.Utils (fst3, snd3, findMultiples)

import Env.Class
import Env.Instance
import Env.TypeConstructor

instanceCheck :: ModuleIdent -> TCEnv -> ClassEnv -> InstEnv -> [Decl a]
              -> (InstEnv, [Message])
instanceCheck :: ModuleIdent
-> TCEnv -> ClassEnv -> InstEnv -> [Decl a] -> (InstEnv, [Message])
instanceCheck m :: ModuleIdent
m tcEnv :: TCEnv
tcEnv clsEnv :: ClassEnv
clsEnv inEnv :: InstEnv
inEnv ds :: [Decl a]
ds =
  case [InstSource] -> [[InstSource]]
forall a. Eq a => [a] -> [[a]]
findMultiples ([InstSource]
local [InstSource] -> [InstSource] -> [InstSource]
forall a. [a] -> [a] -> [a]
++ [InstSource]
imported) of
    [] -> INCM () -> INCState -> (InstEnv, [Message])
forall a. INCM a -> INCState -> (InstEnv, [Message])
execINCM (TCEnv -> ClassEnv -> [Decl a] -> INCM ()
forall a. TCEnv -> ClassEnv -> [Decl a] -> INCM ()
checkDecls TCEnv
tcEnv ClassEnv
clsEnv [Decl a]
ds) INCState
state
    iss :: [[InstSource]]
iss -> (InstEnv
inEnv, ([InstSource] -> Message) -> [[InstSource]] -> [Message]
forall a b. (a -> b) -> [a] -> [b]
map (TCEnv -> [InstSource] -> Message
errMultipleInstances TCEnv
tcEnv) [[InstSource]]
iss)
  where
    local :: [InstSource]
local = (InstIdent -> InstSource) -> [InstIdent] -> [InstSource]
forall a b. (a -> b) -> [a] -> [b]
map ((InstIdent -> ModuleIdent -> InstSource)
-> ModuleIdent -> InstIdent -> InstSource
forall a b c. (a -> b -> c) -> b -> a -> c
flip InstIdent -> ModuleIdent -> InstSource
InstSource ModuleIdent
m) ([InstIdent] -> [InstSource]) -> [InstIdent] -> [InstSource]
forall a b. (a -> b) -> a -> b
$ (Decl a -> [InstIdent]) -> [Decl a] -> [InstIdent]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (ModuleIdent -> TCEnv -> Decl a -> [InstIdent]
forall a. ModuleIdent -> TCEnv -> Decl a -> [InstIdent]
genInstIdents ModuleIdent
m TCEnv
tcEnv) [Decl a]
ds
    imported :: [InstSource]
imported = ((InstIdent, (ModuleIdent, PredSet, [(Ident, Int)])) -> InstSource)
-> [(InstIdent, (ModuleIdent, PredSet, [(Ident, Int)]))]
-> [InstSource]
forall a b. (a -> b) -> [a] -> [b]
map ((InstIdent -> ModuleIdent -> InstSource)
-> (InstIdent, ModuleIdent) -> InstSource
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry InstIdent -> ModuleIdent -> InstSource
InstSource ((InstIdent, ModuleIdent) -> InstSource)
-> ((InstIdent, (ModuleIdent, PredSet, [(Ident, Int)]))
    -> (InstIdent, ModuleIdent))
-> (InstIdent, (ModuleIdent, PredSet, [(Ident, Int)]))
-> InstSource
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((ModuleIdent, PredSet, [(Ident, Int)]) -> ModuleIdent)
-> (InstIdent, (ModuleIdent, PredSet, [(Ident, Int)]))
-> (InstIdent, ModuleIdent)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ModuleIdent, PredSet, [(Ident, Int)]) -> ModuleIdent
forall a b c. (a, b, c) -> a
fst3) ([(InstIdent, (ModuleIdent, PredSet, [(Ident, Int)]))]
 -> [InstSource])
-> [(InstIdent, (ModuleIdent, PredSet, [(Ident, Int)]))]
-> [InstSource]
forall a b. (a -> b) -> a -> b
$ InstEnv -> [(InstIdent, (ModuleIdent, PredSet, [(Ident, Int)]))]
forall k a. Map k a -> [(k, a)]
Map.toList InstEnv
inEnv
    state :: INCState
state = ModuleIdent -> InstEnv -> [Message] -> INCState
INCState ModuleIdent
m InstEnv
inEnv []

-- In order to provide better error messages, we use the following data type
-- to keep track of an instance's source, i.e., the module it was defined in.

data InstSource = InstSource InstIdent ModuleIdent

instance Eq InstSource where
  InstSource i1 :: InstIdent
i1 _ == :: InstSource -> InstSource -> Bool
== InstSource i2 :: InstIdent
i2 _ = InstIdent
i1 InstIdent -> InstIdent -> Bool
forall a. Eq a => a -> a -> Bool
== InstIdent
i2

-- |Instance Check Monad
type INCM = S.State INCState

-- |Internal state of the Instance Check
data INCState = INCState
  { INCState -> ModuleIdent
moduleIdent :: ModuleIdent
  , INCState -> InstEnv
instEnv     :: InstEnv
  , INCState -> [Message]
errors      :: [Message]
  }

execINCM :: INCM a -> INCState -> (InstEnv, [Message])
execINCM :: INCM a -> INCState -> (InstEnv, [Message])
execINCM incm :: INCM a
incm s :: INCState
s =
  let s' :: INCState
s' = INCM a -> INCState -> INCState
forall s a. State s a -> s -> s
S.execState INCM a
incm INCState
s in (INCState -> InstEnv
instEnv INCState
s', [Message] -> [Message]
forall a. [a] -> [a]
reverse ([Message] -> [Message]) -> [Message] -> [Message]
forall a b. (a -> b) -> a -> b
$ [Message] -> [Message]
forall a. Eq a => [a] -> [a]
nub ([Message] -> [Message]) -> [Message] -> [Message]
forall a b. (a -> b) -> a -> b
$ INCState -> [Message]
errors INCState
s')

getModuleIdent :: INCM ModuleIdent
getModuleIdent :: INCM ModuleIdent
getModuleIdent = (INCState -> ModuleIdent) -> INCM ModuleIdent
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
S.gets INCState -> ModuleIdent
moduleIdent

getInstEnv :: INCM InstEnv
getInstEnv :: INCM InstEnv
getInstEnv = (INCState -> InstEnv) -> INCM InstEnv
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
S.gets INCState -> InstEnv
instEnv

modifyInstEnv :: (InstEnv -> InstEnv) -> INCM ()
modifyInstEnv :: (InstEnv -> InstEnv) -> INCM ()
modifyInstEnv f :: InstEnv -> InstEnv
f = (INCState -> INCState) -> INCM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
S.modify ((INCState -> INCState) -> INCM ())
-> (INCState -> INCState) -> INCM ()
forall a b. (a -> b) -> a -> b
$ \s :: INCState
s -> INCState
s { instEnv :: InstEnv
instEnv = InstEnv -> InstEnv
f (InstEnv -> InstEnv) -> InstEnv -> InstEnv
forall a b. (a -> b) -> a -> b
$ INCState -> InstEnv
instEnv INCState
s }

report :: Message -> INCM ()
report :: Message -> INCM ()
report err :: Message
err = (INCState -> INCState) -> INCM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
S.modify (\s :: INCState
s -> INCState
s { errors :: [Message]
errors = Message
err Message -> [Message] -> [Message]
forall a. a -> [a] -> [a]
: INCState -> [Message]
errors INCState
s })

ok :: INCM ()
ok :: INCM ()
ok = () -> INCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

checkDecls :: TCEnv -> ClassEnv -> [Decl a] -> INCM ()
checkDecls :: TCEnv -> ClassEnv -> [Decl a] -> INCM ()
checkDecls tcEnv :: TCEnv
tcEnv clsEnv :: ClassEnv
clsEnv ds :: [Decl a]
ds = do
  (Decl a -> INCM ()) -> [Decl a] -> INCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (TCEnv -> ClassEnv -> Decl a -> INCM ()
forall a. TCEnv -> ClassEnv -> Decl a -> INCM ()
bindInstance TCEnv
tcEnv ClassEnv
clsEnv) [Decl a]
ids
  (Decl a -> StateT INCState Identity DeriveInfo)
-> [Decl a] -> StateT INCState Identity [DeriveInfo]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (TCEnv -> ClassEnv -> Decl a -> StateT INCState Identity DeriveInfo
forall a.
TCEnv -> ClassEnv -> Decl a -> StateT INCState Identity DeriveInfo
declDeriveDataInfo TCEnv
tcEnv ClassEnv
clsEnv) ((Decl a -> Bool) -> [Decl a] -> [Decl a]
forall a. (a -> Bool) -> [a] -> [a]
filter Decl a -> Bool
forall a. Decl a -> Bool
isDataDecl [Decl a]
tds) StateT INCState Identity [DeriveInfo]
-> ([DeriveInfo] -> INCM ()) -> INCM ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
    ([DeriveInfo] -> INCM ()) -> [[DeriveInfo]] -> INCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (ClassEnv -> [DeriveInfo] -> INCM ()
bindDerivedInstances ClassEnv
clsEnv) ([[DeriveInfo]] -> INCM ())
-> ([DeriveInfo] -> [[DeriveInfo]]) -> [DeriveInfo] -> INCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [DeriveInfo] -> [[DeriveInfo]]
groupDeriveInfos
  (Decl a -> StateT INCState Identity DeriveInfo)
-> [Decl a] -> StateT INCState Identity [DeriveInfo]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (TCEnv -> ClassEnv -> Decl a -> StateT INCState Identity DeriveInfo
forall a.
TCEnv -> ClassEnv -> Decl a -> StateT INCState Identity DeriveInfo
declDeriveInfo TCEnv
tcEnv ClassEnv
clsEnv) ((Decl a -> Bool) -> [Decl a] -> [Decl a]
forall a. (a -> Bool) -> [a] -> [a]
filter Decl a -> Bool
forall a. Decl a -> Bool
hasDerivedInstances [Decl a]
tds) StateT INCState Identity [DeriveInfo]
-> ([DeriveInfo] -> INCM ()) -> INCM ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
    ([DeriveInfo] -> INCM ()) -> [[DeriveInfo]] -> INCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (ClassEnv -> [DeriveInfo] -> INCM ()
bindDerivedInstances ClassEnv
clsEnv) ([[DeriveInfo]] -> INCM ())
-> ([DeriveInfo] -> [[DeriveInfo]]) -> [DeriveInfo] -> INCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [DeriveInfo] -> [[DeriveInfo]]
groupDeriveInfos
  (Decl a -> INCM ()) -> [Decl a] -> INCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (TCEnv -> ClassEnv -> Decl a -> INCM ()
forall a. TCEnv -> ClassEnv -> Decl a -> INCM ()
checkInstance TCEnv
tcEnv ClassEnv
clsEnv) [Decl a]
ids
  (Decl a -> INCM ()) -> [Decl a] -> INCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (TCEnv -> ClassEnv -> Decl a -> INCM ()
forall a. TCEnv -> ClassEnv -> Decl a -> INCM ()
checkDefault TCEnv
tcEnv ClassEnv
clsEnv) [Decl a]
dds
  where (tds :: [Decl a]
tds, ods :: [Decl a]
ods) = (Decl a -> Bool) -> [Decl a] -> ([Decl a], [Decl a])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition Decl a -> Bool
forall a. Decl a -> Bool
isTypeDecl [Decl a]
ds
        ids :: [Decl a]
ids = (Decl a -> Bool) -> [Decl a] -> [Decl a]
forall a. (a -> Bool) -> [a] -> [a]
filter Decl a -> Bool
forall a. Decl a -> Bool
isInstanceDecl [Decl a]
ods
        dds :: [Decl a]
dds = (Decl a -> Bool) -> [Decl a] -> [Decl a]
forall a. (a -> Bool) -> [a] -> [a]
filter Decl a -> Bool
forall a. Decl a -> Bool
isDefaultDecl [Decl a]
ods
        isDataDecl :: Decl a -> Bool
isDataDecl (DataDecl    _ _ _ _ _) = Bool
True
        isDataDecl (NewtypeDecl _ _ _ _ _) = Bool
True
        isDataDecl _                       = Bool
False

-- First, the compiler adds all explicit instance declarations to the
-- instance environment.

bindInstance :: TCEnv -> ClassEnv -> Decl a -> INCM ()
bindInstance :: TCEnv -> ClassEnv -> Decl a -> INCM ()
bindInstance tcEnv :: TCEnv
tcEnv clsEnv :: ClassEnv
clsEnv (InstanceDecl _ _ cx :: Context
cx qcls :: QualIdent
qcls inst :: InstanceType
inst ds :: [Decl a]
ds) = do
  ModuleIdent
m <- INCM ModuleIdent
getModuleIdent
  let PredType ps :: PredSet
ps _ = ModuleIdent -> TCEnv -> ClassEnv -> QualTypeExpr -> PredType
expandPolyType ModuleIdent
m TCEnv
tcEnv ClassEnv
clsEnv (QualTypeExpr -> PredType) -> QualTypeExpr -> PredType
forall a b. (a -> b) -> a -> b
$
                        SpanInfo -> Context -> InstanceType -> QualTypeExpr
QualTypeExpr SpanInfo
NoSpanInfo Context
cx InstanceType
inst
  (InstEnv -> InstEnv) -> INCM ()
modifyInstEnv ((InstEnv -> InstEnv) -> INCM ())
-> (InstEnv -> InstEnv) -> INCM ()
forall a b. (a -> b) -> a -> b
$
    InstIdent
-> (ModuleIdent, PredSet, [(Ident, Int)]) -> InstEnv -> InstEnv
bindInstInfo (ModuleIdent -> TCEnv -> QualIdent -> InstanceType -> InstIdent
genInstIdent ModuleIdent
m TCEnv
tcEnv QualIdent
qcls InstanceType
inst) (ModuleIdent
m, PredSet
ps, [(Ident, Int)] -> [Decl a] -> [(Ident, Int)]
forall a. [(Ident, Int)] -> [Decl a] -> [(Ident, Int)]
impls [] [Decl a]
ds)
  where impls :: [(Ident, Int)] -> [Decl a] -> [(Ident, Int)]
impls is :: [(Ident, Int)]
is [] = [(Ident, Int)]
is
        impls is :: [(Ident, Int)]
is (FunctionDecl _ _ f :: Ident
f eqs :: [Equation a]
eqs:ds' :: [Decl a]
ds')
          | Ident
f' Ident -> [Ident] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ((Ident, Int) -> Ident) -> [(Ident, Int)] -> [Ident]
forall a b. (a -> b) -> [a] -> [b]
map (Ident, Int) -> Ident
forall a b. (a, b) -> a
fst [(Ident, Int)]
is = [(Ident, Int)] -> [Decl a] -> [(Ident, Int)]
impls [(Ident, Int)]
is [Decl a]
ds'
          | Bool
otherwise            = [(Ident, Int)] -> [Decl a] -> [(Ident, Int)]
impls ((Ident
f', Equation a -> Int
forall a. Equation a -> Int
eqnArity (Equation a -> Int) -> Equation a -> Int
forall a b. (a -> b) -> a -> b
$ [Equation a] -> Equation a
forall a. [a] -> a
head [Equation a]
eqs) (Ident, Int) -> [(Ident, Int)] -> [(Ident, Int)]
forall a. a -> [a] -> [a]
: [(Ident, Int)]
is) [Decl a]
ds'
          where f' :: Ident
f' = Ident -> Ident
unRenameIdent Ident
f
        impls _ _ = String -> [(Ident, Int)]
forall a. String -> a
internalError "InstanceCheck.bindInstance.impls"
bindInstance _     _      _                                = INCM ()
ok

-- Next, the compiler sorts the data and newtype declarations with non-empty
-- deriving clauses into minimal binding groups and infers contexts for their
-- instance declarations. In the case of (mutually) recursive data types,
-- inference of the appropriate contexts may require a fixpoint calculation.

hasDerivedInstances :: Decl a -> Bool
hasDerivedInstances :: Decl a -> Bool
hasDerivedInstances (DataDecl    _ _ _ _ clss :: [QualIdent]
clss) = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [QualIdent] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [QualIdent]
clss
hasDerivedInstances (NewtypeDecl _ _ _ _ clss :: [QualIdent]
clss) = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [QualIdent] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [QualIdent]
clss
hasDerivedInstances _                          = Bool
False

-- For the purposes of derived instances, a newtype declaration is treated
-- as a data declaration with a single constructor. The compiler also sorts
-- derived classes with respect to the super class hierarchy so that subclass
-- instances are added to the instance environment after their super classes.

data DeriveInfo = DeriveInfo SpanInfo QualIdent PredType [Type] [QualIdent]

declDeriveInfo :: TCEnv -> ClassEnv -> Decl a -> INCM DeriveInfo
declDeriveInfo :: TCEnv -> ClassEnv -> Decl a -> StateT INCState Identity DeriveInfo
declDeriveInfo tcEnv :: TCEnv
tcEnv clsEnv :: ClassEnv
clsEnv (DataDecl p :: SpanInfo
p tc :: Ident
tc tvs :: [Ident]
tvs cs :: [ConstrDecl]
cs clss :: [QualIdent]
clss) =
  TCEnv
-> ClassEnv
-> SpanInfo
-> Ident
-> [Ident]
-> [InstanceType]
-> [QualIdent]
-> StateT INCState Identity DeriveInfo
mkDeriveInfo TCEnv
tcEnv ClassEnv
clsEnv SpanInfo
p Ident
tc [Ident]
tvs ([[InstanceType]] -> [InstanceType]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[InstanceType]]
tyss) [QualIdent]
clss
  where tyss :: [[InstanceType]]
tyss = (ConstrDecl -> [InstanceType]) -> [ConstrDecl] -> [[InstanceType]]
forall a b. (a -> b) -> [a] -> [b]
map ConstrDecl -> [InstanceType]
constrDeclTypes [ConstrDecl]
cs
        constrDeclTypes :: ConstrDecl -> [InstanceType]
constrDeclTypes (ConstrDecl     _ _ tys :: [InstanceType]
tys) = [InstanceType]
tys
        constrDeclTypes (ConOpDecl  _ ty1 :: InstanceType
ty1 _ ty2 :: InstanceType
ty2) = [InstanceType
ty1, InstanceType
ty2]
        constrDeclTypes (RecordDecl      _ _ fs :: [FieldDecl]
fs) = [InstanceType]
tys
          where tys :: [InstanceType]
tys = [InstanceType
ty | FieldDecl _ ls :: [Ident]
ls ty :: InstanceType
ty <- [FieldDecl]
fs, Ident
_ <- [Ident]
ls]
declDeriveInfo tcEnv :: TCEnv
tcEnv clsEnv :: ClassEnv
clsEnv (NewtypeDecl p :: SpanInfo
p tc :: Ident
tc tvs :: [Ident]
tvs nc :: NewConstrDecl
nc clss :: [QualIdent]
clss) =
  TCEnv
-> ClassEnv
-> SpanInfo
-> Ident
-> [Ident]
-> [InstanceType]
-> [QualIdent]
-> StateT INCState Identity DeriveInfo
mkDeriveInfo TCEnv
tcEnv ClassEnv
clsEnv SpanInfo
p Ident
tc [Ident]
tvs [NewConstrDecl -> InstanceType
nconstrType NewConstrDecl
nc] [QualIdent]
clss
declDeriveInfo _ _ _ =
  String -> StateT INCState Identity DeriveInfo
forall a. String -> a
internalError "InstanceCheck.declDeriveInfo: no data or newtype declaration"

declDeriveDataInfo :: TCEnv -> ClassEnv -> Decl a -> INCM DeriveInfo
declDeriveDataInfo :: TCEnv -> ClassEnv -> Decl a -> StateT INCState Identity DeriveInfo
declDeriveDataInfo tcEnv :: TCEnv
tcEnv clsEnv :: ClassEnv
clsEnv (DataDecl p :: SpanInfo
p tc :: Ident
tc tvs :: [Ident]
tvs cs :: [ConstrDecl]
cs _) =
  TCEnv
-> ClassEnv
-> SpanInfo
-> Ident
-> [Ident]
-> [InstanceType]
-> StateT INCState Identity DeriveInfo
mkDeriveDataInfo TCEnv
tcEnv ClassEnv
clsEnv SpanInfo
p Ident
tc [Ident]
tvs ([[InstanceType]] -> [InstanceType]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[InstanceType]]
tyss)
  where tyss :: [[InstanceType]]
tyss = (ConstrDecl -> [InstanceType]) -> [ConstrDecl] -> [[InstanceType]]
forall a b. (a -> b) -> [a] -> [b]
map ConstrDecl -> [InstanceType]
constrDeclTypes [ConstrDecl]
cs
        constrDeclTypes :: ConstrDecl -> [InstanceType]
constrDeclTypes (ConstrDecl     _ _ tys :: [InstanceType]
tys) = [InstanceType]
tys
        constrDeclTypes (ConOpDecl  _ ty1 :: InstanceType
ty1 _ ty2 :: InstanceType
ty2) = [InstanceType
ty1, InstanceType
ty2]
        constrDeclTypes (RecordDecl      _ _ fs :: [FieldDecl]
fs) = [InstanceType]
tys
          where tys :: [InstanceType]
tys = [InstanceType
ty | FieldDecl _ ls :: [Ident]
ls ty :: InstanceType
ty <- [FieldDecl]
fs, Ident
_ <- [Ident]
ls]
declDeriveDataInfo tcEnv :: TCEnv
tcEnv clsEnv :: ClassEnv
clsEnv (NewtypeDecl p :: SpanInfo
p tc :: Ident
tc tvs :: [Ident]
tvs nc :: NewConstrDecl
nc _) =
  TCEnv
-> ClassEnv
-> SpanInfo
-> Ident
-> [Ident]
-> [InstanceType]
-> StateT INCState Identity DeriveInfo
mkDeriveDataInfo TCEnv
tcEnv ClassEnv
clsEnv SpanInfo
p Ident
tc [Ident]
tvs [NewConstrDecl -> InstanceType
nconstrType NewConstrDecl
nc]
declDeriveDataInfo _ _ _ = String -> StateT INCState Identity DeriveInfo
forall a. String -> a
internalError
  "InstanceCheck.declDeriveDataInfo: no data or newtype declaration"

mkDeriveInfo :: TCEnv -> ClassEnv -> SpanInfo -> Ident -> [Ident]
             -> [TypeExpr] -> [QualIdent] -> INCM DeriveInfo
mkDeriveInfo :: TCEnv
-> ClassEnv
-> SpanInfo
-> Ident
-> [Ident]
-> [InstanceType]
-> [QualIdent]
-> StateT INCState Identity DeriveInfo
mkDeriveInfo tcEnv :: TCEnv
tcEnv clsEnv :: ClassEnv
clsEnv spi :: SpanInfo
spi tc :: Ident
tc tvs :: [Ident]
tvs tys :: [InstanceType]
tys clss :: [QualIdent]
clss = do
  ModuleIdent
m <- INCM ModuleIdent
getModuleIdent
  let otc :: QualIdent
otc = ModuleIdent -> Ident -> QualIdent
qualifyWith ModuleIdent
m Ident
tc
      oclss :: [QualIdent]
oclss = (QualIdent -> QualIdent) -> [QualIdent] -> [QualIdent]
forall a b. (a -> b) -> [a] -> [b]
map ((QualIdent -> TCEnv -> QualIdent)
-> TCEnv -> QualIdent -> QualIdent
forall a b c. (a -> b -> c) -> b -> a -> c
flip (ModuleIdent -> QualIdent -> TCEnv -> QualIdent
getOrigName ModuleIdent
m) TCEnv
tcEnv) [QualIdent]
clss
      PredType ps :: PredSet
ps ty :: Type
ty = ModuleIdent
-> TCEnv
-> ClassEnv
-> QualIdent
-> [Ident]
-> [InstanceType]
-> PredType
expandConstrType ModuleIdent
m TCEnv
tcEnv ClassEnv
clsEnv QualIdent
otc [Ident]
tvs [InstanceType]
tys
      (tys' :: [Type]
tys', ty' :: Type
ty') = Type -> ([Type], Type)
arrowUnapply Type
ty
  DeriveInfo -> StateT INCState Identity DeriveInfo
forall (m :: * -> *) a. Monad m => a -> m a
return (DeriveInfo -> StateT INCState Identity DeriveInfo)
-> DeriveInfo -> StateT INCState Identity DeriveInfo
forall a b. (a -> b) -> a -> b
$ SpanInfo
-> QualIdent -> PredType -> [Type] -> [QualIdent] -> DeriveInfo
DeriveInfo SpanInfo
spi QualIdent
otc (PredSet -> Type -> PredType
PredType PredSet
ps Type
ty') [Type]
tys' ([QualIdent] -> DeriveInfo) -> [QualIdent] -> DeriveInfo
forall a b. (a -> b) -> a -> b
$ ClassEnv -> [QualIdent] -> [QualIdent]
sortClasses ClassEnv
clsEnv [QualIdent]
oclss

mkDeriveDataInfo :: TCEnv -> ClassEnv -> SpanInfo -> Ident -> [Ident]
                 -> [TypeExpr] -> INCM DeriveInfo
mkDeriveDataInfo :: TCEnv
-> ClassEnv
-> SpanInfo
-> Ident
-> [Ident]
-> [InstanceType]
-> StateT INCState Identity DeriveInfo
mkDeriveDataInfo tcEnv :: TCEnv
tcEnv clsEnv :: ClassEnv
clsEnv spi :: SpanInfo
spi tc :: Ident
tc tvs :: [Ident]
tvs tys :: [InstanceType]
tys = do
  ModuleIdent
m <- INCM ModuleIdent
getModuleIdent
  let otc :: QualIdent
otc = ModuleIdent -> Ident -> QualIdent
qualifyWith ModuleIdent
m Ident
tc
      PredType ps :: PredSet
ps ty :: Type
ty = ModuleIdent
-> TCEnv
-> ClassEnv
-> QualIdent
-> [Ident]
-> [InstanceType]
-> PredType
expandConstrType ModuleIdent
m TCEnv
tcEnv ClassEnv
clsEnv QualIdent
otc [Ident]
tvs [InstanceType]
tys
      (tys' :: [Type]
tys', ty' :: Type
ty') = Type -> ([Type], Type)
arrowUnapply Type
ty
  DeriveInfo -> StateT INCState Identity DeriveInfo
forall (m :: * -> *) a. Monad m => a -> m a
return (DeriveInfo -> StateT INCState Identity DeriveInfo)
-> DeriveInfo -> StateT INCState Identity DeriveInfo
forall a b. (a -> b) -> a -> b
$ SpanInfo
-> QualIdent -> PredType -> [Type] -> [QualIdent] -> DeriveInfo
DeriveInfo SpanInfo
spi QualIdent
otc (PredSet -> Type -> PredType
PredType PredSet
ps Type
ty') [Type]
tys' [QualIdent
qDataId]

sortClasses :: ClassEnv -> [QualIdent] -> [QualIdent]
sortClasses :: ClassEnv -> [QualIdent] -> [QualIdent]
sortClasses clsEnv :: ClassEnv
clsEnv clss :: [QualIdent]
clss = ((QualIdent, Int) -> QualIdent)
-> [(QualIdent, Int)] -> [QualIdent]
forall a b. (a -> b) -> [a] -> [b]
map (QualIdent, Int) -> QualIdent
forall a b. (a, b) -> a
fst ([(QualIdent, Int)] -> [QualIdent])
-> [(QualIdent, Int)] -> [QualIdent]
forall a b. (a -> b) -> a -> b
$ ((QualIdent, Int) -> (QualIdent, Int) -> Ordering)
-> [(QualIdent, Int)] -> [(QualIdent, Int)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (QualIdent, Int) -> (QualIdent, Int) -> Ordering
forall a a a. Ord a => (a, a) -> (a, a) -> Ordering
compareDepth ([(QualIdent, Int)] -> [(QualIdent, Int)])
-> [(QualIdent, Int)] -> [(QualIdent, Int)]
forall a b. (a -> b) -> a -> b
$ (QualIdent -> (QualIdent, Int))
-> [QualIdent] -> [(QualIdent, Int)]
forall a b. (a -> b) -> [a] -> [b]
map QualIdent -> (QualIdent, Int)
adjoinDepth [QualIdent]
clss
  where (_, d1 :: a
d1) compareDepth :: (a, a) -> (a, a) -> Ordering
`compareDepth` (_, d2 :: a
d2) = a
d1 a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` a
d2
        adjoinDepth :: QualIdent -> (QualIdent, Int)
adjoinDepth cls :: QualIdent
cls = (QualIdent
cls, [QualIdent] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([QualIdent] -> Int) -> [QualIdent] -> Int
forall a b. (a -> b) -> a -> b
$ QualIdent -> ClassEnv -> [QualIdent]
allSuperClasses QualIdent
cls ClassEnv
clsEnv)

groupDeriveInfos :: [DeriveInfo] -> [[DeriveInfo]]
groupDeriveInfos :: [DeriveInfo] -> [[DeriveInfo]]
groupDeriveInfos = (DeriveInfo -> [QualIdent])
-> (DeriveInfo -> [QualIdent]) -> [DeriveInfo] -> [[DeriveInfo]]
forall b a. Eq b => (a -> [b]) -> (a -> [b]) -> [a] -> [[a]]
scc DeriveInfo -> [QualIdent]
bound DeriveInfo -> [QualIdent]
free
  where bound :: DeriveInfo -> [QualIdent]
bound (DeriveInfo _ tc :: QualIdent
tc _ _ _) = [QualIdent
tc]
        free :: DeriveInfo -> [QualIdent]
free (DeriveInfo _ _ _ tys :: [Type]
tys _) = (Type -> [QualIdent]) -> [Type] -> [QualIdent]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Type -> [QualIdent]
typeConstrs [Type]
tys

bindDerivedInstances :: ClassEnv -> [DeriveInfo] -> INCM ()
bindDerivedInstances :: ClassEnv -> [DeriveInfo] -> INCM ()
bindDerivedInstances clsEnv :: ClassEnv
clsEnv dis :: [DeriveInfo]
dis = Bool -> INCM () -> INCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ((DeriveInfo -> Bool) -> [DeriveInfo] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any DeriveInfo -> Bool
hasDataFunType [DeriveInfo]
dis) (INCM () -> INCM ()) -> INCM () -> INCM ()
forall a b. (a -> b) -> a -> b
$ do
  (DeriveInfo -> INCM ()) -> [DeriveInfo] -> INCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (ClassEnv -> DeriveInfo -> INCM ()
enterInitialPredSet ClassEnv
clsEnv) [DeriveInfo]
dis
  StateT INCState Identity Bool -> INCM ()
forall (m :: * -> *). Monad m => m Bool -> m ()
whileM (StateT INCState Identity Bool -> INCM ())
-> StateT INCState Identity Bool -> INCM ()
forall a b. (a -> b) -> a -> b
$ (DeriveInfo
 -> StateT INCState Identity [((InstIdent, PredSet), Bool)])
-> [DeriveInfo]
-> StateT INCState Identity [((InstIdent, PredSet), Bool)]
forall (m :: * -> *) a b. Monad m => (a -> m [b]) -> [a] -> m [b]
concatMapM (ClassEnv
-> DeriveInfo
-> StateT INCState Identity [((InstIdent, PredSet), Bool)]
inferPredSets ClassEnv
clsEnv) [DeriveInfo]
dis StateT INCState Identity [((InstIdent, PredSet), Bool)]
-> ([((InstIdent, PredSet), Bool)]
    -> StateT INCState Identity Bool)
-> StateT INCState Identity Bool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [((InstIdent, PredSet), Bool)] -> StateT INCState Identity Bool
updatePredSets
  where
    hasDataFunType :: DeriveInfo -> Bool
hasDataFunType (DeriveInfo _ _ _ tys :: [Type]
tys clss :: [QualIdent]
clss) =
      [QualIdent]
clss [QualIdent] -> [QualIdent] -> Bool
forall a. Eq a => a -> a -> Bool
== [QualIdent
qDataId] Bool -> Bool -> Bool
&& (Type -> Bool) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Type -> Bool
isFunType [Type]
tys

enterInitialPredSet :: ClassEnv -> DeriveInfo -> INCM ()
enterInitialPredSet :: ClassEnv -> DeriveInfo -> INCM ()
enterInitialPredSet clsEnv :: ClassEnv
clsEnv (DeriveInfo spi :: SpanInfo
spi tc :: QualIdent
tc pty :: PredType
pty _ clss :: [QualIdent]
clss) =
  (QualIdent -> INCM ()) -> [QualIdent] -> INCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (ClassEnv
-> SpanInfo -> QualIdent -> PredType -> QualIdent -> INCM ()
forall s.
HasSpanInfo s =>
ClassEnv -> s -> QualIdent -> PredType -> QualIdent -> INCM ()
bindDerivedInstance ClassEnv
clsEnv SpanInfo
spi QualIdent
tc PredType
pty) [QualIdent]
clss

-- Note: The methods and arities entered into the instance environment have
-- to match methods and arities of the later generated instance declarations.
-- TODO: Add remark about value environment entry

bindDerivedInstance :: HasSpanInfo s => ClassEnv -> s -> QualIdent -> PredType -> QualIdent
                    -> INCM ()
bindDerivedInstance :: ClassEnv -> s -> QualIdent -> PredType -> QualIdent -> INCM ()
bindDerivedInstance clsEnv :: ClassEnv
clsEnv p :: s
p tc :: QualIdent
tc pty :: PredType
pty cls :: QualIdent
cls = do
  ModuleIdent
m <- INCM ModuleIdent
getModuleIdent
  ((i :: InstIdent
i, ps :: PredSet
ps), _) <- ClassEnv
-> s
-> QualIdent
-> PredType
-> [Type]
-> QualIdent
-> INCM ((InstIdent, PredSet), Bool)
forall s.
HasSpanInfo s =>
ClassEnv
-> s
-> QualIdent
-> PredType
-> [Type]
-> QualIdent
-> INCM ((InstIdent, PredSet), Bool)
inferPredSet ClassEnv
clsEnv s
p QualIdent
tc PredType
pty [] QualIdent
cls
  (InstEnv -> InstEnv) -> INCM ()
modifyInstEnv (InstIdent
-> (ModuleIdent, PredSet, [(Ident, Int)]) -> InstEnv -> InstEnv
bindInstInfo InstIdent
i (ModuleIdent
m, PredSet
ps, [(Ident, Int)]
impls))
  where impls :: [(Ident, Int)]
impls | QualIdent
cls QualIdent -> QualIdent -> Bool
forall a. Eq a => a -> a -> Bool
== QualIdent
qEqId      = [(Ident
eqOpId, 2)]
              | QualIdent
cls QualIdent -> QualIdent -> Bool
forall a. Eq a => a -> a -> Bool
== QualIdent
qOrdId     = [(Ident
leqOpId, 2)]
              | QualIdent
cls QualIdent -> QualIdent -> Bool
forall a. Eq a => a -> a -> Bool
== QualIdent
qEnumId    = [ (Ident
succId, 1), (Ident
predId, 1), (Ident
toEnumId, 1)
                                    , (Ident
fromEnumId, 1), (Ident
enumFromId, 1)
                                    , (Ident
enumFromThenId, 2)
                                    ]
              | QualIdent
cls QualIdent -> QualIdent -> Bool
forall a. Eq a => a -> a -> Bool
== QualIdent
qBoundedId = [(Ident
maxBoundId, 0), (Ident
minBoundId, 0)]
              | QualIdent
cls QualIdent -> QualIdent -> Bool
forall a. Eq a => a -> a -> Bool
== QualIdent
qReadId    = [(Ident
readsPrecId, 2)]
              | QualIdent
cls QualIdent -> QualIdent -> Bool
forall a. Eq a => a -> a -> Bool
== QualIdent
qShowId    = [(Ident
showsPrecId, 2)]
              | QualIdent
cls QualIdent -> QualIdent -> Bool
forall a. Eq a => a -> a -> Bool
== QualIdent
qDataId    = [(Ident
dataEqId, 2), (Ident
aValueId, 0)]
              | Bool
otherwise         =
                String -> [(Ident, Int)]
forall a. String -> a
internalError "InstanceCheck.bindDerivedInstance.impls"

inferPredSets :: ClassEnv -> DeriveInfo -> INCM [((InstIdent, PredSet), Bool)]
inferPredSets :: ClassEnv
-> DeriveInfo
-> StateT INCState Identity [((InstIdent, PredSet), Bool)]
inferPredSets clsEnv :: ClassEnv
clsEnv (DeriveInfo spi :: SpanInfo
spi tc :: QualIdent
tc pty :: PredType
pty tys :: [Type]
tys clss :: [QualIdent]
clss) =
  (QualIdent -> INCM ((InstIdent, PredSet), Bool))
-> [QualIdent]
-> StateT INCState Identity [((InstIdent, PredSet), Bool)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (ClassEnv
-> SpanInfo
-> QualIdent
-> PredType
-> [Type]
-> QualIdent
-> INCM ((InstIdent, PredSet), Bool)
forall s.
HasSpanInfo s =>
ClassEnv
-> s
-> QualIdent
-> PredType
-> [Type]
-> QualIdent
-> INCM ((InstIdent, PredSet), Bool)
inferPredSet ClassEnv
clsEnv SpanInfo
spi QualIdent
tc PredType
pty [Type]
tys) [QualIdent]
clss

inferPredSet :: HasSpanInfo s => ClassEnv -> s -> QualIdent -> PredType -> [Type]
             -> QualIdent -> INCM ((InstIdent, PredSet), Bool)
inferPredSet :: ClassEnv
-> s
-> QualIdent
-> PredType
-> [Type]
-> QualIdent
-> INCM ((InstIdent, PredSet), Bool)
inferPredSet clsEnv :: ClassEnv
clsEnv p :: s
p tc :: QualIdent
tc (PredType ps :: PredSet
ps inst :: Type
inst) tys :: [Type]
tys cls :: QualIdent
cls = do
  ModuleIdent
m <- INCM ModuleIdent
getModuleIdent
  let doc :: Doc
doc = ModuleIdent -> Pred -> Doc
ppPred ModuleIdent
m (Pred -> Doc) -> Pred -> Doc
forall a b. (a -> b) -> a -> b
$ QualIdent -> Type -> Pred
Pred QualIdent
cls Type
inst
      sclss :: [QualIdent]
sclss = QualIdent -> ClassEnv -> [QualIdent]
superClasses QualIdent
cls ClassEnv
clsEnv
      ps' :: PredSet
ps'   = [Pred] -> PredSet
forall a. Ord a => [a] -> Set a
Set.fromList [QualIdent -> Type -> Pred
Pred QualIdent
cls Type
ty | Type
ty <- [Type]
tys]
      ps'' :: PredSet
ps''  = [Pred] -> PredSet
forall a. Ord a => [a] -> Set a
Set.fromList [QualIdent -> Type -> Pred
Pred QualIdent
scls Type
inst | QualIdent
scls <- [QualIdent]
sclss]
      ps''' :: PredSet
ps''' = PredSet
ps PredSet -> PredSet -> PredSet
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` PredSet
ps' PredSet -> PredSet -> PredSet
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` PredSet
ps''
  (ps4 :: PredSet
ps4, novarps :: PredSet
novarps) <-
    Bool
-> s
-> String
-> Doc
-> ClassEnv
-> PredSet
-> INCM (PredSet, PredSet)
forall s.
HasSpanInfo s =>
Bool
-> s
-> String
-> Doc
-> ClassEnv
-> PredSet
-> INCM (PredSet, PredSet)
reducePredSet (QualIdent
cls QualIdent -> QualIdent -> Bool
forall a. Eq a => a -> a -> Bool
== QualIdent
qDataId) s
p "derived instance" Doc
doc ClassEnv
clsEnv PredSet
ps'''
  let ps5 :: [Pred]
ps5 = (Pred -> Bool) -> [Pred] -> [Pred]
forall a. (a -> Bool) -> [a] -> [a]
filter Pred -> Bool
noPolyPred ([Pred] -> [Pred]) -> [Pred] -> [Pred]
forall a b. (a -> b) -> a -> b
$ PredSet -> [Pred]
forall a. Set a -> [a]
Set.toList PredSet
ps4
  if (Pred -> Bool) -> [Pred] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (ModuleIdent -> Pred -> Bool
forall p. p -> Pred -> Bool
isDataPred ModuleIdent
m) (PredSet -> [Pred]
forall a. Set a -> [a]
Set.toList PredSet
novarps [Pred] -> [Pred] -> [Pred]
forall a. [a] -> [a] -> [a]
++ [Pred]
ps5) Bool -> Bool -> Bool
&& QualIdent
cls QualIdent -> QualIdent -> Bool
forall a. Eq a => a -> a -> Bool
== QualIdent
qDataId
    then ((InstIdent, PredSet), Bool) -> INCM ((InstIdent, PredSet), Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return    (((QualIdent
cls, QualIdent
tc), PredSet
ps4), Bool
False)
    else (Pred -> INCM ()) -> [Pred] -> INCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (s -> String -> Doc -> Pred -> INCM ()
forall s. HasSpanInfo s => s -> String -> Doc -> Pred -> INCM ()
reportUndecidable s
p "derived instance" Doc
doc) [Pred]
ps5
         INCM ()
-> INCM ((InstIdent, PredSet), Bool)
-> INCM ((InstIdent, PredSet), Bool)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ((InstIdent, PredSet), Bool) -> INCM ((InstIdent, PredSet), Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return (((QualIdent
cls, QualIdent
tc), PredSet
ps4), Bool
True)
  where
    noPolyPred :: Pred -> Bool
noPolyPred (Pred _ (TypeVariable _)) = Bool
False
    noPolyPred (Pred _ _               ) = Bool
True
    isDataPred :: p -> Pred -> Bool
isDataPred _ (Pred qid :: QualIdent
qid _) = QualIdent
qid QualIdent -> QualIdent -> Bool
forall a. Eq a => a -> a -> Bool
== QualIdent
qDataId

updatePredSets :: [((InstIdent, PredSet), Bool)] -> INCM Bool
updatePredSets :: [((InstIdent, PredSet), Bool)] -> StateT INCState Identity Bool
updatePredSets = ([Bool] -> Bool)
-> StateT INCState Identity [Bool] -> StateT INCState Identity Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or (StateT INCState Identity [Bool] -> StateT INCState Identity Bool)
-> ([((InstIdent, PredSet), Bool)]
    -> StateT INCState Identity [Bool])
-> [((InstIdent, PredSet), Bool)]
-> StateT INCState Identity Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (((InstIdent, PredSet), Bool) -> StateT INCState Identity Bool)
-> [((InstIdent, PredSet), Bool)]
-> StateT INCState Identity [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (((InstIdent, PredSet) -> Bool -> StateT INCState Identity Bool)
-> ((InstIdent, PredSet), Bool) -> StateT INCState Identity Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (InstIdent, PredSet) -> Bool -> StateT INCState Identity Bool
updatePredSet)

updatePredSet :: (InstIdent, PredSet) -> Bool -> INCM Bool
updatePredSet :: (InstIdent, PredSet) -> Bool -> StateT INCState Identity Bool
updatePredSet (i :: InstIdent
i, ps :: PredSet
ps) enter :: Bool
enter = do
  InstEnv
inEnv <- INCM InstEnv
getInstEnv
  case InstIdent
-> InstEnv -> Maybe (ModuleIdent, PredSet, [(Ident, Int)])
lookupInstInfo InstIdent
i InstEnv
inEnv of
    Just (m :: ModuleIdent
m, ps' :: PredSet
ps', is :: [(Ident, Int)]
is)
      | Bool -> Bool
not Bool
enter -> (InstEnv -> InstEnv) -> INCM ()
modifyInstEnv (InstIdent -> InstEnv -> InstEnv
removeInstInfo InstIdent
i) INCM ()
-> StateT INCState Identity Bool -> StateT INCState Identity Bool
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> StateT INCState Identity Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
      | PredSet
ps PredSet -> PredSet -> Bool
forall a. Eq a => a -> a -> Bool
== PredSet
ps' -> Bool -> StateT INCState Identity Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
      | Bool
otherwise -> do
        (InstEnv -> InstEnv) -> INCM ()
modifyInstEnv ((InstEnv -> InstEnv) -> INCM ())
-> (InstEnv -> InstEnv) -> INCM ()
forall a b. (a -> b) -> a -> b
$ InstIdent
-> (ModuleIdent, PredSet, [(Ident, Int)]) -> InstEnv -> InstEnv
bindInstInfo InstIdent
i (ModuleIdent
m, PredSet
ps, [(Ident, Int)]
is)
        Bool -> StateT INCState Identity Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    Nothing -> String -> StateT INCState Identity Bool
forall a. String -> a
internalError "InstanceCheck.updatePredSet"

reportUndecidable :: HasSpanInfo s => s -> String -> Doc -> Pred -> INCM ()
reportUndecidable :: s -> String -> Doc -> Pred -> INCM ()
reportUndecidable p :: s
p what :: String
what doc :: Doc
doc predicate :: Pred
predicate@(Pred _ ty :: Type
ty) = do
  ModuleIdent
m <- INCM ModuleIdent
getModuleIdent
  case Type
ty of
    TypeVariable _ -> () -> INCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    _ -> Message -> INCM ()
report (Message -> INCM ()) -> Message -> INCM ()
forall a b. (a -> b) -> a -> b
$ ModuleIdent -> s -> String -> Doc -> Pred -> Message
forall s.
HasSpanInfo s =>
ModuleIdent -> s -> String -> Doc -> Pred -> Message
errMissingInstance ModuleIdent
m s
p String
what Doc
doc Pred
predicate

-- Then, the compiler checks the contexts of all explicit instance
-- declarations to detect missing super class instances. For an instance
-- declaration
--
-- instance cx => C (T u_1 ... u_k) where ...
--
-- the compiler ensures that T is an instance of all of C's super classes
-- and also that the contexts of the corresponding instance declarations are
-- satisfied by cx.

checkInstance :: TCEnv -> ClassEnv -> Decl a -> INCM ()
checkInstance :: TCEnv -> ClassEnv -> Decl a -> INCM ()
checkInstance tcEnv :: TCEnv
tcEnv clsEnv :: ClassEnv
clsEnv (InstanceDecl _ _ cx :: Context
cx cls :: QualIdent
cls inst :: InstanceType
inst _) = do
  ModuleIdent
m <- INCM ModuleIdent
getModuleIdent
  let PredType ps :: PredSet
ps ty :: Type
ty = ModuleIdent -> TCEnv -> ClassEnv -> QualTypeExpr -> PredType
expandPolyType ModuleIdent
m TCEnv
tcEnv ClassEnv
clsEnv (QualTypeExpr -> PredType) -> QualTypeExpr -> PredType
forall a b. (a -> b) -> a -> b
$
                         SpanInfo -> Context -> InstanceType -> QualTypeExpr
QualTypeExpr SpanInfo
NoSpanInfo Context
cx InstanceType
inst
      ocls :: QualIdent
ocls = ModuleIdent -> QualIdent -> TCEnv -> QualIdent
getOrigName ModuleIdent
m QualIdent
cls TCEnv
tcEnv
      ps' :: PredSet
ps' = [Pred] -> PredSet
forall a. Ord a => [a] -> Set a
Set.fromList [ QualIdent -> Type -> Pred
Pred QualIdent
scls Type
ty | QualIdent
scls <- QualIdent -> ClassEnv -> [QualIdent]
superClasses QualIdent
ocls ClassEnv
clsEnv ]
      doc :: Doc
doc = ModuleIdent -> Pred -> Doc
ppPred ModuleIdent
m (Pred -> Doc) -> Pred -> Doc
forall a b. (a -> b) -> a -> b
$ QualIdent -> Type -> Pred
Pred QualIdent
cls Type
ty
      what :: String
what = "instance declaration"
  (ps'' :: PredSet
ps'', _) <- Bool
-> InstanceType
-> String
-> Doc
-> ClassEnv
-> PredSet
-> INCM (PredSet, PredSet)
forall s.
HasSpanInfo s =>
Bool
-> s
-> String
-> Doc
-> ClassEnv
-> PredSet
-> INCM (PredSet, PredSet)
reducePredSet Bool
False InstanceType
inst String
what Doc
doc ClassEnv
clsEnv PredSet
ps'
  (Pred -> INCM ()) -> PredSet -> INCM ()
forall (m :: * -> *) b a.
(Monad m, Ord b) =>
(a -> m b) -> Set a -> m ()
Set.mapM_ (Message -> INCM ()
report (Message -> INCM ()) -> (Pred -> Message) -> Pred -> INCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleIdent -> InstanceType -> String -> Doc -> Pred -> Message
forall s.
HasSpanInfo s =>
ModuleIdent -> s -> String -> Doc -> Pred -> Message
errMissingInstance ModuleIdent
m InstanceType
inst String
what Doc
doc) (PredSet -> INCM ()) -> PredSet -> INCM ()
forall a b. (a -> b) -> a -> b
$
    PredSet
ps'' PredSet -> PredSet -> PredSet
forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` ClassEnv -> PredSet -> PredSet
maxPredSet ClassEnv
clsEnv PredSet
ps
checkInstance _ _ _ = INCM ()
ok

-- All types specified in the optional default declaration of a module
-- must be instances of the Num class. Since these types are used to resolve
-- ambiguous type variables, the predicate sets of the respective instances
-- must be empty.

checkDefault :: TCEnv -> ClassEnv -> Decl a -> INCM ()
checkDefault :: TCEnv -> ClassEnv -> Decl a -> INCM ()
checkDefault tcEnv :: TCEnv
tcEnv clsEnv :: ClassEnv
clsEnv (DefaultDecl _ tys :: [InstanceType]
tys) =
  (InstanceType -> INCM ()) -> [InstanceType] -> INCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (TCEnv -> ClassEnv -> InstanceType -> INCM ()
checkDefaultType TCEnv
tcEnv ClassEnv
clsEnv) [InstanceType]
tys
checkDefault _ _ _ = INCM ()
ok

checkDefaultType :: TCEnv -> ClassEnv -> TypeExpr -> INCM ()
checkDefaultType :: TCEnv -> ClassEnv -> InstanceType -> INCM ()
checkDefaultType tcEnv :: TCEnv
tcEnv clsEnv :: ClassEnv
clsEnv ty :: InstanceType
ty = do
  ModuleIdent
m <- INCM ModuleIdent
getModuleIdent
  let PredType _ ty' :: Type
ty' = ModuleIdent -> TCEnv -> ClassEnv -> QualTypeExpr -> PredType
expandPolyType ModuleIdent
m TCEnv
tcEnv ClassEnv
clsEnv (QualTypeExpr -> PredType) -> QualTypeExpr -> PredType
forall a b. (a -> b) -> a -> b
$
                         SpanInfo -> Context -> InstanceType -> QualTypeExpr
QualTypeExpr SpanInfo
NoSpanInfo [] InstanceType
ty
  (ps :: PredSet
ps, _) <- Bool
-> InstanceType
-> String
-> Doc
-> ClassEnv
-> PredSet
-> INCM (PredSet, PredSet)
forall s.
HasSpanInfo s =>
Bool
-> s
-> String
-> Doc
-> ClassEnv
-> PredSet
-> INCM (PredSet, PredSet)
reducePredSet Bool
False InstanceType
ty String
what Doc
empty ClassEnv
clsEnv
    (Pred -> PredSet
forall a. a -> Set a
Set.singleton (Pred -> PredSet) -> Pred -> PredSet
forall a b. (a -> b) -> a -> b
$ QualIdent -> Type -> Pred
Pred QualIdent
qNumId Type
ty')
  (Pred -> INCM ()) -> PredSet -> INCM ()
forall (m :: * -> *) b a.
(Monad m, Ord b) =>
(a -> m b) -> Set a -> m ()
Set.mapM_ (Message -> INCM ()
report (Message -> INCM ()) -> (Pred -> Message) -> Pred -> INCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleIdent -> InstanceType -> String -> Doc -> Pred -> Message
forall s.
HasSpanInfo s =>
ModuleIdent -> s -> String -> Doc -> Pred -> Message
errMissingInstance ModuleIdent
m InstanceType
ty String
what Doc
empty) PredSet
ps
  where what :: String
what = "default declaration"

-- The function 'reducePredSet' simplifies a predicate set of the form
-- (C_1 tau_1,..,C_n tau_n) where the tau_i are arbitrary types into a
-- predicate set where all predicates are of the form C u with u being
-- a type variable. An error is reported if the predicate set cannot
-- be transformed into this form. In addition, we remove all predicates
-- that are implied by others within the same set.
-- When the flag is set, all missing Data preds are ignored

reducePredSet :: HasSpanInfo s => Bool -> s -> String -> Doc -> ClassEnv -> PredSet
              -> INCM (PredSet, PredSet)
reducePredSet :: Bool
-> s
-> String
-> Doc
-> ClassEnv
-> PredSet
-> INCM (PredSet, PredSet)
reducePredSet b :: Bool
b p :: s
p what :: String
what doc :: Doc
doc clsEnv :: ClassEnv
clsEnv ps :: PredSet
ps = do
  ModuleIdent
m <- INCM ModuleIdent
getModuleIdent
  InstEnv
inEnv <- INCM InstEnv
getInstEnv
  let (ps1 :: PredSet
ps1, ps2 :: PredSet
ps2) = PredSet -> (PredSet, PredSet)
partitionPredSet (PredSet -> (PredSet, PredSet)) -> PredSet -> (PredSet, PredSet)
forall a b. (a -> b) -> a -> b
$ ClassEnv -> PredSet -> PredSet
minPredSet ClassEnv
clsEnv (PredSet -> PredSet) -> PredSet -> PredSet
forall a b. (a -> b) -> a -> b
$ InstEnv -> PredSet -> PredSet
reducePreds InstEnv
inEnv PredSet
ps
      ps2' :: PredSet
ps2' = if Bool
b then (Pred -> Bool) -> PredSet -> PredSet
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (ModuleIdent -> Pred -> Bool
forall p. p -> Pred -> Bool
isNotDataPred ModuleIdent
m) PredSet
ps2 else PredSet
ps2
  (Pred -> INCM ()) -> PredSet -> INCM ()
forall (m :: * -> *) b a.
(Monad m, Ord b) =>
(a -> m b) -> Set a -> m ()
Set.mapM_ (ModuleIdent -> Pred -> INCM ()
reportMissing ModuleIdent
m) PredSet
ps2' INCM () -> INCM (PredSet, PredSet) -> INCM (PredSet, PredSet)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (PredSet, PredSet) -> INCM (PredSet, PredSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (PredSet
ps1, PredSet
ps2)
  where
    isNotDataPred :: p -> Pred -> Bool
isNotDataPred _ (Pred qid :: QualIdent
qid _) = QualIdent
qid QualIdent -> QualIdent -> Bool
forall a. Eq a => a -> a -> Bool
/= QualIdent
qDataId
    reportMissing :: ModuleIdent -> Pred -> INCM ()
reportMissing m :: ModuleIdent
m pr :: Pred
pr@(Pred _ _) =
      Message -> INCM ()
report (Message -> INCM ()) -> Message -> INCM ()
forall a b. (a -> b) -> a -> b
$ ModuleIdent -> s -> String -> Doc -> Pred -> Message
forall s.
HasSpanInfo s =>
ModuleIdent -> s -> String -> Doc -> Pred -> Message
errMissingInstance ModuleIdent
m s
p String
what Doc
doc Pred
pr
    reducePreds :: InstEnv -> PredSet -> PredSet
reducePreds inEnv :: InstEnv
inEnv = (Pred -> PredSet) -> PredSet -> PredSet
forall a b. (Ord a, Ord b) => (a -> Set b) -> Set a -> Set b
Set.concatMap ((Pred -> PredSet) -> PredSet -> PredSet)
-> (Pred -> PredSet) -> PredSet -> PredSet
forall a b. (a -> b) -> a -> b
$ InstEnv -> Pred -> PredSet
reducePred InstEnv
inEnv
    reducePred :: InstEnv -> Pred -> PredSet
reducePred inEnv :: InstEnv
inEnv predicate :: Pred
predicate = PredSet -> (PredSet -> PredSet) -> Maybe PredSet -> PredSet
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Pred -> PredSet
forall a. a -> Set a
Set.singleton Pred
predicate)
                                       (InstEnv -> PredSet -> PredSet
reducePreds InstEnv
inEnv)
                                       (InstEnv -> Pred -> Maybe PredSet
instPredSet InstEnv
inEnv Pred
predicate)

instPredSet :: InstEnv -> Pred -> Maybe PredSet
instPredSet :: InstEnv -> Pred -> Maybe PredSet
instPredSet inEnv :: InstEnv
inEnv (Pred qcls :: QualIdent
qcls ty :: Type
ty) =
  case Bool -> Type -> (Type, [Type])
unapplyType Bool
False Type
ty of
    (TypeConstructor tc :: QualIdent
tc, tys :: [Type]
tys) ->
      ((ModuleIdent, PredSet, [(Ident, Int)]) -> PredSet)
-> Maybe (ModuleIdent, PredSet, [(Ident, Int)]) -> Maybe PredSet
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Type] -> PredSet -> PredSet
forall a. ExpandAliasType a => [Type] -> a -> a
expandAliasType [Type]
tys (PredSet -> PredSet)
-> ((ModuleIdent, PredSet, [(Ident, Int)]) -> PredSet)
-> (ModuleIdent, PredSet, [(Ident, Int)])
-> PredSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModuleIdent, PredSet, [(Ident, Int)]) -> PredSet
forall a b c. (a, b, c) -> b
snd3) (InstIdent
-> InstEnv -> Maybe (ModuleIdent, PredSet, [(Ident, Int)])
lookupInstInfo (QualIdent
qcls, QualIdent
tc) InstEnv
inEnv)
    _ -> Maybe PredSet
forall a. Maybe a
Nothing

-- ---------------------------------------------------------------------------
-- Auxiliary definitions
-- ---------------------------------------------------------------------------

genInstIdents :: ModuleIdent -> TCEnv -> Decl a -> [InstIdent]
genInstIdents :: ModuleIdent -> TCEnv -> Decl a -> [InstIdent]
genInstIdents m :: ModuleIdent
m tcEnv :: TCEnv
tcEnv (DataDecl    _ tc :: Ident
tc _ _ qclss :: [QualIdent]
qclss) =
  (QualIdent -> InstIdent) -> [QualIdent] -> [InstIdent]
forall a b. (a -> b) -> [a] -> [b]
map ((QualIdent -> InstanceType -> InstIdent)
-> InstanceType -> QualIdent -> InstIdent
forall a b c. (a -> b -> c) -> b -> a -> c
flip (ModuleIdent -> TCEnv -> QualIdent -> InstanceType -> InstIdent
genInstIdent ModuleIdent
m TCEnv
tcEnv) (InstanceType -> QualIdent -> InstIdent)
-> InstanceType -> QualIdent -> InstIdent
forall a b. (a -> b) -> a -> b
$ SpanInfo -> QualIdent -> InstanceType
ConstructorType SpanInfo
NoSpanInfo (QualIdent -> InstanceType) -> QualIdent -> InstanceType
forall a b. (a -> b) -> a -> b
$ Ident -> QualIdent
qualify Ident
tc)
      [QualIdent]
qclss
genInstIdents m :: ModuleIdent
m tcEnv :: TCEnv
tcEnv (NewtypeDecl _ tc :: Ident
tc _ _ qclss :: [QualIdent]
qclss) =
  (QualIdent -> InstIdent) -> [QualIdent] -> [InstIdent]
forall a b. (a -> b) -> [a] -> [b]
map ((QualIdent -> InstanceType -> InstIdent)
-> InstanceType -> QualIdent -> InstIdent
forall a b c. (a -> b -> c) -> b -> a -> c
flip (ModuleIdent -> TCEnv -> QualIdent -> InstanceType -> InstIdent
genInstIdent ModuleIdent
m TCEnv
tcEnv) (InstanceType -> QualIdent -> InstIdent)
-> InstanceType -> QualIdent -> InstIdent
forall a b. (a -> b) -> a -> b
$ SpanInfo -> QualIdent -> InstanceType
ConstructorType SpanInfo
NoSpanInfo (QualIdent -> InstanceType) -> QualIdent -> InstanceType
forall a b. (a -> b) -> a -> b
$ Ident -> QualIdent
qualify Ident
tc)
      [QualIdent]
qclss
genInstIdents m :: ModuleIdent
m tcEnv :: TCEnv
tcEnv (InstanceDecl _ _ _ qcls :: QualIdent
qcls ty :: InstanceType
ty _) =
  [ModuleIdent -> TCEnv -> QualIdent -> InstanceType -> InstIdent
genInstIdent ModuleIdent
m TCEnv
tcEnv QualIdent
qcls InstanceType
ty]
genInstIdents _ _     _                            = []

genInstIdent :: ModuleIdent -> TCEnv -> QualIdent -> TypeExpr -> InstIdent
genInstIdent :: ModuleIdent -> TCEnv -> QualIdent -> InstanceType -> InstIdent
genInstIdent m :: ModuleIdent
m tcEnv :: TCEnv
tcEnv qcls :: QualIdent
qcls = ModuleIdent -> TCEnv -> InstIdent -> InstIdent
qualInstIdent ModuleIdent
m TCEnv
tcEnv (InstIdent -> InstIdent)
-> (InstanceType -> InstIdent) -> InstanceType -> InstIdent
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (,) QualIdent
qcls (QualIdent -> InstIdent)
-> (InstanceType -> QualIdent) -> InstanceType -> InstIdent
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InstanceType -> QualIdent
typeConstr

-- When qualifiying an instance identifier, we replace both the class and
-- type constructor with their original names as found in the type constructor
-- environment.

qualInstIdent :: ModuleIdent -> TCEnv -> InstIdent -> InstIdent
qualInstIdent :: ModuleIdent -> TCEnv -> InstIdent -> InstIdent
qualInstIdent m :: ModuleIdent
m tcEnv :: TCEnv
tcEnv (cls :: QualIdent
cls, tc :: QualIdent
tc) = (QualIdent -> QualIdent
qual QualIdent
cls, QualIdent -> QualIdent
qual QualIdent
tc)
  where
    qual :: QualIdent -> QualIdent
qual = (QualIdent -> TCEnv -> QualIdent)
-> TCEnv -> QualIdent -> QualIdent
forall a b c. (a -> b -> c) -> b -> a -> c
flip (ModuleIdent -> QualIdent -> TCEnv -> QualIdent
getOrigName ModuleIdent
m) TCEnv
tcEnv

unqualInstIdent :: TCEnv -> InstIdent -> InstIdent
unqualInstIdent :: TCEnv -> InstIdent -> InstIdent
unqualInstIdent tcEnv :: TCEnv
tcEnv (qcls :: QualIdent
qcls, tc :: QualIdent
tc) = (QualIdent -> QualIdent
unqual QualIdent
qcls, QualIdent -> QualIdent
unqual QualIdent
tc)
  where
    unqual :: QualIdent -> QualIdent
unqual = [QualIdent] -> QualIdent
forall a. [a] -> a
head ([QualIdent] -> QualIdent)
-> (QualIdent -> [QualIdent]) -> QualIdent -> QualIdent
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (QualIdent -> TCEnv -> [QualIdent])
-> TCEnv -> QualIdent -> [QualIdent]
forall a b c. (a -> b -> c) -> b -> a -> c
flip QualIdent -> TCEnv -> [QualIdent]
reverseLookupByOrigName TCEnv
tcEnv

isFunType :: Type -> Bool
isFunType :: Type -> Bool
isFunType (TypeArrow         _ _) = Bool
True
isFunType (TypeApply       t1 :: Type
t1 t2 :: Type
t2) = Type -> Bool
isFunType Type
t1 Bool -> Bool -> Bool
|| Type -> Bool
isFunType Type
t2
isFunType (TypeForall      _  ty :: Type
ty) = Type -> Bool
isFunType Type
ty
isFunType (TypeConstrained tys :: [Type]
tys _) = (Type -> Bool) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Type -> Bool
isFunType [Type]
tys
isFunType _                       = Bool
False

-- ---------------------------------------------------------------------------
-- Error messages
-- ---------------------------------------------------------------------------

errMultipleInstances :: TCEnv -> [InstSource] -> Message
errMultipleInstances :: TCEnv -> [InstSource] -> Message
errMultipleInstances tcEnv :: TCEnv
tcEnv iss :: [InstSource]
iss = Doc -> Message
message (Doc -> Message) -> Doc -> Message
forall a b. (a -> b) -> a -> b
$
  String -> Doc
text "Multiple instances for the same class and type" Doc -> Doc -> Doc
$+$
    Int -> Doc -> Doc
nest 2 ([Doc] -> Doc
vcat ((InstSource -> Doc) -> [InstSource] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map InstSource -> Doc
ppInstSource [InstSource]
iss))
  where
    ppInstSource :: InstSource -> Doc
ppInstSource (InstSource i :: InstIdent
i m :: ModuleIdent
m) = InstIdent -> Doc
ppInstIdent (TCEnv -> InstIdent -> InstIdent
unqualInstIdent TCEnv
tcEnv InstIdent
i) Doc -> Doc -> Doc
<+>
      Doc -> Doc
parens (String -> Doc
text "defined in" Doc -> Doc -> Doc
<+> ModuleIdent -> Doc
ppMIdent ModuleIdent
m)

errMissingInstance :: HasSpanInfo s => ModuleIdent -> s -> String -> Doc -> Pred
                   -> Message
errMissingInstance :: ModuleIdent -> s -> String -> Doc -> Pred -> Message
errMissingInstance m :: ModuleIdent
m p :: s
p what :: String
what doc :: Doc
doc predicate :: Pred
predicate = SpanInfo -> Doc -> Message
forall s. HasSpanInfo s => s -> Doc -> Message
spanInfoMessage (s -> SpanInfo
forall a. HasSpanInfo a => a -> SpanInfo
getSpanInfo s
p) (Doc -> Message) -> Doc -> Message
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
vcat
  [ String -> Doc
text "Missing instance for" Doc -> Doc -> Doc
<+> ModuleIdent -> Pred -> Doc
ppPred ModuleIdent
m Pred
predicate
  , String -> Doc
text "in" Doc -> Doc -> Doc
<+> String -> Doc
text String
what Doc -> Doc -> Doc
<+> Doc
doc
  ]