{- |
    Module      :  $Header$
    Description :  Checks consistency of interface files
    Copyright   :  (c) 2000 - 2007 Wolfgang Lux
                       2015        Jan Tikovsky
                       2016        Finn Teegen
    License     :  BSD-3-clause

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

   Interface files include declarations of all entities that are exported
   by the module, but defined in another module. Since these declarations
   can become inconsistent if client modules are not recompiled properly,
   the compiler checks that all imported declarations in an interface
   agree with their original definitions.

   One may ask why we include imported declarations at all, if the
   compiler always has to compare those declarations with the original
   definitions. The main reason for this is that it helps to avoid
   unnecessary recompilations of client modules. As an example, consider
   the three modules:

     module A where { data T = C }
     module B(T(..)) where { import A }
     module C where { import B; f = C }

   where module B could be considered as a public interface of module A,
   which restricts access to type A.T and its constructor C.
   The client module C imports this type via the public interface B.
   If now module A is changed by adding a definition of a new global function

     module A where { data T = C; f = C }

   module B must be recompiled because A's interface is changed.
   On the other hand, module C need not be recompiled because the change in
   A does not affect B's interface. By including the declaration of type A.T
   in B's interface, the compiler can trivially check that B's interface
   remains unchanged and therefore the client module C is not recompiled.

   Another reason for including imported declarations in interfaces is
   that the compiler in principle could avoid loading interfaces of
   modules that are imported only indirectly, which would save processing
   time and allow distributing binary packages of a library with a public
   interface module only. However, this has not been implemented yet.
-}

module Checks.InterfaceCheck (interfaceCheck) where

import           Control.Monad            (unless)
import qualified Control.Monad.State as S
import           Data.List                (sort)
import           Data.Maybe               (fromMaybe)

import Curry.Base.Ident
import Curry.Base.Position
import Curry.Base.SpanInfo
import Curry.Base.Pretty
import Curry.Syntax

