{-# LANGUAGE PatternGuards #-}
module GF.Compile.TypeCheck.Concrete( checkLType, inferLType, computeLType, ppType ) where
import Prelude hiding ((<>)) -- GHC 8.4.1 clash with Text.PrettyPrint

import GF.Infra.CheckM
import GF.Data.Operations

import GF.Grammar
import GF.Grammar.Lookup
import GF.Grammar.Predef
import GF.Grammar.PatternMatch
import GF.Grammar.Lockfield (isLockLabel, lockRecType, unlockRecord)
import GF.Compile.TypeCheck.Primitives

import Data.List
import Control.Monad
import GF.Text.Pretty

computeLType :: SourceGrammar -> Context -> Type -> Check Type
computeLType gr g0 t = comp (reverse [(b,x, Vr x) | (b,x,_) <- g0] ++ g0) t
 where
  comp g ty = case ty of
    _ | Just _ <- isTypeInts ty -> return ty ---- shouldn't be needed
      | isPredefConstant ty     -> return ty ---- shouldn't be needed

    Q (m,ident) -> checkIn ("module" <+> m) $ do
      ty' <- lookupResDef gr (m,ident)
      if ty' == ty then return ty else comp g ty' --- is this necessary to test?

    AdHocOverload ts -> do
     over <- getOverload gr g (Just typeType) t
     case over of
       Just (tr,_) -> return tr
       _ -> checkError ("unresolved overloading of constants" <+> ppTerm Qualified 0 t)

    Vr ident  -> checkLookup ident g -- never needed to compute!

    App f a -> do
      f' <- comp g f
      a' <- comp g a
      case f' of
        Abs b x t -> comp ((b,x,a'):g) t
        _ -> return $ App f' a'

    Prod bt x a b -> do
      a' <- comp g a
      b' <- comp ((bt,x,Vr x) : g) b
      return $ Prod bt x a' b'

    Abs bt x b -> do
      b' <- comp ((bt,x,Vr x):g) b
      return $ Abs bt x b'

    Let (x,(_,a)) b -> comp ((Explicit,x,a):g) b

    ExtR r s -> do
      r' <- comp g r
      s' <- comp g s
      case (r',s') of
        (RecType rs, RecType ss) -> plusRecType r' s' >>= comp g
        _ -> return $ ExtR r' s'

    RecType fs -> do
      let fs' = sortRec fs
      liftM RecType $ mapPairsM (comp g) fs'

    ELincat c t -> do
      t' <- comp g t
      lockRecType c t' ---- locking to be removed AR 20/6/2009

    _ | ty == typeTok -> return typeStr

    _ -> composOp (comp g) ty

-- the underlying algorithms

inferLType :: SourceGrammar -> Context -> Term -> Check (Term, Type)
inferLType gr g trm = case trm of

   Q (m,ident) | isPredef m -> termWith trm $ case typPredefined ident of
                                                Just ty -> return ty
                                                Nothing -> checkError ("unknown in Predef:" <+> ident)

   Q ident -> checks [
     termWith trm $ lookupResType gr ident >>= computeLType gr g
     ,
     lookupResDef gr ident >>= inferLType gr g
     ,
     checkError ("cannot infer type of constant" <+> ppTerm Unqualified 0 trm)
     ]

   QC (m,ident) | isPredef m -> termWith trm $ case typPredefined ident of
                                                 Just ty -> return ty
                                                 Nothing -> checkError ("unknown in Predef:" <+> ident)

   QC ident -> checks [
       termWith trm $ lookupResType gr ident >>= computeLType gr g
       ,
       lookupResDef gr ident >>= inferLType gr g
       ,
       checkError ("cannot infer type of canonical constant" <+> ppTerm Unqualified 0 trm)
       ]

   Vr ident -> termWith trm $ checkLookup ident g

   Typed e t -> do
     t' <- computeLType gr g t
     checkLType gr g e t'

   AdHocOverload ts -> do
     over <- getOverload gr g Nothing trm
     case over of
       Just trty -> return trty
       _ -> checkError ("unresolved overloading of constants" <+> ppTerm Qualified 0 trm)

   App f a -> do
     over <- getOverload gr g Nothing trm
     case over of
       Just trty -> return trty
       _ -> do
         (f',fty) <- inferLType gr g f
         fty' <- computeLType gr g fty
         case fty' of
           Prod bt z arg val -> do
             a' <- justCheck g a arg
             ty <- if isWildIdent z
                      then return val
                      else substituteLType [(bt,z,a')] val
             return (App f' a',ty)
           _ ->
             let term = ppTerm Unqualified 0 f
                 funName = pp . head . words .render $ term
              in checkError ("A function type is expected for" <+> term <+> "instead of type" <+> ppType fty $$
                             "\n   ** Maybe you gave too many arguments to" <+> funName <+> "\n")

   S f x -> do
     (f', fty) <- inferLType gr g f
     case fty of
       Table arg val -> do
         x'<- justCheck g x arg
         return (S f' x', val)
       _ -> checkError ("table lintype expected for the table in" $$ nest 2 (ppTerm Unqualified 0 trm))

   P t i -> do
     (t',ty) <- inferLType gr g t   --- ??
     ty' <- computeLType gr g ty
     let tr2 = P t' i
     termWith tr2 $ case ty' of
       RecType ts -> case lookup i ts of
                       Nothing -> checkError ("unknown label" <+> i <+> "in" $$ nest 2 (ppTerm Unqualified 0 ty'))
                       Just x  -> return x
       _          -> checkError ("record type expected for:" <+> ppTerm Unqualified 0 t $$
                                 " instead of the inferred:" <+> ppTerm Unqualified 0 ty')

   R r -> do
     let (ls,fs) = unzip r
     fsts <- mapM inferM fs
     let ts = [ty | (Just ty,_) <- fsts]
     checkCond ("cannot infer type of record" $$ nest 2 (ppTerm Unqualified 0 trm)) (length ts == length fsts)
     return $ (R (zip ls fsts), RecType (zip ls ts))

   T (TTyped arg) pts -> do
     (_,val) <- checks $ map (inferCase (Just arg)) pts
     checkLType gr g trm (Table arg val)
   T (TComp arg) pts -> do
     (_,val) <- checks $ map (inferCase (Just arg)) pts
     checkLType gr g trm (Table arg val)
   T ti pts -> do  -- tries to guess: good in oper type inference
     let pts' = [pt | pt@(p,_) <- pts, isConstPatt p]
     case pts' of
       [] -> checkError ("cannot infer table type of" <+> ppTerm Unqualified 0 trm)
----       PInt k : _ -> return $ Ints $ max [i | PInt i <- pts']
       _  -> do
         (arg,val) <- checks $ map (inferCase Nothing) pts'
         checkLType gr g trm (Table arg val)
   V arg pts -> do
     (_,val) <- checks $ map (inferLType gr g) pts
--   return (trm, Table arg val) -- old, caused issue 68
     checkLType gr g trm (Table arg val)

   K s  -> do
     if elem ' ' s
        then do
          let ss = foldr C Empty (map K (words s))
          ----- removed irritating warning AR 24/5/2008
          ----- checkWarn ("token \"" ++ s ++
          -----              "\" converted to token list" ++ prt ss)
          return (ss, typeStr)
        else return (trm, typeStr)

   EInt i -> return (trm, typeInt)

   EFloat i -> return (trm, typeFloat)

   Empty -> return (trm, typeStr)

   C s1 s2 ->
     check2 (flip (justCheck g) typeStr) C s1 s2 typeStr

   Glue s1 s2 ->
     check2 (flip (justCheck g) typeStr) Glue s1 s2 typeStr ---- typeTok

---- hack from Rename.identRenameTerm, to live with files with naming conflicts 18/6/2007
   Strs (Cn c : ts) | c == cConflict -> do
     checkWarn ("unresolved constant, could be any of" <+> hcat (map (ppTerm Unqualified 0) ts))
     inferLType gr g (head ts)

   Strs ts -> do
     ts' <- mapM (\t -> justCheck g t typeStr) ts
     return (Strs ts', typeStrs)

   Alts t aa -> do
     t'  <- justCheck g t typeStr
     aa' <- flip mapM aa (\ (c,v) -> do
        c' <- justCheck g c typeStr
        v' <- checks $ map (justCheck g v) [typeStrs, EPattType typeStr]
        return (c',v'))
     return (Alts t' aa', typeStr)

   RecType r -> do
     let (ls,ts) = unzip r
     ts' <- mapM (flip (justCheck g) typeType) ts
     return (RecType (zip ls ts'), typeType)

   ExtR r s -> do

---     over <- getOverload gr g Nothing r
---     let r1 = maybe r fst over
     let r1 = r ---

     (r',rT) <- inferLType gr g r1
     rT'     <- computeLType gr g rT

     (s',sT) <- inferLType gr g s
     sT'     <- computeLType gr g sT

     let trm' = ExtR r' s'
     case (rT', sT') of
       (RecType rs, RecType ss) -> do
         let rt = RecType ([field | field@(l,_) <- rs, notElem l (map fst ss)] ++ ss) -- select types of later fields
         checkLType gr g trm' rt ---- return (trm', rt)
       _ | rT' == typeType && sT' == typeType -> do
         return (trm', typeType)
       _ -> checkError ("records or record types expected in" <+> ppTerm Unqualified 0 trm)

   Sort _     ->
     termWith trm $ return typeType

   Prod bt x a b -> do
     a' <- justCheck g a typeType
     b' <- justCheck ((bt,x,a'):g) b typeType
     return (Prod bt x a' b', typeType)

   Table p t  -> do
     p' <- justCheck g p typeType --- check p partype!
     t' <- justCheck g t typeType
     return $ (Table p' t', typeType)

   FV vs -> do
     (_,ty) <- checks $ map (inferLType gr g) vs
---     checkIfComplexVariantType trm ty
     checkLType gr g trm ty

   EPattType ty -> do
     ty' <- justCheck g ty typeType
     return (EPattType ty',typeType)
   EPatt p -> do
     ty <- inferPatt p
     return (trm, EPattType ty)

   ELin c trm -> do
     (trm',ty) <- inferLType gr g trm
     ty' <- lockRecType c ty ---- lookup c; remove lock AR 20/6/2009
     return $ (ELin c trm', ty')

   _ -> checkError ("cannot infer lintype of" <+> ppTerm Unqualified 0 trm)

 where
   isPredef m = elem m [cPredef,cPredefAbs]

   justCheck g ty te = checkLType gr g ty te >>= return . fst

   -- for record fields, which may be typed
   inferM (mty, t) = do
     (t', ty') <- case mty of
       Just ty -> checkLType gr g t ty
       _ -> inferLType gr g t
     return (Just ty',t')

   inferCase mty (patt,term) = do
     arg  <- maybe (inferPatt patt) return mty
     cont <- pattContext gr g arg patt
     (_,val) <- inferLType gr (reverse cont ++ g) term
     return (arg,val)
   isConstPatt p = case p of
     PC _ ps -> True --- all isConstPatt ps
     PP _ ps -> True --- all isConstPatt ps
     PR ps -> all (isConstPatt . snd) ps
     PT _ p -> isConstPatt p
     PString _ -> True
     PInt _ -> True
     PFloat _ -> True
     PChar -> True
     PChars _ -> True
     PSeq p q -> isConstPatt p && isConstPatt q
     PAlt p q -> isConstPatt p && isConstPatt q
     PRep p -> isConstPatt p
     PNeg p -> isConstPatt p
     PAs _ p -> isConstPatt p
     _ -> False

   inferPatt p = case p of
     PP (q,c) ps | q /= cPredef -> liftM valTypeCnc (lookupResType gr (q,c))
     PAs _ p  -> inferPatt p
     PNeg p   -> inferPatt p
     PAlt p q -> checks [inferPatt p, inferPatt q]
     PSeq _ _ -> return $ typeStr
     PRep _   -> return $ typeStr
     PChar    -> return $ typeStr
     PChars _ -> return $ typeStr
     _ -> inferLType gr g (patt2term p) >>= return . snd

-- type inference: Nothing, type checking: Just t
-- the latter permits matching with value type
getOverload :: SourceGrammar -> Context -> Maybe Type -> Term -> Check (Maybe (Term,Type))
getOverload gr g mt ot = case appForm ot of
     (f@(Q c), ts) -> case lookupOverload gr c of
       Ok typs -> do
         ttys <- mapM (inferLType gr g) ts
         v <- matchOverload f typs ttys
         return $ Just v
       _ -> return Nothing
     (AdHocOverload cs@(f:_), ts) -> do     --- the function name f is only used in error messages
       let typs = concatMap collectOverloads cs
       ttys <- mapM (inferLType gr g) ts
       v <- matchOverload f typs ttys
       return $ Just v
     _ -> return Nothing

 where
   collectOverloads tr@(Q c) = case lookupOverload gr c of
     Ok typs -> typs
     _ -> case lookupResType gr c of
       Ok ty -> let (args,val) = typeFormCnc ty in [(map (\(b,x,t) -> t) args,(val,tr))]
       _ -> []
   collectOverloads _ = [] --- constructors QC

   matchOverload f typs ttys = do
     let (tts,tys) = unzip ttys
     let vfs = lookupOverloadInstance tys typs
     let matches = [vf | vf@((_,v,_),_) <- vfs, matchVal mt v]
     let showTypes ty = hsep (map ppType ty)


     let (stys,styps) = (showTypes tys, [showTypes ty | (ty,_) <- typs])

     -- to avoid strange error msg e.g. in case of unmatch record extension, show whole types if needed AR 28/1/2013
     let (stysError,stypsError) = if elem (render stys) (map render styps)
            then (hsep (map (ppTerm Unqualified 0) tys), [hsep (map (ppTerm Unqualified 0) ty) | (ty,_) <- typs])
            else (stys,styps)

     case ([vf | (vf,True) <- matches],[vf | (vf,False) <- matches]) of
       ([(_,val,fun)],_) -> return (mkApp fun tts, val)
       ([],[(pre,val,fun)]) -> do
         checkWarn $  "ignoring lock fields in resolving" <+> ppTerm Unqualified 0 ot $$
                      "for" $$
                      nest 2 (showTypes tys) $$
                      "using" $$
                      nest 2 (showTypes pre)
         return (mkApp fun tts, val)
       ([],[]) -> do
         checkError $ "no overload instance of" <+> ppTerm Qualified 0 f $$
                      maybe empty (\x -> "with value type" <+> ppType x) mt $$
                      "for argument list" $$
                      nest 2 stysError $$
                      "among alternatives" $$
                      nest 2 (vcat stypsError)


       (vfs1,vfs2) -> case (noProds vfs1,noProds vfs2) of
         ([(val,fun)],_) -> do
           return (mkApp fun tts, val)
         ([],[(val,fun)]) -> do
           checkWarn ("ignoring lock fields in resolving" <+> ppTerm Unqualified 0 ot)
           return (mkApp fun tts, val)

----- unsafely exclude irritating warning AR 24/5/2008
-----           checkWarn $ "overloading of" +++ prt f +++
-----             "resolved by excluding partial applications:" ++++
-----             unlines [prtType env ty | (ty,_) <- vfs', not (noProd ty)]

--- now forgiving ambiguity with a warning AR 1/2/2014
--  This gives ad hoc overloading the same behaviour as the choice of the first match in renaming did before.
--  But it also gives a chance to ambiguous overloadings that were banned before.
         (nps1,nps2) -> do
              checkWarn $  "ambiguous overloading of" <+> ppTerm Unqualified 0 f <+>
                  ----     "with argument types" <+> hsep (map (ppTerm Qualified 0) tys) $$
                           "resolved by selecting the first of the alternatives" $$
                           nest 2 (vcat [ppTerm Qualified 0 fun | (_,ty,fun) <- vfs1 ++ if null vfs1 then vfs2 else []])
              case [(mkApp fun tts,val) | (val,fun) <- nps1 ++ nps2] of
                 [] -> checkError $ "no alternatives left when resolving" <+> ppTerm Unqualified 0 f
                 h:_ -> return h

   matchVal mt v = elem mt [Nothing,Just v,Just (unlocked v)]

   unlocked v = case v of
     RecType fs -> RecType $ filter (not . isLockLabel . fst) (sortRec fs)
     _ -> v
   ---- TODO: accept subtypes
   ---- TODO: use a trie
   lookupOverloadInstance tys typs =
     [((pre,mkFunType rest val, t),isExact) |
       let lt = length tys,
       (ty,(val,t)) <- typs, length ty >= lt,
       let (pre,rest) = splitAt lt ty,
       let isExact = pre == tys,
       isExact || map unlocked pre == map unlocked tys
     ]

   noProds vfs = [(v,f) | (_,v,f) <- vfs, noProd v]

   noProd ty = case ty of
     Prod _ _ _ _ -> False
     _ -> True

checkLType :: SourceGrammar -> Context -> Term -> Type -> Check (Term, Type)
checkLType gr g trm typ0 = do
  typ <- computeLType gr g typ0

  case trm of

    Abs bt x c -> do
      case typ of
        Prod bt' z a b -> do
          (c',b') <- if isWildIdent z
                       then checkLType gr ((bt,x,a):g) c b
                       else do b' <- checkIn (pp "abs") $ substituteLType [(bt',z,Vr x)] b
                               checkLType gr ((bt,x,a):g) c b'
          return $ (Abs bt x c', Prod bt' z a b')
        _ -> checkError $ "function type expected instead of" <+> ppType typ $$
                          "\n   ** Double-check that the type signature of the operation" $$
                          "matches the number of arguments given to it.\n"

    App f a -> do
       over <- getOverload gr g (Just typ) trm
       case over of
         Just trty -> return trty
         _ -> do
          (trm',ty') <- inferLType gr g trm
          termWith trm' $ checkEqLType gr g typ ty' trm'

    AdHocOverload ts -> do
      over <- getOverload gr g Nothing trm
      case over of
        Just trty -> return trty
        _ -> checkError ("unresolved overloading of constants" <+> ppTerm Qualified 0 trm)

    Q _ -> do
       over <- getOverload gr g (Just typ) trm
       case over of
         Just trty -> return trty
         _ -> do
          (trm',ty') <- inferLType gr g trm
          termWith trm' $ checkEqLType gr g typ ty' trm'

    T _ [] ->
      checkError ("found empty table in type" <+> ppTerm Unqualified 0 typ)
    T _ cs -> case typ of
      Table arg val -> do
        case allParamValues gr arg of
          Ok vs -> do
            let ps0 = map fst cs
            ps <- testOvershadow ps0 vs
            if null ps
              then return ()
              else checkWarn ("patterns never reached:" $$
                              nest 2 (vcat (map (ppPatt Unqualified 0) ps)))
          _ -> return () -- happens with variable types
        cs' <- mapM (checkCase arg val) cs
        return (T (TTyped arg) cs', typ)
      _ -> checkError $ "table type expected for table instead of" $$ nest 2 (ppType typ)
    V arg0 vs ->
      case typ of
        Table arg1 val ->
           do arg' <- checkEqLType gr g arg0 arg1 trm
              vs1 <- allParamValues gr arg1
              if length vs1 == length vs
                 then return ()
                 else checkError $ "wrong number of values in table" <+> ppTerm Unqualified 0 trm
              vs' <- map fst `fmap` sequence [checkLType gr g v val|v<-vs]
              return (V arg' vs',typ)

    R r -> case typ of --- why needed? because inference may be too difficult
       RecType rr -> do
       --let (ls,_) = unzip rr        -- labels of expected type
         fsts <- mapM (checkM r) rr   -- check that they are found in the record
         return $ (R fsts, typ)       -- normalize record

       _ -> checkError ("record type expected in type checking instead of" $$ nest 2 (ppTerm Unqualified 0 typ))

    ExtR r s -> case typ of
       _ | typ == typeType -> do
         trm' <- computeLType gr g trm
         case trm' of
           RecType _ -> termWith trm' $ return typeType
           ExtR (Vr _) (RecType _) -> termWith trm' $ return typeType
                                      -- ext t = t ** ...
           _ -> checkError ("invalid record type extension" <+> nest 2 (ppTerm Unqualified 0 trm))

       RecType rr -> do

         ll2 <- case s of
           R ss -> return $ map fst ss
           _ -> do
             (s',typ2) <- inferLType gr g s
             case typ2 of
               RecType ss -> return $ map fst ss
               _ ->  checkError ("cannot get labels from" $$ nest 2 (ppTerm Unqualified 0 typ2))
         let ll1 = [l | (l,_) <- rr, notElem l ll2]

---         over <- getOverload gr g Nothing r --- this would solve #66 but fail ParadigmsAra. AR 6/7/2020
---         let r1 = maybe r fst over
         let r1 = r ---

         (r',_) <- checkLType gr g r1 (RecType [field | field@(l,_) <- rr, elem l ll1])
         (s',_) <- checkLType gr g s  (RecType [field | field@(l,_) <- rr, elem l ll2])

         let rec = R ([(l,(Nothing,P r' l)) | l <- ll1] ++ [(l,(Nothing,P s' l)) | l <- ll2])
         return (rec, typ)

       ExtR ty ex -> do
         r' <- justCheck g r ty
         s' <- justCheck g s ex
         return $ (ExtR r' s', typ) --- is this all? it assumes the same division in trm and typ

       _ -> checkError ("record extension not meaningful for" <+> ppTerm Unqualified 0 typ)

    FV vs -> do
      ttys <- mapM (flip (checkLType gr g) typ) vs
---      checkIfComplexVariantType trm typ
      return (FV (map fst ttys), typ) --- typ' ?

    S tab arg -> checks [ do
      (tab',ty) <- inferLType gr g tab
      ty'       <- computeLType gr g ty
      case ty' of
        Table p t -> do
          (arg',val) <- checkLType gr g arg p
          checkEqLType gr g typ t trm
          return (S tab' arg', t)
        _ -> checkError ("table type expected for applied table instead of" <+> ppType ty')
     , do
      (arg',ty) <- inferLType gr g arg
      ty'       <- computeLType gr g ty
      (tab',_)  <- checkLType gr g tab (Table ty' typ)
      return (S tab' arg', typ)
      ]
    Let (x,(mty,def)) body -> case mty of
      Just ty -> do
        (ty0,_)    <- checkLType gr g ty typeType
        (def',ty') <- checkLType gr g def ty0
        body' <- justCheck ((Explicit,x,ty'):g) body typ
        return (Let (x,(Just ty',def')) body', typ)
      _ -> do
        (def',ty) <- inferLType gr g def  -- tries to infer type of local constant
        checkLType gr g (Let (x,(Just ty,def')) body) typ

    ELin c tr -> do
      tr1 <- unlockRecord c tr
      checkLType gr g tr1 typ

    _ -> do
      (trm',ty') <- inferLType gr g trm
      termWith trm' $ checkEqLType gr g typ ty' trm'
 where
   justCheck g ty te = checkLType gr g ty te >>= return . fst
{-
   recParts rr t = (RecType rr1,RecType rr2) where
     (rr1,rr2) = partition (flip elem (map fst t) . fst) rr
-}
   checkM rms (l,ty) = case lookup l rms of
     Just (Just ty0,t) -> do
       checkEqLType gr g ty ty0 t
       (t',ty') <- checkLType gr g t ty
       return (l,(Just ty',t'))
     Just (_,t) -> do
       (t',ty') <- checkLType gr g t ty
       return (l,(Just ty',t'))
     _ -> checkError $
            if isLockLabel l
              then let cat = drop 5 (showIdent (label2ident l))
                   in ppTerm Unqualified 0 (R rms) <+> "is not in the lincat of" <+> cat <>
                      "; try wrapping it with lin" <+> cat
              else "cannot find value for label" <+> l <+> "in" <+> ppTerm Unqualified 0 (R rms)

   checkCase arg val (p,t) = do
     cont <- pattContext gr g arg p
     t' <- justCheck (reverse cont ++ g) t val
     return (p,t')

pattContext :: SourceGrammar -> Context -> Type -> Patt -> Check Context
pattContext env g typ p = case p of
  PV x -> return [(Explicit,x,typ)]
  PP (q,c) ps | q /= cPredef -> do ---- why this /=? AR 6/1/2006
    t <- lookupResType env (q,c)
    let (cont,v) = typeFormCnc t
    checkCond ("wrong number of arguments for constructor in" <+> ppPatt Unqualified 0 p)
              (length cont == length ps)
    checkEqLType env g typ v (patt2term p)
    mapM (\((_,_,ty),p) -> pattContext env g ty p) (zip cont ps) >>= return . concat
  PR r -> do
    typ' <- computeLType env g typ
    case typ' of
      RecType t -> do
        let pts = [(ty,tr) | (l,tr) <- r, Just ty <- [lookup l t]]
        ----- checkWarn $ prt p ++++ show pts ----- debug
        mapM (uncurry (pattContext env g)) pts >>= return . concat
      _ -> checkError ("record type expected for pattern instead of" <+> ppTerm Unqualified 0 typ')
  PT t p' -> do
    checkEqLType env g typ t (patt2term p')
    pattContext env g typ p'

  PAs x p -> do
    g' <- pattContext env g typ p
    return ((Explicit,x,typ):g')

  PAlt p' q -> do
    g1 <- pattContext env g typ p'
    g2 <- pattContext env g typ q
    let pts = nub ([x | pt@(_,x,_) <- g1, notElem pt g2] ++ [x | pt@(_,x,_) <- g2, notElem pt g1])
    checkCond
      ("incompatible bindings of" <+>
       fsep pts <+>
       "in pattern alterantives" <+> ppPatt Unqualified 0 p) (null pts)
    return g1 -- must be g1 == g2
  PSeq p q -> do
    g1 <- pattContext env g typ p
    g2 <- pattContext env g typ q
    return $ g1 ++ g2
  PRep p' -> noBind typeStr p'
  PNeg p' -> noBind typ p'

  _ -> return [] ---- check types!
 where
   noBind typ p' = do
    co <- pattContext env g typ p'
    if not (null co)
      then checkWarn ("no variable bound inside pattern" <+> ppPatt Unqualified 0 p)
           >> return []
      else return []

checkEqLType :: SourceGrammar -> Context -> Type -> Type -> Term -> Check Type
checkEqLType gr g t u trm = do
  (b,t',u',s) <- checkIfEqLType gr g t u trm
  case b of
    True  -> return t'
    False ->
      let inferredType = ppTerm Qualified 0 u
          expectedType = ppTerm Qualified 0 t
          term = ppTerm Unqualified 0 trm
          funName = pp . head . words .render $ term
          helpfulMsg =
            case (arrows inferredType, arrows expectedType) of
              (0,0) -> pp "" -- None of the types is a function
              _ -> "\n   **" <+>
                  if expectedType `isLessApplied` inferredType
                    then "Maybe you gave too few arguments to" <+> funName
                    else pp "Double-check that type signature and number of arguments match."
      in checkError $ s <+> "type of" <+> term $$
                            "expected:" <+> expectedType $$ -- ppqType t u $$
                            "inferred:" <+> inferredType $$ -- ppqType u t
                            helpfulMsg
  where
    -- count the number of arrows in the prettyprinted term
    arrows :: Doc -> Int
    arrows = length . filter (=="->") . words . render

    -- If prettyprinted type t has fewer arrows then prettyprinted type u,
    -- then t is "less applied", and we can print out more helpful error msg.
    isLessApplied :: Doc -> Doc -> Bool
    isLessApplied t u = arrows t < arrows u

checkIfEqLType :: SourceGrammar -> Context -> Type -> Type -> Term -> Check (Bool,Type,Type,String)
checkIfEqLType gr g t u trm = do
  t' <- computeLType gr g t
  u' <- computeLType gr g u
  case t' == u' || alpha [] t' u' of
    True -> return (True,t',u',[])
    -- forgive missing lock fields by only generating a warning.
    --- better: use a flag to forgive? (AR 31/1/2006)
    _ -> case missingLock [] t' u' of
      Ok lo -> do
        checkWarn $ "missing lock field" <+> fsep lo
        return (True,t',u',[])
      Bad s -> return (False,t',u',s)

  where

   -- check that u is a subtype of t
   --- quick hack version of TC.eqVal
   alpha g t u = case (t,u) of

     -- error (the empty type!) is subtype of any other type
     (_,u) | u == typeError -> True

     -- contravariance
     (Prod _ x a b, Prod _ y c d) -> alpha g c a && alpha ((x,y):g) b d

     -- record subtyping
     (RecType rs, RecType ts) -> all (\ (l,a) ->
                                   any (\ (k,b) -> l == k && alpha g a b) ts) rs
     (ExtR r s, ExtR r' s') -> alpha g r r' && alpha g s s'
     (ExtR r s, t) -> alpha g r t || alpha g s t

     -- the following say that Ints n is a subset of Int and of Ints m >= n
     -- But why does it also allow Int as a subtype of Ints m? /TH 2014-04-04
     (t,u) | Just m <- isTypeInts t, Just n <- isTypeInts u -> m >= n
           | Just _ <- isTypeInts t, u == typeInt           -> True ---- check size!
           | t == typeInt,           Just _ <- isTypeInts u -> True ---- why this ???? AR 11/12/2005

     ---- this should be made in Rename
     (Q  (m,a), Q  (n,b)) | a == b -> elem m (allExtendsPlus gr n)
                                   || elem n (allExtendsPlus gr m)
                                   || m == n --- for Predef
     (QC (m,a), QC (n,b)) | a == b -> elem m (allExtendsPlus gr n)
                                   || elem n (allExtendsPlus gr m)
     (QC (m,a), Q  (n,b)) | a == b -> elem m (allExtendsPlus gr n)
                                   || elem n (allExtendsPlus gr m)
     (Q  (m,a), QC (n,b)) | a == b -> elem m (allExtendsPlus gr n)
                                   || elem n (allExtendsPlus gr m)

     -- contravariance
     (Table a b,  Table c d)  -> alpha g c a && alpha g b d
     (Vr x,       Vr y)       -> x == y || elem (x,y) g || elem (y,x) g
     _                        -> t == u
     --- the following should be one-way coercions only. AR 4/1/2001
                                  || elem t sTypes && elem u sTypes
                                  || (t == typeType && u == typePType)
                                  || (u == typeType && t == typePType)

   missingLock g t u = case (t,u) of
     (RecType rs, RecType ts) ->
       let
         ls = [l | (l,a) <- rs,
                   not (any (\ (k,b) -> alpha g a b && l == k) ts)]
         (locks,others) = partition isLockLabel ls
       in case others of
         _:_ -> Bad $ render ("missing record fields:" <+> fsep (punctuate ',' (others)))
         _ -> return locks
     -- contravariance
     (Prod _ x a b, Prod _ y c d) -> do
        ls1 <- missingLock g c a
        ls2 <- missingLock g b d
        return $ ls1 ++ ls2

     _ -> Bad ""

   sTypes = [typeStr, typeTok, typeString]

-- auxiliaries

-- | light-weight substitution for dep. types
substituteLType :: Context -> Type -> Check Type
substituteLType g t = case t of
  Vr x -> return $ maybe t id $ lookup x [(x,t) | (_,x,t) <- g]
  _ -> composOp (substituteLType g) t

termWith :: Term -> Check Type -> Check (Term, Type)
termWith t ct = do
  ty <- ct
  return (t,ty)

-- | compositional check\/infer of binary operations
check2 :: (Term -> Check Term) -> (Term -> Term -> Term) ->
          Term -> Term -> Type -> Check (Term,Type)
check2 chk con a b t = do
  a' <- chk a
  b' <- chk b
  return (con a' b', t)

-- printing a type with a lock field lock_C as C
ppType :: Type -> Doc
ppType ty =
  case ty of
    RecType fs   -> case filter isLockLabel $ map fst fs of
                      [lock] -> pp (drop 5 (showIdent (label2ident lock)))
                      _      -> ppTerm Unqualified 0 ty
    Prod _ x a b -> ppType a <+> "->" <+> ppType b
    _            -> ppTerm Unqualified 0 ty
{-
ppqType :: Type -> Type -> Doc
ppqType t u = case (ppType t, ppType u) of
  (pt,pu) | render pt == render pu -> ppTerm Qualified 0 t
  (pt,_) -> pt
-}
checkLookup :: Ident -> Context -> Check Type
checkLookup x g =
  case [ty | (b,y,ty) <- g, x == y] of
    []     -> checkError ("unknown variable" <+> x)
    (ty:_) -> return ty