import Base.CurryKinds (toKind')
import Base.CurryTypes
import Base.Messages (Message, posMessage, internalError)
import Base.TopEnv
import Base.Types

import Env.Class
import Env.Instance
import Env.OpPrec
import Env.TypeConstructor
import Env.Value

data ICState = ICState
  { ICState -> ModuleIdent
moduleIdent :: ModuleIdent
  , ICState -> OpPrecEnv
precEnv     :: OpPrecEnv
  , ICState -> TCEnv
tyConsEnv   :: TCEnv
  , ICState -> ClassEnv
classEnv    :: ClassEnv
  , ICState -> InstEnv
instEnv     :: InstEnv
  , ICState -> ValueEnv
valueEnv    :: ValueEnv
  , ICState -> [Message]
errors      :: [Message]
  }

type IC = S.State ICState

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

getPrecEnv :: IC OpPrecEnv
getPrecEnv :: IC OpPrecEnv
getPrecEnv = (ICState -> OpPrecEnv) -> IC OpPrecEnv
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
S.gets ICState -> OpPrecEnv
precEnv

getTyConsEnv :: IC TCEnv
getTyConsEnv :: IC TCEnv
getTyConsEnv = (ICState -> TCEnv) -> IC TCEnv
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
S.gets ICState -> TCEnv
tyConsEnv

getClassEnv :: IC ClassEnv
getClassEnv :: IC ClassEnv
getClassEnv = (ICState -> ClassEnv) -> IC ClassEnv
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
S.gets ICState -> ClassEnv
classEnv

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

getValueEnv :: IC ValueEnv
getValueEnv :: IC ValueEnv
getValueEnv = (ICState -> ValueEnv) -> IC ValueEnv
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
S.gets ICState -> ValueEnv
valueEnv

-- |Report a syntax error
report :: Message -> IC ()
report :: Message -> IC ()
report msg :: Message
msg = (ICState -> ICState) -> IC ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
S.modify ((ICState -> ICState) -> IC ()) -> (ICState -> ICState) -> IC ()
forall a b. (a -> b) -> a -> b
$ \s :: ICState
s -> ICState
s { errors :: [Message]
errors = Message
msg Message -> [Message] -> [Message]
forall a. a -> [a] -> [a]
: ICState -> [Message]
errors ICState
s }

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

interfaceCheck :: OpPrecEnv -> TCEnv -> ClassEnv -> InstEnv -> ValueEnv
               -> Interface -> [Message]
interfaceCheck :: OpPrecEnv
-> TCEnv
-> ClassEnv
-> InstEnv
-> ValueEnv
-> Interface
-> [Message]
interfaceCheck pEnv :: OpPrecEnv
pEnv tcEnv :: TCEnv
tcEnv clsEnv :: ClassEnv
clsEnv inEnv :: InstEnv
inEnv tyEnv :: ValueEnv
tyEnv (Interface m :: ModuleIdent
m _ ds :: [IDecl]
ds) = [Message] -> [Message]
forall a. [a] -> [a]
reverse (ICState -> [Message]
errors ICState
s)
  where s :: ICState
s = IC () -> ICState -> ICState
forall s a. State s a -> s -> s
S.execState ((IDecl -> IC ()) -> [IDecl] -> IC ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ IDecl -> IC ()
checkImport [IDecl]
ds) ICState
initState
        initState :: ICState
initState = ModuleIdent
-> OpPrecEnv
-> TCEnv
-> ClassEnv
-> InstEnv
-> ValueEnv
-> [Message]
-> ICState
ICState ModuleIdent
m OpPrecEnv
pEnv TCEnv
tcEnv ClassEnv
clsEnv InstEnv
inEnv ValueEnv
tyEnv []

checkImport :: IDecl -> IC ()
checkImport :: IDecl -> IC ()
checkImport (IInfixDecl p :: Position
p fix :: Infix
fix pr :: Precedence
pr op :: QualIdent
op) = (PrecInfo -> Bool) -> Position -> QualIdent -> IC ()
checkPrecInfo PrecInfo -> Bool
check Position
p QualIdent
op
  where check :: PrecInfo -> Bool
check (PrecInfo op' :: QualIdent
op' (OpPrec fix' :: Infix
fix' pr' :: Precedence
pr')) =
          QualIdent
op QualIdent -> QualIdent -> Bool
forall a. Eq a => a -> a -> Bool
== QualIdent
op' Bool -> Bool -> Bool
&& Infix
fix Infix -> Infix -> Bool
forall a. Eq a => a -> a -> Bool
== Infix
fix' Bool -> Bool -> Bool
&& Precedence
pr Precedence -> Precedence -> Bool
forall a. Eq a => a -> a -> Bool
== Precedence
pr'
checkImport (HidingDataDecl p :: Position
p tc :: QualIdent
tc k :: Maybe KindExpr
k tvs :: [Ident]
tvs) =
  String
-> (TypeInfo -> Maybe (IC ())) -> Position -> QualIdent -> IC ()
checkTypeInfo "hidden data type" TypeInfo -> Maybe (IC ())
check Position
p QualIdent
tc
  where check :: TypeInfo -> Maybe (IC ())
check (DataType     tc' :: QualIdent
tc' k' :: Kind
k' _)
          | QualIdent
tc QualIdent -> QualIdent -> Bool
forall a. Eq a => a -> a -> Bool
== QualIdent
tc' Bool -> Bool -> Bool
&& Maybe KindExpr -> Int -> Kind
toKind' Maybe KindExpr
k ([Ident] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Ident]
tvs) Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
k' = IC () -> Maybe (IC ())
forall a. a -> Maybe a
Just IC ()
ok
        check (RenamingType tc' :: QualIdent
tc' k' :: Kind
k' _)
          | QualIdent
tc QualIdent -> QualIdent -> Bool
forall a. Eq a => a -> a -> Bool
== QualIdent
tc' Bool -> Bool -> Bool
&& Maybe KindExpr -> Int -> Kind
toKind' Maybe KindExpr
k ([Ident] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Ident]
tvs) Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
k' = IC () -> Maybe (IC ())
forall a. a -> Maybe a
Just IC ()
ok
        check _ = Maybe (IC ())
forall a. Maybe a
Nothing
checkImport (IDataDecl p :: Position
p tc :: QualIdent
tc k :: Maybe KindExpr
k tvs :: [Ident]
tvs cs :: [ConstrDecl]
cs _) = String
-> (TypeInfo -> Maybe (IC ())) -> Position -> QualIdent -> IC ()
checkTypeInfo "data type" TypeInfo -> Maybe (IC ())
check Position
p QualIdent
tc
  where check :: TypeInfo -> Maybe (IC ())
check (DataType     tc' :: QualIdent
tc' k' :: Kind
k' cs' :: [DataConstr]
cs')
          | QualIdent
tc QualIdent -> QualIdent -> Bool
forall a. Eq a => a -> a -> Bool
== QualIdent
tc' Bool -> Bool -> Bool
&& Maybe KindExpr -> Int -> Kind
toKind' Maybe KindExpr
k ([Ident] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Ident]
tvs) Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
k' Bool -> Bool -> Bool
&&
            ([ConstrDecl] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [ConstrDecl]
cs Bool -> Bool -> Bool
|| (ConstrDecl -> Ident) -> [ConstrDecl] -> [Ident]
forall a b. (a -> b) -> [a] -> [b]
map ConstrDecl -> Ident
constrId [ConstrDecl]
cs [Ident] -> [Ident] -> Bool
forall a. Eq a => a -> a -> Bool
== (DataConstr -> Ident) -> [DataConstr] -> [Ident]
forall a b. (a -> b) -> [a] -> [b]
map DataConstr -> Ident
constrIdent [DataConstr]
cs')
          = IC () -> Maybe (IC ())
forall a. a -> Maybe a
Just ((ConstrDecl -> IC ()) -> [ConstrDecl] -> IC ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (QualIdent -> [Ident] -> ConstrDecl -> IC ()
checkConstrImport QualIdent
tc [Ident]
tvs) [ConstrDecl]
cs)
        check (RenamingType tc' :: QualIdent
tc' k' :: Kind
k'   _)
          | QualIdent
tc QualIdent -> QualIdent -> Bool
forall a. Eq a => a -> a -> Bool
== QualIdent
tc' Bool -> Bool -> Bool
&& Maybe KindExpr -> Int -> Kind
toKind' Maybe KindExpr
k ([Ident] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Ident]
tvs) Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
k' Bool -> Bool -> Bool
&& [ConstrDecl] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [ConstrDecl]
cs
          = IC () -> Maybe (IC ())
forall a. a -> Maybe a
Just IC ()
ok
        check _ = Maybe (IC ())
forall a. Maybe a
Nothing
checkImport (INewtypeDecl p :: Position
p tc :: QualIdent
tc k :: Maybe KindExpr
k tvs :: [Ident]
tvs nc :: NewConstrDecl
nc _) = String
-> (TypeInfo -> Maybe (IC ())) -> Position -> QualIdent -> IC ()
checkTypeInfo "newtype" TypeInfo -> Maybe (IC ())
check Position
p QualIdent
tc
  where check :: TypeInfo -> Maybe (IC ())
check (RenamingType tc' :: QualIdent
tc' k' :: Kind
k' nc' :: DataConstr
nc')
          | QualIdent
tc QualIdent -> QualIdent -> Bool
forall a. Eq a => a -> a -> Bool
== QualIdent
tc' Bool -> Bool -> Bool
&& Maybe KindExpr -> Int -> Kind
toKind' Maybe KindExpr
k ([Ident] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Ident]
tvs) Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
k' Bool -> Bool -> Bool
&&
            NewConstrDecl -> Ident
nconstrId NewConstrDecl
nc Ident -> Ident -> Bool
forall a. Eq a => a -> a -> Bool
== DataConstr -> Ident
constrIdent DataConstr
nc'
          = IC () -> Maybe (IC ())
forall a. a -> Maybe a
Just (QualIdent -> [Ident] -> NewConstrDecl -> IC ()
checkNewConstrImport QualIdent
tc [Ident]
tvs NewConstrDecl
nc)
        check _ = Maybe (IC ())
forall a. Maybe a
Nothing
checkImport (ITypeDecl p :: Position
p tc :: QualIdent
tc k :: Maybe KindExpr
k tvs :: [Ident]
tvs ty :: TypeExpr
ty) = do
  ModuleIdent
m <- IC ModuleIdent
getModuleIdent
  let check :: TypeInfo -> Maybe (IC ())
check (AliasType tc' :: QualIdent
tc' k' :: Kind
k' n' :: Int
n' ty' :: Type
ty')
        | QualIdent
tc QualIdent -> QualIdent -> Bool
forall a. Eq a => a -> a -> Bool
== QualIdent
tc' Bool -> Bool -> Bool
&& Maybe KindExpr -> Int -> Kind
toKind' Maybe KindExpr
k ([Ident] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Ident]
tvs) Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
k' Bool -> Bool -> Bool
&&
          [Ident] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Ident]
tvs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
n' Bool -> Bool -> Bool
&& ModuleIdent -> [Ident] -> TypeExpr -> Type
toQualType ModuleIdent
m [Ident]
tvs TypeExpr
ty Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
ty'
        = IC () -> Maybe (IC ())
forall a. a -> Maybe a
Just IC ()
ok
      check _ = Maybe (IC ())
forall a. Maybe a
Nothing
  String
-> (TypeInfo -> Maybe (IC ())) -> Position -> QualIdent -> IC ()
checkTypeInfo "synonym type" TypeInfo -> Maybe (IC ())
check Position
p QualIdent
tc
checkImport (IFunctionDecl p :: Position
p f :: QualIdent
f (Just tv :: Ident
tv) n :: Int
n ty :: QualTypeExpr
ty) = do
  ModuleIdent
m <- IC ModuleIdent
getModuleIdent
  let check :: ValueInfo -> Bool
check (Value f' :: QualIdent
f' cm' :: Bool
cm' n' :: Int
n' (ForAll _ ty' :: PredType
ty')) =
        QualIdent
f QualIdent -> QualIdent -> Bool
forall a. Eq a => a -> a -> Bool
== QualIdent
f' Bool -> Bool -> Bool
&& Bool
cm' Bool -> Bool -> Bool
&& Int
n' Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
n Bool -> Bool -> Bool
&& ModuleIdent -> [Ident] -> QualTypeExpr -> PredType
toQualPredType ModuleIdent
m [Ident
tv] QualTypeExpr
ty PredType -> PredType -> Bool
forall a. Eq a => a -> a -> Bool
== PredType
ty'
      check _ = Bool
False
  String -> (ValueInfo -> Bool) -> Position -> QualIdent -> IC ()
forall a.
HasPosition a =>
String -> (ValueInfo -> Bool) -> a -> QualIdent -> IC ()
checkValueInfo "method" ValueInfo -> Bool
check Position
p QualIdent
f
checkImport (IFunctionDecl p :: Position
p f :: QualIdent
f Nothing n :: Int
n ty :: QualTypeExpr
ty) = do
  ModuleIdent
m <- IC ModuleIdent
getModuleIdent
  let check :: ValueInfo -> Bool
check (Value f' :: QualIdent
f' cm' :: Bool
cm' n' :: Int
n' (ForAll _ ty' :: PredType
ty')) =
        QualIdent
f QualIdent -> QualIdent -> Bool
forall a. Eq a => a -> a -> Bool
== QualIdent
f' Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
cm' Bool -> Bool -> Bool
&& Int
n' Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
n Bool -> Bool -> Bool
&& ModuleIdent -> [Ident] -> QualTypeExpr -> PredType
toQualPredType ModuleIdent
m [] QualTypeExpr
ty PredType -> PredType -> Bool
forall a. Eq a => a -> a -> Bool
== PredType
ty'
      check _ = Bool
False
  String -> (ValueInfo -> Bool) -> Position -> QualIdent -> IC ()
forall a.
HasPosition a =>
String -> (ValueInfo -> Bool) -> a -> QualIdent -> IC ()
checkValueInfo "function" ValueInfo -> Bool
check Position
p QualIdent
f
checkImport (HidingClassDecl p :: Position
p cx :: Context
cx cls :: QualIdent
cls k :: Maybe KindExpr
k _) = do
  ClassEnv
clsEnv <- IC ClassEnv
getClassEnv
  let check :: TypeInfo -> Maybe (IC ())
check (TypeClass cls' :: QualIdent
cls' k' :: Kind
k' _)
        | QualIdent
cls QualIdent -> QualIdent -> Bool
forall a. Eq a => a -> a -> Bool
== QualIdent
cls' Bool -> Bool -> Bool
&& Maybe KindExpr -> Int -> Kind
toKind' Maybe KindExpr
k 0 Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
k' Bool -> Bool -> Bool
&&
          [QualIdent
cls'' | Constraint _ cls'' :: QualIdent
cls'' _ <- Context
cx] [QualIdent] -> [QualIdent] -> Bool
forall a. Eq a => a -> a -> Bool
== QualIdent -> ClassEnv -> [QualIdent]
superClasses QualIdent
cls' ClassEnv
clsEnv
        = IC () -> Maybe (IC ())
forall a. a -> Maybe a
Just IC ()
ok
      check _ = Maybe (IC ())
forall a. Maybe a
Nothing
  String
-> (TypeInfo -> Maybe (IC ())) -> Position -> QualIdent -> IC ()
checkTypeInfo "hidden type class" TypeInfo -> Maybe (IC ())
check Position
p QualIdent
cls
checkImport (IClassDecl p :: Position
p cx :: Context
cx cls :: QualIdent
cls k :: Maybe KindExpr
k clsvar :: Ident
clsvar ms :: [IMethodDecl]
ms _) = do
  ClassEnv
clsEnv <- IC ClassEnv
getClassEnv
  let check :: TypeInfo -> Maybe (IC ())
check (TypeClass cls' :: QualIdent
cls' k' :: Kind
k' fs :: [ClassMethod]
fs)
        | QualIdent
cls QualIdent -> QualIdent -> Bool
forall a. Eq a => a -> a -> Bool
== QualIdent
cls' Bool -> Bool -> Bool
&& Maybe KindExpr -> Int -> Kind
toKind' Maybe KindExpr
k 0 Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
k' Bool -> Bool -> Bool
&&
          [QualIdent
cls'' | Constraint _ cls'' :: QualIdent
cls'' _ <- Context
cx] [QualIdent] -> [QualIdent] -> Bool
forall a. Eq a => a -> a -> Bool
== QualIdent -> ClassEnv -> [QualIdent]
superClasses QualIdent
cls' ClassEnv
clsEnv Bool -> Bool -> Bool
&&
          (IMethodDecl -> (Ident, Maybe Int))
-> [IMethodDecl] -> [(Ident, Maybe Int)]
forall a b. (a -> b) -> [a] -> [b]
map (\m :: IMethodDecl
m -> (IMethodDecl -> Ident
imethod IMethodDecl
m, IMethodDecl -> Maybe Int
imethodArity IMethodDecl
m)) [IMethodDecl]
ms [(Ident, Maybe Int)] -> [(Ident, Maybe Int)] -> Bool
forall a. Eq a => a -> a -> Bool
==
            (ClassMethod -> (Ident, Maybe Int))
-> [ClassMethod] -> [(Ident, Maybe Int)]
forall a b. (a -> b) -> [a] -> [b]
map (\f :: ClassMethod
f -> (ClassMethod -> Ident
methodName ClassMethod
f, ClassMethod -> Maybe Int
methodArity ClassMethod
f)) [ClassMethod]
fs
        = IC () -> Maybe (IC ())
forall a. a -> Maybe a
Just (IC () -> Maybe (IC ())) -> IC () -> Maybe (IC ())
forall a b. (a -> b) -> a -> b
$ (IMethodDecl -> IC ()) -> [IMethodDecl] -> IC ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (QualIdent -> Ident -> IMethodDecl -> IC ()
checkMethodImport QualIdent
cls Ident
clsvar) [IMethodDecl]
ms
      check _ = Maybe (IC ())
forall a. Maybe a
Nothing
  String
-> (TypeInfo -> Maybe (IC ())) -> Position -> QualIdent -> IC ()
checkTypeInfo "type class" TypeInfo -> Maybe (IC ())
check Position
p QualIdent
cls
checkImport (IInstanceDecl p :: Position
p cx :: Context
cx cls :: QualIdent
cls ty :: TypeExpr
ty is :: [IMethodImpl]
is m :: Maybe ModuleIdent
m) =
  (PredSet -> [IMethodImpl] -> Bool)
-> Position -> InstIdent -> Maybe ModuleIdent -> IC ()
checkInstInfo PredSet -> [IMethodImpl] -> Bool
check Position
p (QualIdent
cls, TypeExpr -> QualIdent
typeConstr TypeExpr
ty) Maybe ModuleIdent
m
  where PredType ps :: PredSet
ps _ = [Ident] -> QualTypeExpr -> PredType
toPredType [] (QualTypeExpr -> PredType) -> QualTypeExpr -> PredType
forall a b. (a -> b) -> a -> b
$ SpanInfo -> Context -> TypeExpr -> QualTypeExpr
QualTypeExpr SpanInfo
NoSpanInfo Context
cx TypeExpr
ty
        check :: PredSet -> [IMethodImpl] -> Bool
check ps' :: PredSet
ps' is' :: [IMethodImpl]
is' = PredSet
ps PredSet -> PredSet -> Bool
forall a. Eq a => a -> a -> Bool
== PredSet
ps' Bool -> Bool -> Bool
&& [IMethodImpl] -> [IMethodImpl]
forall a. Ord a => [a] -> [a]
sort [IMethodImpl]
is [IMethodImpl] -> [IMethodImpl] -> Bool
forall a. Eq a => a -> a -> Bool
== [IMethodImpl] -> [IMethodImpl]
forall a. Ord a => [a] -> [a]
sort [IMethodImpl]
is'

checkConstrImport :: QualIdent -> [Ident] -> ConstrDecl -> IC ()
checkConstrImport :: QualIdent -> [Ident] -> ConstrDecl -> IC ()
checkConstrImport tc :: QualIdent
tc tvs :: [Ident]
tvs (ConstrDecl p :: SpanInfo
p c :: Ident
c tys :: [TypeExpr]
tys) = do
  ModuleIdent
m <- IC ModuleIdent
getModuleIdent
  let qc :: QualIdent
qc = QualIdent -> Ident -> QualIdent
qualifyLike QualIdent
tc Ident
c
      check :: ValueInfo -> Bool
check (DataConstructor c' :: QualIdent
c' _ _ (ForAll uqvs :: Int
uqvs pty :: PredType
pty)) =
        QualIdent
qc QualIdent -> QualIdent -> Bool
forall a. Eq a => a -> a -> Bool
== QualIdent
c' Bool -> Bool -> Bool
&& [Ident] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Ident]
tvs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
uqvs Bool -> Bool -> Bool
&&
        ModuleIdent -> PredType -> PredType
qualifyPredType ModuleIdent
m (QualIdent -> [Ident] -> [TypeExpr] -> PredType
toConstrType QualIdent
tc [Ident]
tvs [TypeExpr]
tys) PredType -> PredType -> Bool
forall a. Eq a => a -> a -> Bool
== PredType
pty
      check _ = Bool
False
  String -> (ValueInfo -> Bool) -> SpanInfo -> QualIdent -> IC ()
forall a.
HasPosition a =>
String -> (ValueInfo -> Bool) -> a -> QualIdent -> IC ()
checkValueInfo "data constructor" ValueInfo -> Bool
check SpanInfo
p QualIdent
qc
checkConstrImport tc :: QualIdent
tc tvs :: [Ident]
tvs (ConOpDecl p :: SpanInfo
p ty1 :: TypeExpr
ty1 op :: Ident
op ty2 :: TypeExpr
ty2) = do
  ModuleIdent
m <- IC ModuleIdent
getModuleIdent
  let qc :: QualIdent
qc = QualIdent -> Ident -> QualIdent
qualifyLike QualIdent
tc Ident
op
      check :: ValueInfo -> Bool
check (DataConstructor c' :: QualIdent
c' _ _ (ForAll uqvs :: Int
uqvs pty :: PredType
pty)) =
        QualIdent
qc QualIdent -> QualIdent -> Bool
forall a. Eq a => a -> a -> Bool
== QualIdent
c' Bool -> Bool -> Bool
&& [Ident] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Ident]
tvs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
uqvs Bool -> Bool -> Bool
&&
        ModuleIdent -> PredType -> PredType
qualifyPredType ModuleIdent
m (QualIdent -> [Ident] -> [TypeExpr] -> PredType
toConstrType QualIdent
tc [Ident]
tvs [TypeExpr
ty1, TypeExpr
ty2]) PredType -> PredType -> Bool
forall a. Eq a => a -> a -> Bool
== PredType
pty
      check _ = Bool
False
  String -> (ValueInfo -> Bool) -> SpanInfo -> QualIdent -> IC ()
forall a.
HasPosition a =>
String -> (ValueInfo -> Bool) -> a -> QualIdent -> IC ()
checkValueInfo "data constructor" ValueInfo -> Bool
check SpanInfo
p QualIdent
qc
checkConstrImport tc :: QualIdent
tc tvs :: [Ident]
tvs (RecordDecl p :: SpanInfo
p c :: Ident
c fs :: [FieldDecl]
fs) = do
  ModuleIdent
m <- IC ModuleIdent
getModuleIdent
  let qc :: QualIdent
qc = QualIdent -> Ident -> QualIdent
qualifyLike QualIdent
tc Ident
c
      (ls :: [Ident]
ls, tys :: [TypeExpr]
tys) = [(Ident, TypeExpr)] -> ([Ident], [TypeExpr])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Ident
l, TypeExpr
ty) | FieldDecl _ labels :: [Ident]
labels ty :: TypeExpr
ty <- [FieldDecl]
fs, Ident
l <- [Ident]
labels]
      check :: ValueInfo -> Bool
check (DataConstructor c' :: QualIdent
c' _ ls' :: [Ident]
ls' (ForAll uqvs :: Int
uqvs pty :: PredType
pty)) =
        QualIdent
qc QualIdent -> QualIdent -> Bool
forall a. Eq a => a -> a -> Bool
== QualIdent
c' Bool -> Bool -> Bool
&& [Ident] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Ident]
tvs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
uqvs Bool -> Bool -> Bool
&& [Ident]
ls [Ident] -> [Ident] -> Bool
forall a. Eq a => a -> a -> Bool
== [Ident]
ls' Bool -> Bool -> Bool
&&
        ModuleIdent -> PredType -> PredType
qualifyPredType ModuleIdent
m (QualIdent -> [Ident] -> [TypeExpr] -> PredType
toConstrType QualIdent
tc [Ident]
tvs [TypeExpr]
tys) PredType -> PredType -> Bool
forall a. Eq a => a -> a -> Bool
== PredType
pty
      check _ = Bool
False
  String -> (ValueInfo -> Bool) -> SpanInfo -> QualIdent -> IC ()
forall a.
HasPosition a =>
String -> (ValueInfo -> Bool) -> a -> QualIdent -> IC ()
checkValueInfo "data constructor" ValueInfo -> Bool
check SpanInfo
p QualIdent
qc

checkNewConstrImport :: QualIdent -> [Ident] -> NewConstrDecl -> IC ()
checkNewConstrImport :: QualIdent -> [Ident] -> NewConstrDecl -> IC ()
checkNewConstrImport tc :: QualIdent
tc tvs :: [Ident]
tvs (NewConstrDecl p :: SpanInfo
p c :: Ident
c ty :: TypeExpr
ty) = do
  ModuleIdent
m <- IC ModuleIdent
getModuleIdent
  let qc :: QualIdent
qc = QualIdent -> Ident -> QualIdent
qualifyLike QualIdent
tc Ident
c
      check :: ValueInfo -> Bool
check (NewtypeConstructor c' :: QualIdent
c' _ (ForAll uqvs :: Int
uqvs (PredType _ ty' :: Type
ty'))) =
        QualIdent
qc QualIdent -> QualIdent -> Bool
forall a. Eq a => a -> a -> Bool
== QualIdent
c' Bool -> Bool -> Bool
&& [Ident] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Ident]
tvs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
uqvs Bool -> Bool -> Bool
&&ModuleIdent -> [Ident] -> TypeExpr -> Type
toQualType ModuleIdent
m [Ident]
tvs TypeExpr
ty Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== [Type] -> Type
forall a. [a] -> a
head (Type -> [Type]
arrowArgs Type
ty')
      check _ = Bool
False
  String -> (ValueInfo -> Bool) -> SpanInfo -> QualIdent -> IC ()
forall a.
HasPosition a =>
String -> (ValueInfo -> Bool) -> a -> QualIdent -> IC ()
checkValueInfo "newtype constructor" ValueInfo -> Bool
check SpanInfo
p QualIdent
qc
checkNewConstrImport tc :: QualIdent
tc tvs :: [Ident]
tvs (NewRecordDecl p :: SpanInfo
p c :: Ident
c (l :: Ident
l, ty :: TypeExpr
ty)) = do
  ModuleIdent
m <- IC ModuleIdent
getModuleIdent
  let qc :: QualIdent
qc = QualIdent -> Ident -> QualIdent
qualifyLike QualIdent
tc Ident
c
      check :: ValueInfo -> Bool
check (NewtypeConstructor c' :: QualIdent
c' l' :: Ident
l' (ForAll uqvs :: Int
uqvs (PredType _ ty' :: Type
ty'))) =
        QualIdent
qc QualIdent -> QualIdent -> Bool
forall a. Eq a => a -> a -> Bool
== QualIdent
c' Bool -> Bool -> Bool
&& [Ident] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Ident]
tvs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
uqvs Bool -> Bool -> Bool
&& Ident
l Ident -> Ident -> Bool
forall a. Eq a => a -> a -> Bool
== Ident
l' Bool -> Bool -> Bool
&&
        ModuleIdent -> [Ident] -> TypeExpr -> Type
toQualType ModuleIdent
m [Ident]
tvs TypeExpr
ty Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== [Type] -> Type
forall a. [a] -> a
head (Type -> [Type]
arrowArgs Type
ty')
      check _ = Bool
False
  String -> (ValueInfo -> Bool) -> SpanInfo -> QualIdent -> IC ()
forall a.
HasPosition a =>
String -> (ValueInfo -> Bool) -> a -> QualIdent -> IC ()
checkValueInfo "newtype constructor" ValueInfo -> Bool
check SpanInfo
p QualIdent
qc

checkMethodImport :: QualIdent -> Ident -> IMethodDecl -> IC ()
checkMethodImport :: QualIdent -> Ident -> IMethodDecl -> IC ()
checkMethodImport qcls :: QualIdent
qcls clsvar :: Ident
clsvar (IMethodDecl p :: Position
p f :: Ident
f _ qty :: QualTypeExpr
qty) =
  String -> (ValueInfo -> Bool) -> Position -> QualIdent -> IC ()
forall a.
HasPosition a =>
String -> (ValueInfo -> Bool) -> a -> QualIdent -> IC ()
checkValueInfo "method" ValueInfo -> Bool
check Position
p QualIdent
qf
  where qf :: QualIdent
qf = QualIdent -> Ident -> QualIdent
qualifyLike QualIdent
qcls Ident
f
        check :: ValueInfo -> Bool
check (Value f' :: QualIdent
f' cm' :: Bool
cm' _ (ForAll _ pty :: PredType
pty)) =
          QualIdent
qf QualIdent -> QualIdent -> Bool
forall a. Eq a => a -> a -> Bool
== QualIdent
f' Bool -> Bool -> Bool
&& Bool
cm' Bool -> Bool -> Bool
&& QualIdent -> Ident -> QualTypeExpr -> PredType
toMethodType QualIdent
qcls Ident
clsvar QualTypeExpr
qty PredType -> PredType -> Bool
forall a. Eq a => a -> a -> Bool
== PredType
pty
        check _ = Bool
False

checkPrecInfo :: (PrecInfo -> Bool) -> Position -> QualIdent -> IC ()
checkPrecInfo :: (PrecInfo -> Bool) -> Position -> QualIdent -> IC ()
checkPrecInfo check :: PrecInfo -> Bool
check p :: Position
p op :: QualIdent
op = do
  OpPrecEnv
pEnv <- IC OpPrecEnv
getPrecEnv
  let checkInfo :: ModuleIdent -> Ident -> IC ()
checkInfo m :: ModuleIdent
m op' :: Ident
op' = case QualIdent -> OpPrecEnv -> [PrecInfo]
forall a. QualIdent -> TopEnv a -> [a]
qualLookupTopEnv QualIdent
op OpPrecEnv
pEnv of
        []     -> Message -> IC ()
report (Message -> IC ()) -> Message -> IC ()
forall a b. (a -> b) -> a -> b
$ Position -> ModuleIdent -> Ident -> Message
errNoPrecedence Position
p ModuleIdent
m Ident
op'
        [prec :: PrecInfo
prec] -> Bool -> IC () -> IC ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (PrecInfo -> Bool
check PrecInfo
prec)
                         (Message -> IC ()
report (Message -> IC ()) -> Message -> IC ()
forall a b. (a -> b) -> a -> b
$ Position -> String -> ModuleIdent -> Ident -> Message
errImportConflict Position
p "precedence" ModuleIdent
m Ident
op')
        _      -> String -> IC ()
forall a. String -> a
internalError "checkPrecInfo"
  (ModuleIdent -> Ident -> IC ()) -> QualIdent -> IC ()
checkImported ModuleIdent -> Ident -> IC ()
checkInfo QualIdent
op

checkTypeInfo :: String -> (TypeInfo -> Maybe (IC ())) -> Position
              -> QualIdent -> IC ()
checkTypeInfo :: String
-> (TypeInfo -> Maybe (IC ())) -> Position -> QualIdent -> IC ()
checkTypeInfo what :: String
what check :: TypeInfo -> Maybe (IC ())
check p :: Position
p tc :: QualIdent
tc = do
  TCEnv
tcEnv <- IC TCEnv
getTyConsEnv
  let checkInfo :: ModuleIdent -> Ident -> IC ()
checkInfo m :: ModuleIdent
m tc' :: Ident
tc' = case QualIdent -> TCEnv -> [TypeInfo]
forall a. QualIdent -> TopEnv a -> [a]
qualLookupTopEnv QualIdent
tc TCEnv
tcEnv of
        []   -> Message -> IC ()
report (Message -> IC ()) -> Message -> IC ()
forall a b. (a -> b) -> a -> b
$ Position -> String -> ModuleIdent -> Ident -> Message
errNotExported Position
p String
what ModuleIdent
m Ident
tc'
        [ti :: TypeInfo
ti] -> IC () -> Maybe (IC ()) -> IC ()
forall a. a -> Maybe a -> a
fromMaybe (Message -> IC ()
report (Message -> IC ()) -> Message -> IC ()
forall a b. (a -> b) -> a -> b
$ Position -> String -> ModuleIdent -> Ident -> Message
errImportConflict Position
p String
what ModuleIdent
m Ident
tc') (TypeInfo -> Maybe (IC ())
check TypeInfo
ti)
        _    -> String -> IC ()
forall a. String -> a
internalError "checkTypeInfo"
  (ModuleIdent -> Ident -> IC ()) -> QualIdent -> IC ()
checkImported ModuleIdent -> Ident -> IC ()
checkInfo QualIdent
tc

checkInstInfo :: (PredSet -> [(Ident, Int)] -> Bool) -> Position -> InstIdent
              -> Maybe ModuleIdent -> IC ()
checkInstInfo :: (PredSet -> [IMethodImpl] -> Bool)
-> Position -> InstIdent -> Maybe ModuleIdent -> IC ()
checkInstInfo check :: PredSet -> [IMethodImpl] -> Bool
check p :: Position
p i :: InstIdent
i mm :: Maybe ModuleIdent
mm = do
  InstEnv
inEnv <- IC InstEnv
getInstEnv
  let checkInfo :: ModuleIdent -> p -> IC ()
checkInfo m :: ModuleIdent
m _ = case InstIdent -> InstEnv -> Maybe InstInfo
lookupInstInfo InstIdent
i InstEnv
inEnv of
        Just (m' :: ModuleIdent
m', ps :: PredSet
ps, is :: [IMethodImpl]
is)
          | ModuleIdent
m ModuleIdent -> ModuleIdent -> Bool
forall a. Eq a => a -> a -> Bool
/= ModuleIdent
m'   -> Message -> IC ()
report (Message -> IC ()) -> Message -> IC ()
forall a b. (a -> b) -> a -> b
$ Position -> ModuleIdent -> InstIdent -> Message
errNoInstance Position
p ModuleIdent
m InstIdent
i
          | Bool
otherwise ->
            Bool -> IC () -> IC ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (PredSet -> [IMethodImpl] -> Bool
check PredSet
ps [IMethodImpl]
is) (IC () -> IC ()) -> IC () -> IC ()
forall a b. (a -> b) -> a -> b
$ Message -> IC ()
report (Message -> IC ()) -> Message -> IC ()
forall a b. (a -> b) -> a -> b
$ Position -> ModuleIdent -> InstIdent -> Message
errInstanceConflict Position
p ModuleIdent
m InstIdent
i
        Nothing -> Message -> IC ()
report (Message -> IC ()) -> Message -> IC ()
forall a b. (a -> b) -> a -> b
$ Position -> ModuleIdent -> InstIdent -> Message
errNoInstance Position
p ModuleIdent
m InstIdent
i
  (ModuleIdent -> Ident -> IC ()) -> QualIdent -> IC ()
checkImported ModuleIdent -> Ident -> IC ()
forall p. ModuleIdent -> p -> IC ()
checkInfo ((Ident -> QualIdent)
-> (ModuleIdent -> Ident -> QualIdent)
-> Maybe ModuleIdent
-> Ident
-> QualIdent
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Ident -> QualIdent
qualify ModuleIdent -> Ident -> QualIdent
qualifyWith Maybe ModuleIdent
mm Ident
anonId)

checkValueInfo :: HasPosition a => String -> (ValueInfo -> Bool) -> a
               -> QualIdent -> IC ()
checkValueInfo :: String -> (ValueInfo -> Bool) -> a -> QualIdent -> IC ()
checkValueInfo what :: String
what check :: ValueInfo -> Bool
check p :: a
p x :: QualIdent
x = do
  ValueEnv
tyEnv <- IC ValueEnv
getValueEnv
  let checkInfo :: ModuleIdent -> Ident -> IC ()
checkInfo m :: ModuleIdent
m x' :: Ident
x' = case QualIdent -> ValueEnv -> [ValueInfo]
forall a. QualIdent -> TopEnv a -> [a]
qualLookupTopEnv QualIdent
x ValueEnv
tyEnv of
        []   -> Message -> IC ()
report (Message -> IC ()) -> Message -> IC ()
forall a b. (a -> b) -> a -> b
$ Position -> String -> ModuleIdent -> Ident -> Message
errNotExported Position
p' String
what ModuleIdent
m Ident
x'
        [vi :: ValueInfo
vi] -> Bool -> IC () -> IC ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (ValueInfo -> Bool
check ValueInfo
vi)
                  (Message -> IC ()
report (Message -> IC ()) -> Message -> IC ()
forall a b. (a -> b) -> a -> b
$ Position -> String -> ModuleIdent -> Ident -> Message
errImportConflict Position
p' String
what ModuleIdent
m Ident
x')
        _    -> String -> IC ()
forall a. String -> a
internalError "checkValueInfo"
  (ModuleIdent -> Ident -> IC ()) -> QualIdent -> IC ()
checkImported ModuleIdent -> Ident -> IC ()
checkInfo QualIdent
x
  where p' :: Position
p' = a -> Position
forall a. HasPosition a => a -> Position
getPosition a
p

checkImported :: (ModuleIdent -> Ident -> IC ()) -> QualIdent -> IC ()
checkImported :: (ModuleIdent -> Ident -> IC ()) -> QualIdent -> IC ()
checkImported _ (QualIdent _ Nothing  _) = IC ()
ok
checkImported f :: ModuleIdent -> Ident -> IC ()
f (QualIdent _ (Just m :: ModuleIdent
m) x :: Ident
x) = ModuleIdent -> Ident -> IC ()
f ModuleIdent
m Ident
x

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

errNotExported :: Position -> String -> ModuleIdent -> Ident -> Message
errNotExported :: Position -> String -> ModuleIdent -> Ident -> Message
errNotExported p :: Position
p what :: String
what m :: ModuleIdent
m x :: Ident
x = Position -> Doc -> Message
forall p. HasPosition p => p -> Doc -> Message
posMessage Position
p (Doc -> Message) -> Doc -> Message
forall a b. (a -> b) -> a -> b
$
  String -> Doc
text "Inconsistent module interfaces"
  Doc -> Doc -> Doc
$+$ String -> Doc
text "Module" Doc -> Doc -> Doc
<+> String -> Doc
text (ModuleIdent -> String
moduleName ModuleIdent
m)
  Doc -> Doc -> Doc
<+> String -> Doc
text "does not export"Doc -> Doc -> Doc
<+> String -> Doc
text String
what Doc -> Doc -> Doc
<+> String -> Doc
text (Ident -> String
escName Ident
x)

errNoPrecedence :: Position -> ModuleIdent -> Ident -> Message
errNoPrecedence :: Position -> ModuleIdent -> Ident -> Message
errNoPrecedence p :: Position
p m :: ModuleIdent
m x :: Ident
x = Position -> Doc -> Message
forall p. HasPosition p => p -> Doc -> Message
posMessage Position
p (Doc -> Message) -> Doc -> Message
forall a b. (a -> b) -> a -> b
$
  String -> Doc
text "Inconsistent module interfaces"
  Doc -> Doc -> Doc
$+$ String -> Doc
text "Module" Doc -> Doc -> Doc
<+> String -> Doc
text (ModuleIdent -> String
moduleName ModuleIdent
m)
  Doc -> Doc -> Doc
<+> String -> Doc
text "does not define a precedence for" Doc -> Doc -> Doc
<+> String -> Doc
text (Ident -> String
escName Ident
x)

errNoInstance :: Position -> ModuleIdent -> InstIdent -> Message
errNoInstance :: Position -> ModuleIdent -> InstIdent -> Message
errNoInstance p :: Position
p m :: ModuleIdent
m i :: InstIdent
i = Position -> Doc -> Message
forall p. HasPosition p => p -> Doc -> Message
posMessage Position
p (Doc -> Message) -> Doc -> Message
forall a b. (a -> b) -> a -> b
$
  String -> Doc
text "Inconsistent module interfaces"
  Doc -> Doc -> Doc
$+$ String -> Doc
text "Module" Doc -> Doc -> Doc
<+> String -> Doc
text (ModuleIdent -> String
moduleName ModuleIdent
m)
  Doc -> Doc -> Doc
<+> String -> Doc
text "does not define an instance for" Doc -> Doc -> Doc
<+> InstIdent -> Doc
ppInstIdent InstIdent
i

errImportConflict :: Position -> String -> ModuleIdent -> Ident -> Message
errImportConflict :: Position -> String -> ModuleIdent -> Ident -> Message
errImportConflict p :: Position
p what :: String
what m :: ModuleIdent
m x :: Ident
x = Position -> Doc -> Message
forall p. HasPosition p => p -> Doc -> Message
posMessage Position
p (Doc -> Message) -> Doc -> Message
forall a b. (a -> b) -> a -> b
$
  String -> Doc
text "Inconsistent module interfaces"
  Doc -> Doc -> Doc
$+$ String -> Doc
text "Declaration of" Doc -> Doc -> Doc
<+> String -> Doc
text String
what Doc -> Doc -> Doc
<+> String -> Doc
text (Ident -> String
escName Ident
x)
  Doc -> Doc -> Doc
<+> String -> Doc
text "does not match its definition in module" Doc -> Doc -> Doc
<+> String -> Doc
text (ModuleIdent -> String
moduleName ModuleIdent
m)

errInstanceConflict :: Position -> ModuleIdent -> InstIdent -> Message
errInstanceConflict :: Position -> ModuleIdent -> InstIdent -> Message
errInstanceConflict p :: Position
p m :: ModuleIdent
m i :: InstIdent
i = Position -> Doc -> Message
forall p. HasPosition p => p -> Doc -> Message
posMessage Position
p (Doc -> Message) -> Doc -> Message
forall a b. (a -> b) -> a -> b
$
  String -> Doc
text "Inconsistent module interfaces"
  Doc -> Doc -> Doc
$+$ String -> Doc
text "Declaration of instance" Doc -> Doc -> Doc
<+> InstIdent -> Doc
ppInstIdent InstIdent
i
  Doc -> Doc -> Doc
<+> String -> Doc
text "does not match its definition in module" Doc -> Doc -> Doc
<+> String -> Doc
text (ModuleIdent -> String
moduleName ModuleIdent
m)