-- UUAGC 0.9.50.2 (build/103/lib-ehc/UHC/Light/Compiler/Ty.ag)
module UHC.Light.Compiler.Ty(TyAGItf (..), Ty (..), TyAnn (..), TyL, tyInt, tyChar
, tyLHdAndTl, tyProdArgs
, tyUnAnn
, tyCanonAnn
, TyVarId, mkTyVar, mkNewTyVar, mkNewUIDTyVarL, mkNewTyVarL, mkTyFreshProd, mkTyFreshProdFrom, tyEnsureNonAny
, TyVarIdL, TyVarIdS
, LookupTy
, TyVarWild (..), TyVarWildMp
, tvwmpNoQuantS
, mkTyQu, TyVarCateg (..)
, tyMbVar
, tyVar
, TyQu (..)
, tvCatIsPlain, tvCatIsFixed
, TvInfo (..)
, emptyTvInfo
, mkTvInfo, mkTvInfoTy
, TvCatMp, emptyTvCatMp
, tyQu_Forall, tyQu_Exists
, tyquIsExists, tyquIsForall
, tyquMetaLev
, tyquExists
, showTyQu
, tyAnnMono
, tyAnnDecomposeMk
, tyIsVar, tyIsCon
, tvIsPlain, tyIsVarPlain
, tyIsSimple
, tyMbCon, tyConNm
, Polarity
, polCovariant, polContravariant, polInvariant
, polIsCovariant, polIsContravariant, polIsInvariant
, polOpp
, FIMode (..)
, fimOpp
, fimSwapPol
, InstTo (..)
, instToSplitQu
, kiStar
, tyQu_KiForall, tyQu_KiExists
, tyAppFunArgsWithLkup
, TyKiKey (..)
, tyKiKeyMbName
, tyKiKeyIsName
, instToL1AssocL
, kiRow
, FldTyL
, tyRowUnAnn, tyRowExtsUnAnn
, tyMbConWithLkup
, tyAppFunMbConNm, tyAppFunConNm
, tyRowExtsWithLkup, tyRecExtrWithLkup, tyRecExtsWithLkup
, tyRowExtr, tyRecExtr, tyRecExts
, rowExtCmp
, tyRecOffset
, tyDataTyNm
, tyRecExts2
, tyRowOffsetOrder
, tyExtsOffset
, tyRecOffsetWithLkup
, Pred (..)
, Impls (..), ImplsVarId
, TyCtxt (..)
, tyEnsureNonAnyImpl
, LookupImpls
, tvCatIsMeta
, TvPurpose (..)
, tvpurposeIsTy
, mkTvInfoPlain
, PredScope (..), initPredScope
, pscpMbVar
, pscpEnter, pscpLeave
, pscpEnter', pscpLeave', pscpMk'
, pscpIsVisibleIn, pscpCommon
, pscpParents
, pscpCmp, pscpCmpByLen
, ImplsProveOcc (..), mkImplsProveOcc
, PredOcc (..), poId, mkPredOcc
, CHRPredOccCxt (..)
, CHRPredOcc' (..), CHRPredOcc, cpoScope, mkCHRPredOcc
, cpo2PredOcc
, mkTyMetaVar
, mkImplsTail, mkImplsVar, mkImplsNil
, mkTyImpls
, mkTyPr
, tyArrowArgResWithLkup
, tyArrowImplsResWithLkup, tyArrowImplsArgResWithLkup
, tyArrowImplsRes, tyArrowImplsArgRes
, tyQuant
, tyLImplsPreds
, tyPred, predNm, tyPredNm, tyPrArrowArgsRes
, tyPredMatchNmArgs, predMatchNmArgs
, tyPred2DataTy, pred2DataTy
, predTy
, predHasRuntimeEvidence
, implsPredsTailWithLkup, tyImplsWithLkup, implsPrIdLWithLkup
, tyImpls, implsPredsTail, implsPredsMbTail, implsIsTail, tyIsImplsTail, tyImplsPreds, implsPrIdPredL, implsPrIdL
, tyMb1ArrTailVar2VarWithLkup
, implsMbVar, implsTailVar
, implsIsEmpty
, tyIsPredicated, tyIsPredicatedWithLkup
, Label (..), LabelAGItf (..)
, LabelVarId
, LabelOffset (..)
, tyIsEmptyRow
, tyRowIsCanonOrdered
, labelMbVar
, tyLamArgsRes
, tyIsLam
, mkTyLam
, tyString
, tyAppFunArgsMk
, tyLamEtaRed
, tyDecomposeMk
, tyRecMap
, PredSeq (..)
, predSeqToList, predLFlatten
, mkPolNegate, mkPolVar
, tyAllConS
, tyInteger
, tyMbRecExts
, mkPredOccRng
, mkCHRPredOccRng
, tyIsA) where

import UHC.Util.Utils
import UHC.Light.Compiler.Base.Common
import UHC.Light.Compiler.Base.TermLike
import UHC.Light.Compiler.Base.HsName.Builtin
import UHC.Light.Compiler.Opts.Base
import Data.Maybe
import qualified Data.Set as Set
import qualified Data.Map as Map
import Data.List
import UHC.Util.Pretty
import UHC.Util.Utils
import Control.Monad
import UHC.Util.Binary
import UHC.Util.Serialize



{-|
There are some conventions/restrictions on the structure of types that are not enforced
by the abstract syntax:

Encoding of prove-constraints:
  concrete syntax:
    {! impls !} -> ty
  abstract syntax:
    Ty_App (Ty_App (Ty_Con "->") (Ty_Impls impls)) ty

Encoding of assume-constraints:
  concrete syntax:
    (ty, {! pred1 !}, ..., {! predn !})
  abstract syntax:
    Ty_Ext (... (Ty_Ext ty (prod m+1) (Ty_Pred pred_1) ) ...) (prod m+n) (Ty_Pred pred_n)

  In other words: the predicates are at the outset of a product, pred_n "more outermost"
  than pred_{n-1}.

-}


{-|
The basic alternatives encode the following:
- Con: data type constructors, including tuple constructors
- App: application to 1 argument, for example 'a -> b' is encoded as (App (App -> a) b)
- Any: representing Bot/Top depending on context: (1) unknown expected type, (2) error type
- Var: type variables, including a category: plain tyvars, fixed tyvars (aka skolems)

-}


{-|
The module UHC.Light.Compiler.Ty
contains the Haskell interface to the internal representation of types
used by EHC. The AST is described in Ty/AbsSyn.

-}








































type TyL        = [Ty]



type TyVarId    = VarId



type TyVarIdL   = [TyVarId]
type TyVarIdS   = VarIdS



type FldTyL = AssocL (Maybe HsName) Ty



type ImplsVarId    = VarId



type LabelVarId      = VarId



type LookupTy = TyVarId -> Maybe Ty



type LookupImpls = ImplsVarId -> Maybe Impls



-- | tyvars may act as wildcard, that is, they act as placeholders inside partial type signatures, providing
--   some structure. Such wildcards come in flavors:
data TyVarWild
  = TyVarWild_NoQuantTyExpr_YesQuantLetBinding		-- quantify: not in TyExpr, yes in let binding
  | TyVarWild_NoQuantTyExpr_NoQuantLetBinding		-- quantify: not in TyExpr, not in let binding (enforce monomorphism)
  deriving Eq

type TyVarWildMp = Map.Map TyVarId TyVarWild



tvwmpNoQuantS :: TyVarWildMp -> UIDS
tvwmpNoQuantS = Map.keysSet . Map.filter (== TyVarWild_NoQuantTyExpr_NoQuantLetBinding)



tvCatIsPlain :: TyVarCateg -> Bool
tvCatIsPlain TyVarCateg_Plain  = True
tvCatIsPlain _                 = False

tvCatIsFixed :: TyVarCateg -> Bool
tvCatIsFixed TyVarCateg_Fixed  = True
tvCatIsFixed _                 = False



tvCatIsMeta :: TyVarCateg -> Bool
tvCatIsMeta TyVarCateg_Meta   = True
tvCatIsMeta _                 = False



data TvPurpose
  = TvPurpose_Ty TyVarCateg     -- stands for unknown type, the known humble type variable
  | TvPurpose_Impls             -- possibly empty sequence of implicit parameters
  | TvPurpose_Scope             -- predicate scope
  | TvPurpose_Pred              -- predicate
  | TvPurpose_AssNm             -- assumed name, in CHR
  | TvPurpose_Label             -- label, in CHR, for ext records
  | TvPurpose_Offset            -- offset, in CHR, for ext records
  | TvPurpose_PredSeq           -- experimental still
  deriving (Eq,Ord)



instance Show TvPurpose where
  show (TvPurpose_Ty TyVarCateg_Fixed)  = "c"
  show (TvPurpose_Ty TyVarCateg_Meta )  = "m"
  show (TvPurpose_Ty _               )  = "v"
  show TvPurpose_Impls                  = "i"
  show TvPurpose_Scope                  = "s"
  show TvPurpose_Pred                   = "p"
  show TvPurpose_AssNm                  = "a"
  show TvPurpose_Label                  = "l"
  show TvPurpose_Offset                 = "o"
  show TvPurpose_PredSeq                = "s"



tvpurposeIsTy (TvPurpose_Ty _) = True
tvpurposeIsTy _                = False



data TvInfo
  = TvInfo
      { tvinfoCateg     :: !TyVarCateg
      , tvinfoPurpose   :: !TvPurpose
      }



emptyTvInfo
  = TvInfo TyVarCateg_Plain
           (TvPurpose_Ty TyVarCateg_Plain)



mkTvInfo = TvInfo

mkTvInfoTy :: TyVarCateg -> TvInfo
mkTvInfoTy c = mkTvInfo c (TvPurpose_Ty c)



instance Show TvInfo where
  show i | pur == TvPurpose_Ty TyVarCateg_Fixed && cat == TyVarCateg_Fixed = "c"
         | otherwise                                                       = show pur
    where cat = tvinfoCateg i
          pur = tvinfoPurpose i



mkTvInfoPlain :: TvPurpose -> TvInfo
mkTvInfoPlain p = mkTvInfo TyVarCateg_Plain p



type TvCatMp = Map.Map TyVarId TvInfo
emptyTvCatMp = Map.empty



data LabelOffset
  = LabelOffset_Off !Int
  | LabelOffset_Var !UID
  deriving
    ( Eq, Ord
    , Typeable, Data
    )



instance Show LabelOffset where
  show (LabelOffset_Off o) = show o
  show (LabelOffset_Var v) = "off_" ++ show v



data PredScope
  = PredScope_Lev !(RLList Int)
  | PredScope_Var !TyVarId
  deriving (Eq,Ord)

initPredScope :: PredScope
initPredScope = PredScope_Lev rllEmpty



deriving instance Typeable PredScope
deriving instance Data PredScope



pscpMbVar :: PredScope -> Maybe TyVarId
pscpMbVar (PredScope_Var v) = Just v
pscpMbVar _                 = Nothing



instance Show PredScope where
  show (PredScope_Lev l) = show l
  show (PredScope_Var v) = "[sc_" ++ show v ++ "]"



pscpEnter :: Int -> PredScope -> (Int,PredScope)
pscpEnter x (PredScope_Lev s) = (x+1,PredScope_Lev (s `rllConcat` rllSingleton x))

pscpLeave :: PredScope -> PredScope
pscpLeave (PredScope_Lev s) = PredScope_Lev $ fst $ fromJust $ rllInitLast s



-- enter yes/no scope, give back the threaded counter to outside the new scope and inside
-- use in conjunction with pscpLeave'
pscpEnter' :: Bool -> Int -> (Int,Int)
pscpEnter' yesEnter x
  = if yesEnter
    then (fst $ pscpEnter x initPredScope,0)
    else (x,x)

-- leave scope, on previous entering yes/no scope, give back the threaded counter to outside the new scope and inside
-- use in conjunction with pscpEnter'
pscpLeave' :: Bool -> Int -> Int -> Int
pscpLeave' yesEnter newScopeCounter innerScopeCounter
  = if yesEnter
    then newScopeCounter
    else innerScopeCounter

-- make scope, depending on yes/no entering
-- use in conjunction with pscpEnter'
pscpMk' :: Bool -> Int -> PredScope -> PredScope
pscpMk' yesEnter x s
  = if yesEnter
    then snd $ pscpEnter x s
    else s



pscpIsVisibleIn :: PredScope -> PredScope -> Bool
pscpIsVisibleIn (PredScope_Lev sOuter) (PredScope_Lev sInner) = sOuter `rllIsPrefixOf` sInner
pscpIsVisibleIn _                      _                      = False

pscpCommon :: PredScope -> PredScope -> Maybe PredScope
pscpCommon (PredScope_Lev s1) (PredScope_Lev s2)
  = Just $ PredScope_Lev $ commonPrefix s1 s2
  where commonPrefix xxs     yys     | isJust ht1 && isJust ht2 && x == y     = rllSingleton x `rllConcat` commonPrefix xs ys
                                     | otherwise                              = rllEmpty
                                     where ht1 = rllHeadTail xxs
                                           ht2 = rllHeadTail yys
                                           (x,xs) = fromJust ht1
                                           (y,ys) = fromJust ht2
        -- commonPrefix _       _                    = rllEmpty
pscpCommon _                  _
  = Nothing



pscpParents :: PredScope -> [PredScope]
pscpParents (PredScope_Lev s) | not (rllNull s) = map PredScope_Lev $ rllInits $ rllInit s
pscpParents _                                   = []



pscpCmp :: PredScope -> PredScope -> Maybe Ordering
pscpCmp (PredScope_Lev s) (PredScope_Lev t) = Just $ s `compare` t
pscpCmp _                 _                 = Nothing

pscpCmpByLen :: PredScope -> PredScope -> Ordering
pscpCmpByLen (PredScope_Lev s) (PredScope_Lev t) = (rllLength s) `compare` (rllLength t)



data ImplsProveOcc
  = ImplsProveOcc
      { ipoId       :: !UID
      , ipoScope    :: !PredScope
      }
  deriving (Eq,Show,Ord)

mkImplsProveOcc :: UID -> PredScope -> ImplsProveOcc
mkImplsProveOcc = ImplsProveOcc



deriving instance Typeable ImplsProveOcc
deriving instance Data ImplsProveOcc



data PredOcc
  =  PredOcc
       { poPr               :: !Pred
       , poPoi              :: !PredOccId
       , poScope            :: !PredScope
       , poRange            :: !Range
       }
  deriving (Show,Eq,Ord)

poId :: PredOcc -> UID
poId = poiId . poPoi

mkPredOcc :: Pred -> PredOccId -> PredScope -> PredOcc
mkPredOcc p i sc = rngLift emptyRange mkPredOccRng p i sc



mkPredOccRng :: Range -> Pred -> PredOccId -> PredScope -> PredOcc
mkPredOccRng r p i sc = PredOcc p i sc r



data CHRPredOccCxt
  = CHRPredOccCxt_Scope1
      { cpocxScope			:: !PredScope			-- default, only allowed value for occurring preds
      --											-- others for solving and CHR's only
      }
  deriving (Show,Eq,Ord)




deriving instance Typeable CHRPredOccCxt
deriving instance Data CHRPredOccCxt



data CHRPredOcc' p
  =  CHRPredOcc
       { cpoPr               :: !p
       -- , cpoScope            :: !PredScope
       , cpoCxt              :: !CHRPredOccCxt
       , cpoRange            :: !Range
       }
  deriving (Show,Eq,Ord)

type CHRPredOcc = CHRPredOcc' Pred

mkCHRPredOcc :: Pred -> PredScope -> CHRPredOcc
mkCHRPredOcc p sc = mkCHRPredOccRng emptyRange p sc

cpoScope :: CHRPredOcc -> PredScope
cpoScope = cpocxScope . cpoCxt



cpo2PredOcc :: PredOccId -> CHRPredOcc -> PredOcc
cpo2PredOcc i o
  = mkPredOccRng
      (cpoRange o)
      (cpoPr o)
      i
      (cpoScope o)



deriving instance Typeable1 CHRPredOcc'
deriving instance Data CHRPredOcc



mkCHRPredOccRng :: Range -> Pred -> PredScope -> CHRPredOcc
mkCHRPredOccRng r p sc = CHRPredOcc p (CHRPredOccCxt_Scope1 sc) r



tyQu_Forall = TyQu_Forall metaLevVal
tyQu_Exists = TyQu_Exists metaLevVal



tyQu_KiForall = TyQu_Forall metaLevTy
tyQu_KiExists = TyQu_Exists metaLevTy



tyquIsExists, tyquIsForall :: TyQu -> Bool



tyquIsForall (TyQu_Forall _)         = True
tyquIsForall _                       = False

tyquIsExists (TyQu_Exists _)         = True
tyquIsExists _                       = False



tyquMetaLev (TyQu_Forall l)         = l
tyquMetaLev (TyQu_Exists l)         = l
tyquMetaLev (TyQu_Plain  l)         = l



tyquExists, tyquForall :: TyQu -> TyQu



tyquForall   (TyQu_Exists l)         = TyQu_Forall l
tyquForall   q                       = q

tyquExists   (TyQu_Forall l)         = TyQu_Exists l
tyquExists   q                       = q



showTyQu  (TyQu_Forall 0) =  "forall"
showTyQu  (TyQu_Forall 1) =  "forall" ++ [charKindStar]
showTyQu  (TyQu_Forall l) =  "forall" ++ [charKindStar] ++ show l
showTyQu  (TyQu_Exists 0) =  "exists"
showTyQu  (TyQu_Exists 1) =  "exists" ++ [charKindStar]
showTyQu  (TyQu_Exists l) =  "exists" ++ [charKindStar] ++ show l
showTyQu  (TyQu_Plain  0) =  ""
showTyQu  (TyQu_Plain  1) =  [charKindStar]
showTyQu  (TyQu_Plain  l) =  [charKindStar] ++ show l



tyIsA :: Ty -> String
tyIsA (Ty_Con   a      ) = "CON"
tyIsA (Ty_App   a b    ) = "APP"
tyIsA (Ty_Ann   a b    ) = "ANN"
tyIsA (Ty_Var   a b    ) = "VAR"
tyIsA (Ty_Any          ) = "ANY"
tyIsA (Ty_TBind a b c d) = "QUANT"
tyIsA (Ty_Ext   a b c  ) = "EXT"
tyIsA (Ty_Pred  a      ) = "PRED"
tyIsA (Ty_Lam   a b    ) = "LAM"
tyIsA (Ty_Impls a      ) = "IMPLS"



-- | Remove TyAnn's
tyUnAnn :: Ty -> Ty
tyUnAnn = fst . appUnAnn
{-# INLINE tyUnAnn #-}



tyRowUnAnn :: AssocL HsName Ty -> AssocL HsName Ty
tyRowUnAnn = assocLMapElt tyUnAnn

tyRowExtsUnAnn :: (Ty,AssocL HsName Ty) -> (Ty,AssocL HsName Ty)
tyRowExtsUnAnn (x,y) = (tyUnAnn x,tyRowUnAnn y)



-- | Canonicalize TyAnn's
tyCanonAnn :: Ty -> Ty
tyCanonAnn t
  = c [] t
  where c seen t@(Ty_Ann a ta) | a `elem` seen = c seen ta
                               | otherwise     = Ty_Ann a $ c (a:seen) ta
        c _    t                               = t



-- | Add TyAnn
tyAnn :: TyAnn -> Ty -> Ty
tyAnn a t@(Ty_Ann a' _) | a == a' = t
tyAnn a t                         = Ty_Ann a t

-- | Add TyAnn_Mono
tyAnnMono :: Ty -> Ty
tyAnnMono = tyAnn TyAnn_Mono



-- | Decompose type for annotation into unannotated type + reconstruction
tyAnnDecomposeMk    :: Ty -> (Ty, [TyAnn], Ty -> Ty)
tyAnnDecomposeMk t
  = case t of
      Ty_Ann a t'       -> (ta,as,\ta' -> tyAnn a $ mk ta')
                        where (ta,as,mk) = tyAnnDecomposeMk t'
      _                 -> (t ,[],id)



tyIsVar :: Ty -> Bool
tyIsVar = isJust . tyMbVar

tyIsCon :: Ty -> Bool
tyIsCon = isJust . tyMbCon

tyIsQu :: Ty -> Bool
tyIsQu = isJust . tyMbQu



tyIsVarPlain :: Ty -> Bool
tyIsVarPlain = maybe False (tvCatIsPlain . snd) . tyMbVar'

tvIsPlain :: TvCatMp -> TyVarId -> Bool
tvIsPlain m v = maybe False (tvCatIsPlain . tvinfoCateg) $ Map.lookup v m



tyIsEmptyRow :: Ty -> Bool
tyIsEmptyRow = maybe False (== hsnRowEmpty) . tyMbCon



tyIsSimple :: Ty -> Bool
tyIsSimple t = tyIsVar t || tyIsCon t



tyIsLam :: Ty -> Bool
tyIsLam ty
  = not (null as)
  where (as,_) = tyLamArgsRes ty



instance AppLike Ty Ty {- TyAnn () -} where
  -- AppLike

  app1App        = Ty_App
  appTop         = id
  appCon         = Ty_Con . mkHNm
  appPar         = id
  appRngVar _    = panic "Ty.appRngVar"
  appProdApp tyL  = recRec (zip positionalFldNames tyL)
  -- appDflt		 = Ty_Any
  appDbg s		 = Ty_Dbg $ "*ERR: " ++ s ++ " :*"

  appMbCon (Ty_Con n) 	    = Just n
  appMbCon _            	= Nothing

  appMbApp1 (Ty_App f a) 	= Just (f,a)
  appMbApp1 _            	= Nothing

  appMbAnn1 (Ty_Ann a t) 	= Just (t, Ty_Ann a)
  appMbAnn1 _            	= Nothing

  appMbCanon1 t             = do (is,r) <- tyMbArrowImplsResWithLkup (const Nothing) t
                                 if not (null is) && all (maybe False implsIsEmpty . tyMbImpls) is then return (r, appArr is) else Nothing

  appMbDbg  (Ty_Dbg s)      = Just s
  appMbDbg  _            	= Nothing

  appMbBind1 (Ty_TBind q v k t) = Just (t, Ty_TBind q v k)
  appMbBind1 _            	    = Nothing



instance BndLike Ty TyVarId {- TyAnn () -} where
  -- BndLike
  bndBndIn n l x = Ty_TBind (TyQu_Plain (l-1)) n x



instance RecLike Ty Ty {- TyAnn () -} where
  -- RecLike
  recRow r 		= foldl (\t (n,e) -> Ty_Ext t n e) r

  recMbRecRow 	= tyMbRecRowWithLkup (const Nothing)
  recUnRowExts	= tyRowExtsWithLkup (const Nothing)



mkTyVar :: TyVarId -> Ty
mkTyVar tv = Ty_Var tv TyVarCateg_Plain



mkTyMetaVar :: TyVarId -> Ty
mkTyMetaVar tv = Ty_Var tv TyVarCateg_Meta



mkNewTyVar :: UID -> Ty
mkNewTyVar u = let  (_,v) = mkNewUID u in mkTyVar v



mkNewUIDTyVarL :: Int -> UID -> ([UID],TyL)
mkNewUIDTyVarL sz u = let vs = mkNewUIDL sz u in (vs,map mkTyVar vs)

mkNewTyVarL :: Int -> UID -> TyL
mkNewTyVarL sz u = snd (mkNewUIDTyVarL sz u)



tyEnsureNonAny :: UID -> Ty -> Ty
tyEnsureNonAny u t = if t /= Ty_Any then t else mkNewTyVar u



tyEnsureNonAnyImpl :: UID -> Ty -> Ty
tyEnsureNonAnyImpl u t
  = if t /= Ty_Any then  t
                   else  let  [i,r] = mkNewUIDL 2 u
                         in   [mkImplsVar i] `appArr` mkTyVar r



mkTyQu :: TyQu -> [(TyVarId,Ty)] -> Ty -> Ty
mkTyQu q tvL t = foldr (\(tv,k) t -> Ty_TBind q tv k t) t tvL



mkTyFreshProdFrom :: UID -> Int -> Ty
mkTyFreshProdFrom uid arity =  appProdApp . map mkTyVar . mkNewUIDL arity $ uid

mkTyFreshProd :: Int -> Ty
mkTyFreshProd = mkTyFreshProdFrom uidStart



mkTyLam :: [TyVarId] -> Ty -> Ty
mkTyLam args body = foldr Ty_Lam body args



mkImplsTail :: ImplsVarId -> Impls
mkImplsTail v = Impls_Tail v []

mkImplsVar :: ImplsVarId -> Ty
mkImplsVar v = Ty_Impls (mkImplsTail v)

mkImplsNil :: Ty
mkImplsNil = Ty_Impls Impls_Nil



mkTyImpls :: [Pred] -> Ty -> Ty
mkTyImpls prL t = map mkTyPr prL `appArr` t



mkTyPr :: Pred -> Ty
mkTyPr p
  =  case p of
       Pred_Pred t  -> t
       _            -> Ty_Pred p



tyInt :: Ty
tyInt   = appCon hsnInt



tyChar :: Ty
tyChar  = appCon hsnChar





kiStar :: Ty
kiStar  = appCon hsnKindStar



kiRow :: Ty
kiRow       = appCon hsnKindRow
-- tyRowEmpty  = appCon hsnRowEmpty



tyInteger :: Ty
tyInteger      	  = appCon hsnInteger





tyString :: EHCOpts -> Ty
tyString o = appCon (ehcOptBuiltin o ehbnPrelString)



-- tyArrowArgsRes  :: Ty -> (TyL,Ty)
-- tyAppFunArgs    :: Ty -> (Ty,TyL)
-- tyAppArgs       :: Ty -> TyL
-- tyArrowArgs     :: Ty -> TyL
-- tyArrowRes      :: Ty -> Ty
-- tyArrowArg      :: Ty -> Ty



tyArrowArgResWithLkup :: LookupTy -> Ty -> (Ty,Ty)
tyArrowArgResWithLkup lookup = tyVarChkVisitLift lookup appUn1Arr appUn1Arr



tyArrowImplsArgResWithLkup :: LookupTy -> Ty -> (TyL,Ty,Ty)
tyArrowImplsArgResWithLkup lookup t
  = (i,a,r)
  where (i,t')  = tyArrowImplsResWithLkup lookup t
        (a,r)   = tyArrowArgResWithLkup   lookup t'

tyMbArrowImplsResWithLkup :: LookupTy -> Ty -> Maybe (TyL,Ty)
tyMbArrowImplsResWithLkup lookup t
  = extr t
  where extr t = case appMb1Arr t of
                   Just (a,r)
                     | isImpls a'
                       -- -> let (as,r') = extr r in (a':as,r')
                       -> case extr r of
                            Just (as,r') -> Just (a':as,r')
                            _            -> Just ([a'],r)
                     where  a' = tyUnAnn a
                            isImpls (Ty_Pred  _)  = True
                            isImpls (Ty_Impls _)  = True
                            isImpls _             = False
                   _   -> tyVarLift lookup extr (const Nothing) t

tyArrowImplsResWithLkup :: LookupTy -> Ty -> (TyL,Ty)
tyArrowImplsResWithLkup lookup t = maybe ([],t) id $ tyMbArrowImplsResWithLkup lookup t



tyArrowImplsRes :: Ty -> (TyL,Ty)
tyArrowImplsRes = tyArrowImplsResWithLkup (const Nothing)

tyArrowImplsArgRes  :: Ty -> (TyL,Ty,Ty)
tyArrowImplsArgRes = tyArrowImplsArgResWithLkup (const Nothing)



tyProdArgs      :: Ty -> TyL
tyLHdAndTl      :: [Ty] -> (Ty,TyL)



-- Substitution aware
tyAppFunArgsWithLkup :: LookupTy -> Ty -> (Ty,TyL)
tyAppFunArgsWithLkup lookup = tyVarChkVisitLift lookup appUnApp appUnApp
{-# INLINE tyAppFunArgsWithLkup #-}



tyAppFunArgsMk    :: Ty -> (Ty, TyL, Ty -> TyL -> Ty)
tyAppFunArgsMk
  =  extr []
  where  extr as t
           =  case tyUnAnn t of
                Ty_TBind q v k t  -> (f,as,\f as -> Ty_TBind q v k $ mk f as)
                                  where (f,as,mk) = tyAppFunArgsMk t
                Ty_App f a        -> extr (a:as) f
                _                 -> (t,as,\f as -> appTopApp (f:as))



tyLHdAndTl   = hdAndTl' Ty_Any
{-# INLINE tyLHdAndTl #-}



tyMbCon :: Ty -> Maybe HsName
-- tyMbCon t = case tyUnAnn t of {Ty_Con nm -> Just nm ; _ -> Nothing}
tyMbCon = appMbCon -- . fst . appUnAnn
{-# INLINE tyMbCon #-}

tyConNm :: Ty -> HsName
tyConNm = maybe hsnUnknown id . tyMbCon
{-# INLINE tyConNm #-}



tyMbConWithLkup :: LookupTy -> Ty -> Maybe HsName
tyMbConWithLkup lookup = tyVarChkVisitLift lookup tyMbCon tyMbCon
{-# INLINE tyMbConWithLkup #-}



tyMbVar' :: Ty -> Maybe (TyVarId,TyVarCateg)
tyMbVar' t = case tyUnAnn t of {Ty_Var v c -> Just (v,c) ; _ -> Nothing}

tyMbVar :: Ty -> Maybe TyVarId
tyMbVar = fmap fst . tyMbVar'
{-# INLINE tyMbVar #-}



tyMbQu :: Ty -> Maybe TyQu
tyMbQu t
  = case tyUnAnn t of
      Ty_TBind q _ _ _
        -> Just q
      _ -> Nothing



tyVar :: Ty -> TyVarId
tyVar = maybe uidStart id . tyMbVar
{-# INLINE tyVar #-}



tyProdArgs ty = let (t,al) = tyRecExts ty in map snd al



tyAppFunMbConNm :: Ty -> Maybe HsName
tyAppFunMbConNm = tyMbCon . fst . appUnApp
{-# INLINE tyAppFunMbConNm #-}

tyAppFunConNm :: Ty -> HsName
tyAppFunConNm = tyConNm . fst . appUnApp
{-# INLINE tyAppFunConNm #-}



-- | The name of a data type extracted from a Ty
tyDataTyNm :: Ty -> HsName
tyDataTyNm = tyAppFunConNm . appUnArrRes



-- | All constructors occurring in a type
tyAllConS    :: Ty -> Set.Set HsName
tyAllConS t
  =  Set.unions $ (maybe Set.empty Set.singleton $ tyMbCon f) : map tyAllConS a
  where (f,a,_) = tyDecomposeMk t



tyQuant :: Ty -> Ty
tyQuant t
  =  case tyUnAnn t of
       Ty_TBind _ _ _ t'  -> tyQuant t'
       _                  -> t



tyLImplsPreds :: TyL -> ([Pred],Impls)
tyLImplsPreds = foldr (\t (ps,i) -> case tyUnAnn t of {Ty_Pred p -> (p:ps,i); Ty_Impls i -> (ps,i)}) ([],Impls_Nil)



tyLamArgsRes :: Ty -> ([TyVarId],Ty)
tyLamArgsRes
  =  extr
  where  extr t
           =  case tyUnAnn t of
                Ty_Lam a r  -> (a:as',r')
                            where (as',r') = extr r
                _           -> ([],t)



-- Eta reduce when the full list of args can be eliminated thus, i.e. it matches with the tail of the args applied in the app (if any) of the body
tyLamEtaRed :: Ty -> Maybe Ty
tyLamEtaRed t
  | llas > 0 && rlDiff >= 0 && map mkTyVar las == rTl = Just (appTopApp (f:rHd))
  | otherwise                                         = Nothing
  where (las,r  ) = tyLamArgsRes t
        (f  ,ras) = appUnApp r
        llas      = length las
        rlas      = length ras
        rlDiff	  = rlas - llas
        (rHd,rTl) = splitAt rlDiff ras



-- mkTyRow :: Ty -> AssocL HsName Ty -> Ty
-- mkTyRow r = foldl (\t (n,e) -> Ty_Ext t n e) r

{-
mkTyRec :: AssocL HsName Ty -> Ty
mkTyRec al = hsnRec `appConApp` [recRowEmp `recRow` al]

mkTyRecExt :: Ty -> AssocL HsName Ty -> Ty
mkTyRecExt recd al
  =  let  (row,exts) = recUnRowExts (recUnRecRow recd)
     in   hsnRec `appConApp` [row `recRow` (exts ++ al)]
-}

-- mkTySum :: AssocL HsName Ty -> Ty
-- mkTySum al = hsnSum `appConApp` [recRowEmp `recRow` al]



tyVarChkVisitLift :: LookupTy -> (Ty -> x) -> (Ty -> x) -> Ty -> x
tyVarChkVisitLift
  = withLkupChkVisitLift tyMbVar (noVisit . tyUnAnn)
  where noVisit (Ty_TBind _ qv _ _) = Set.singleton qv
        noVisit _                   = Set.empty

tyVarLift :: LookupTy -> (Ty -> x) -> (Ty -> x) -> Ty -> x
tyVarLift = withLkupLift tyMbVar
{-# INLINE tyVarLift #-}



implsTailVarLiftCyc :: (TyVarId -> Maybe Impls) -> (TyVarIdS -> Impls -> x) -> (Impls -> x) -> TyVarIdS -> Impls -> x
implsTailVarLiftCyc = withLkupLiftCyc1 implsMbVar (const Set.empty)
{-# INLINE implsTailVarLiftCyc #-}



tyRowExtsWithLkup :: LookupTy -> Ty -> (Ty,AssocL HsName Ty)
tyRowExtsWithLkup lookup
  =  extr []
  where  extr as t
           =  case tyUnAnn t of
                (Ty_Ext r l e) -> extr ((l,e):as) r
                t'             -> tyVarLift lookup (extr as) (flip (,) as) t'

tyRecExtsWithLkup :: LookupTy -> Ty -> (Ty,AssocL HsName Ty)
tyRecExtsWithLkup lookup t
  =  case tyRecRowWithLkup lookup t of
       Ty_Any  -> (Ty_Any,[])
       row     -> tyRowExtsWithLkup lookup row

tyRecRowWithLkup :: LookupTy -> Ty -> Ty
tyRecRowWithLkup lookup = maybe Ty_Any id . tyMbRecRowWithLkup lookup

tyRowExtrWithLkup :: LookupTy -> HsName -> Ty -> Maybe (Ty,Ty)
tyRowExtrWithLkup lookup lbl t
  = extr t
  where extr t
          = case tyUnAnn t of
              (Ty_Ext r l e) | lbl == l   -> Just (r,e)
                             | otherwise  -> maybe Nothing (\(r',e') -> Just (Ty_Ext r' l e,e')) (extr r)
              t'                          -> tyVarLift lookup extr (const Nothing) t'

tyRecExtrWithLkup :: LookupTy -> HsName -> Ty -> Maybe (Ty,Ty)
tyRecExtrWithLkup lookup lbl t
  =  case tyRowExtrWithLkup lookup lbl (tyRecRowWithLkup lookup t) of
       Nothing    -> Nothing
       Just (r,e) -> Just (hsnRec `appConApp` [r],e)

tyMbRecRowWithLkup :: LookupTy -> Ty -> Maybe Ty
tyMbRecRowWithLkup lookup t
  =  case tyAppFunArgsWithLkup lookup t of
       (f,[row])
         -> case tyMbConWithLkup lookup f of
              Just n | hsnIsRec n || hsnIsSum n -> Just row
              _                                 -> Nothing
       _                                        -> Nothing






-- tyMbRecRow :: Ty -> Maybe Ty
-- tyMbRecRow = tyMbRecRowWithLkup (const Nothing)
-- {-# INLINE tyMbRecRow #-}
{-
  =  case tyAppFunArgs t of
       (Ty_Con n,[row]) | hsnIsRec n || hsnIsSum n -> Just row
       _                                           -> Nothing
-}

-- tyRecRow :: Ty -> Ty
-- tyRecRow = maybe Ty_Any id . recMbRecRow
-- {-# INLINE tyRecRow #-}

-- tyRowExts :: Ty -> (Ty,AssocL HsName Ty)
-- tyRowExts = tyRowExtsWithLkup (const Nothing)
-- {-# INLINE tyRowExts #-}

tyRecExts :: Ty -> (Ty,AssocL HsName Ty)
tyRecExts = tyRecExtsWithLkup (const Nothing)
{-# INLINE tyRecExts #-}

tyRowExtr :: HsName -> Ty -> Maybe (Ty,Ty)
tyRowExtr = tyRowExtrWithLkup (const Nothing)
{-# INLINE tyRowExtr #-}

tyRecExtr :: HsName -> Ty -> Maybe (Ty,Ty)
tyRecExtr = tyRecExtrWithLkup (const Nothing)
{-# INLINE tyRecExtr #-}



tyMbRecExts :: Ty -> Maybe (Ty,AssocL HsName Ty)
tyMbRecExts = fmap recUnRowExts . recMbRecRow



tyRecExts2 :: Ty -> AssocL HsName (AssocL HsName Ty)
tyRecExts2
  = assocLMapElt (snd . tyRecExts) . snd . tyRecExts



tyDecomposeMk    :: Ty -> (Ty, TyL, Ty -> TyL -> Ty)
tyDecomposeMk t
  = case t of
      Ty_TBind q v k t' -> (f,as,\f' as' -> Ty_TBind q v k $ mk f' as')
                        where (f,as,mk) = tyDecomposeMk t'
      Ty_App _ _        -> (f,as,\f' as' -> appTopApp (f':as'))
                        where (f,as) = appUnApp t
      Ty_Ext _ _ _      -> (r,assocLElts e,\r' e' -> recRow r' $ zip (assocLKeys e) e')
                        where (r,e) = recUnRowExts t
      _ | not (null an) -> (t2,as,\f' as' -> mk1 $ mk2 f' as')
        | otherwise     -> (t,[],const)
                        where (t1,an,mk1) = tyAnnDecomposeMk t
                              (t2,as,mk2) = tyDecomposeMk    t1



-- | Map 'f' over fields of record
tyRecMap :: (Ty -> Ty) -> Ty -> Ty
tyRecMap f r
  = mk rem (map f fs)
  where (rem,fs,mk) = tyDecomposeMk r



tyRowIsCanonOrdered :: AssocL HsName a -> Bool
tyRowIsCanonOrdered = isSortedByOn rowLabCmp fst
{-# INLINE tyRowIsCanonOrdered #-}



rowExtCmp :: (HsName,a) -> (HsName,a) -> Ordering
rowExtCmp (n1,_) (n2,_) = n1 `rowLabCmp` n2
{-# INLINE rowExtCmp #-}

-- tyRowCanonOrderBy :: (o -> o -> Ordering) -> AssocL o a -> AssocL o a
-- tyRowCanonOrderBy = rowCanonOrderBy
-- {-# INLINE tyRowCanonOrderBy #-}

-- tyRowCanonOrder :: AssocL HsName a -> AssocL HsName a
-- tyRowCanonOrder = tyRowCanonOrderBy rowLabCmp
-- {-# INLINE tyRowCanonOrder #-}



tyRowOffsetOrder :: (a -> Int) -> AssocL HsName a -> AssocL HsName a
tyRowOffsetOrder off = sortOn (off . snd)
{-# INLINE tyRowOffsetOrder #-}



tyExtsOffset :: HsName -> AssocL HsName a -> ((Int,Presence),Maybe a)
tyExtsOffset lbl exts
  = find 0 lbl exts
  where find o l (e@(_,a):es) = case (l,panic "Ty.tyExtsOffset") `rowExtCmp` e of
                            GT -> find (o+1) l es
                            EQ -> ((o,Present),Just a)
                            LT -> ((o,Absent),Nothing)
        find o _ []     = ((o,Absent),Nothing)

tyRecOffset :: HsName -> Ty -> Int
tyRecOffset lbl t
  = fst $ fst $ tyExtsOffset lbl $ rowCanonOrder exts
  where (_,exts) = tyRecExts t



tyRecOffsetWithLkup :: LookupTy -> HsName -> Ty -> Int
tyRecOffsetWithLkup lookup nm
  = tyVarLift lookup o o
  where o = tyRecOffset nm



tyPred :: Ty -> Pred
tyPred t
  =  case tyUnAnn t of
       Ty_Pred pt  -> pt
       _           -> Pred_Pred t

predNm :: Pred -> HsName
predNm = tyAppFunConNm . predTy
{-# INLINE predNm #-}

tyPredNm :: Ty -> HsName
tyPredNm = predNm . tyPred
{-# INLINE tyPredNm #-}

tyPrArrowArgsRes :: Ty -> ([Pred],Pred)
tyPrArrowArgsRes tp = let (tl,t) = appUnArr tp in (map tyPred tl, tyPred t)



-- | extract class name and class args of predicate packages as Ty
tyPredMatchNmArgs :: Ty -> (HsName,[Ty])
tyPredMatchNmArgs = predMatchNmArgs . tyPred
{-# INLINE tyPredMatchNmArgs #-}

-- | extract class name and class args of predicate
predMatchNmArgs :: Pred -> (HsName,[Ty])
predMatchNmArgs p
  =  case p of
       Pred_Class t    -> (tyAppFunConNm t, appUnAppArgs t)
       Pred_Pred  t    -> predMatchNmArgs $ snd $ tyPrArrowArgsRes t
       Pred_Lacks _ (Label_Lab l)  -> (hsnUniqify HsNameUniqifier_LacksLabel l, [])
       Pred_Lacks _ _              -> (mkHNm "_LabVar_", [])      -- necessary? only used by CHR's
       Pred_Eq t1 t2   -> (hsnEqTilde,[t1,t2])



-- | construct for a predicate its corresponding data type
pred2DataTy :: Pred -> Ty
pred2DataTy p
  = appConApp (hsnClass2Dict n) as
  where (n,as) = predMatchNmArgs p

-- | construct for a predicate packaged as a Ty its corresponding data type
tyPred2DataTy :: Ty -> Ty
tyPred2DataTy = pred2DataTy . tyPred
{-# INLINE tyPred2DataTy #-}



predTy :: Pred -> Ty
predTy p
  =  case p of
       Pred_Class t    -> t
       Pred_Pred  t    -> t
       Pred_Lacks    t _  -> t
       Pred_Eq t _ -> t  -- does it matter if we return the left or the right type?



predSeqToList :: PredSeq -> [Pred]
predSeqToList (PredSeq_Cons h t) = h : predSeqToList t
predSeqToList _                  = []

predLFlatten :: [Pred] -> [Pred]
predLFlatten
  = concatMap fl
  where fl (Pred_Preds s) = predSeqToList s
        fl p              = [p]



-- | Is runtime evidence required for the predicate?
predHasRuntimeEvidence :: Pred -> Bool
predHasRuntimeEvidence p
  =  case p of
       Pred_Eq _ _ -> False
       _           -> True



implsPredsTailWithLkup' :: (TyVarId -> Maybe Impls) -> PredScope -> Impls -> ([(PredOcc,[ImplsProveOcc])],Impls)
implsPredsTailWithLkup' lookup sc i
  = extr Set.empty i
  where extr vsVisited i
          = case i of
              Impls_Cons _ p pv prange ipos t
                -> ((mkPredOccRng prange p pv sc,ipos) : p',mi)
                where (p',mi) = extr vsVisited t
              _ -> implsTailVarLiftCyc lookup extr ((,) []) vsVisited i

implsPredsTailWithLkup :: (TyVarId -> Maybe Impls) -> PredScope -> Impls -> ([PredOcc],Impls)
implsPredsTailWithLkup lookup sc i
  = (map fst is,t)
  where (is,t) = implsPredsTailWithLkup' lookup sc i

tyImplsWithLkup :: LookupTy -> Ty -> Impls
tyImplsWithLkup lookup = tyVarLift lookup tyImpls tyImpls
{-# INLINE tyImplsWithLkup #-}

implsPrIdLWithLkup :: (TyVarId -> Maybe Impls) -> Impls -> [PredOccId]
implsPrIdLWithLkup lookup = map poPoi . fst . implsPredsTailWithLkup lookup initPredScope
{-# INLINE implsPrIdLWithLkup #-}




tyMbVarWithLkup :: LookupTy -> Ty -> Maybe TyVarId
tyMbVarWithLkup lookup = tyVarLift lookup tyMbVar tyMbVar



tyMbImpls :: Ty -> Maybe Impls
tyMbImpls
  = extr . tyUnAnn
  where extr (Ty_Impls i) = Just i
        extr _            = Nothing

tyImpls :: Ty -> Impls
tyImpls = panicJust "tyImpls" . tyMbImpls
{-# INLINE tyImpls #-}

implsPredsTail' :: PredScope -> Impls -> ([(PredOcc,[ImplsProveOcc])],Impls)
implsPredsTail' = implsPredsTailWithLkup' (const Nothing)
{-# INLINE implsPredsTail' #-}

implsPredsTail :: PredScope -> Impls -> ([PredOcc],Impls)
implsPredsTail = implsPredsTailWithLkup (const Nothing)
{-# INLINE implsPredsTail #-}

implsPredsMbTail :: Impls -> ([(PredOcc,[ImplsProveOcc])],Maybe Impls)
implsPredsMbTail i =  case implsPredsTail' initPredScope i of
                        (i',t@(Impls_Tail _ _)) -> (i',Just t)
                        (i',   Impls_Nil      ) -> (i',Nothing)

tyImplsPreds :: PredScope -> Ty -> [PredOcc]
tyImplsPreds sc = fst . implsPredsTail sc . tyImpls
{-# INLINE tyImplsPreds #-}

implsIsTail :: Impls -> Bool
implsIsTail = isJust . implsMbVar
{-# INLINE implsIsTail #-}

tyIsImplsTail :: Ty -> Bool
tyIsImplsTail = implsIsTail . tyImpls
{-# INLINE tyIsImplsTail #-}

implsPrIdPredL :: Impls -> [(PredOccId,Pred)]
implsPrIdPredL i = [ (poPoi po, poPr po) | po <- fst $ implsPredsTail initPredScope i ]

implsPrIdL :: Impls -> [PredOccId]
implsPrIdL = map fst . implsPrIdPredL
{-# INLINE implsPrIdL #-}



-- | Is an 'Impls' the tail (last empty element) of a sequence?
implsMbTailVarWithLkup :: LookupImpls -> Impls -> Maybe ImplsVarId
implsMbTailVarWithLkup lkup (Impls_Tail iv _) = maybe (Just iv) (const Nothing) (lkup iv)
implsMbTailVarWithLkup _    _                 = Nothing
{-# INLINE implsMbTailVarWithLkup #-}

-- | Is a 'Ty' the tail of an Impls?
tyMbTailVarWithLkup :: LookupImpls -> Ty -> Maybe ImplsVarId
tyMbTailVarWithLkup lkup t = do { i <- tyMbImpls t ; implsMbTailVarWithLkup lkup i }
{-# INLINE tyMbTailVarWithLkup #-}

-- | Is 'Ty' a function type from an Impls tail to ...
tyMb1ArrTailVarWithLkup :: LookupImpls -> Ty -> Maybe (ImplsVarId,Ty)
tyMb1ArrTailVarWithLkup lkup t = do { (a,r) <- appMb1Arr t; i <- tyMbTailVarWithLkup lkup a; return (i,r) }
{-# INLINE tyMb1ArrTailVarWithLkup #-}

-- | Is 'Ty' a function type from an Impls tail to a ty var
tyMb1ArrTailVar2VarWithLkup :: LookupTy -> LookupImpls -> Ty -> Maybe (ImplsVarId,TyVarId)
tyMb1ArrTailVar2VarWithLkup lkupt lkupi t = do { (i,r) <- tyMb1ArrTailVarWithLkup lkupi t; v <- tyMbVarWithLkup lkupt r; return (i,v) }



implsMbVar :: Impls -> Maybe TyVarId
implsMbVar (Impls_Tail v _)  = Just v
implsMbVar _                 = Nothing

implsTailVar :: Impls -> ImplsVarId
implsTailVar = panicJust "implsTailVar" . implsMbVar
{-# INLINE implsTailVar #-}



implsIsEmpty :: Impls -> Bool
implsIsEmpty (Impls_Cons _ _ _ _ _ _) = False
implsIsEmpty _                        = True



tyIsPredicated :: Ty -> Bool
tyIsPredicated (Ty_Impls i) = not $ implsIsEmpty i
tyIsPredicated t            = isPr a
                            where a = map tyUnAnn $ appUnArrArgs t
                                  isPr (Ty_Pred p:_) = True
                                  isPr _             = False

tyIsPredicatedWithLkup :: LookupTy -> Ty -> Bool
tyIsPredicatedWithLkup lookup = tyVarLift lookup tyIsPredicated tyIsPredicated
{-# INLINE tyIsPredicatedWithLkup #-}



labelMbVar :: Label -> Maybe TyVarId
labelMbVar (Label_Var v)  = Just v
labelMbVar _              = Nothing



data TyKiKey
  = TyKiKey_Name    !HsName
  | TyKiKey_TyVar   !TyVarId
  deriving (Eq,Ord)

instance Show TyKiKey where
  show (TyKiKey_Name  n) = show n
  show (TyKiKey_TyVar v) = show v



deriving instance Typeable TyKiKey
deriving instance Data TyKiKey



tyKiKeyMbName :: TyKiKey -> Maybe HsName
tyKiKeyMbName (TyKiKey_Name n) = Just n
tyKiKeyMbName _                = Nothing



tyKiKeyIsName :: TyKiKey -> Bool
tyKiKeyIsName = isJust . tyKiKeyMbName
{-# INLINE tyKiKeyIsName #-}



data TyCtxt = TyCtxt_Ty | TyCtxt_Pred | TyCtxt_Class deriving (Show,Eq)



type Polarity = Ty



polCovariant :: Polarity
polCovariant = appCon hsnCovariant

polContravariant :: Polarity
polContravariant = appCon hsnContravariant

polInvariant :: Polarity
polInvariant = appCon hsnInvariant



mkPolNegate :: Polarity -> Polarity
mkPolNegate = appCon1App hsnPolNegation

mkPolVar :: UID -> Polarity
mkPolVar = mkTyVar



polIs :: HsName -> Polarity -> Bool
polIs nm = maybe False (== nm) . tyMbCon

polIsCovariant, polIsContravariant, polIsInvariant :: Polarity -> Bool
polIsCovariant     = polIs hsnCovariant
polIsContravariant = polIs hsnContravariant
polIsInvariant     = polIs hsnInvariant



polOpp :: Polarity -> Polarity
polOpp pol | polIsCovariant     pol = polContravariant
           | polIsContravariant pol = polCovariant
           | otherwise              = polInvariant



data FIMode  =  FitSubLR
             |  FitSubRL
             |  FitUnify
             deriving (Eq,Ord)



fimOpp :: FIMode -> FIMode
fimOpp m
  =  case m of
       FitSubLR  -> FitSubRL
       FitSubRL  -> FitSubLR
       _         -> m



fimSwapPol :: Polarity -> FIMode -> FIMode
fimSwapPol pol m = if polIsContravariant pol then fimOpp m else m



instance Show FIMode where
  show FitSubLR  = "<="
  show FitSubRL  = ">="
  show FitUnify  = "=="



data InstTo
  = InstTo_Plain        				-- a plain value
  | InstTo_Qu                           -- the fresh type (tyvar) instantiated to
      { instoQu     	:: TyQu			-- how tvar was quantified, also includes the meta level
      , instoFrom   	:: TyVarId		-- the tvar from which is instantiated
      , instoTo     	:: TyVarId		-- the new tvar to which is instantiated
      , instoL1     	:: Ty
      }
{-
  | InstTo_Lam                          -- a lambda
      { instoLam    :: [InstTo]
      }
-}
  deriving Show



instToIsQu :: InstTo -> Bool
instToIsQu (InstTo_Qu _ _ _ _) = True
instToIsQu _                   = False



-- split of initial quantifier instantiations, to be used for Sys F generation for type parameterization
instToSplitQu :: [InstTo] -> ([InstTo],[InstTo])
instToSplitQu = span instToIsQu



-- get tvar -> kind bindings of instantiation
instToL1AssocL :: [InstTo] -> AssocL TyVarId (MetaLev,Ty)
instToL1AssocL l = [ (v,(tyquMetaLev q,k)) | (InstTo_Qu q _ v k) <- l ]



instance Serialize TyKiKey where
  sput (TyKiKey_Name  a) = sputWord8 0 >> sput a
  sput (TyKiKey_TyVar a) = sputWord8 1 >> sput a
  sget = do t <- sgetWord8
            case t of
              0 -> liftM TyKiKey_Name  sget
              1 -> liftM TyKiKey_TyVar sget



instance Binary ImplsProveOcc where
  put (ImplsProveOcc a b) = put a >> put b
  get = liftM2 ImplsProveOcc get get

instance Serialize ImplsProveOcc where
  sput = sputPlain
  sget = sgetPlain

instance Binary PredScope where
  put (PredScope_Lev   a      ) = putWord8 0  >> put a
  put (PredScope_Var   a      ) = putWord8 1  >> put a
  get = do tag <- getWord8
           case tag of
             0  -> liftM  PredScope_Lev   get
             1  -> liftM  PredScope_Var   get

instance Serialize PredScope where
  sput = sputPlain
  sget = sgetPlain

instance Binary CHRPredOccCxt where
  put (CHRPredOccCxt_Scope1 a) = put a
  get = liftM CHRPredOccCxt_Scope1 get

instance Serialize CHRPredOccCxt where
  sput = sputPlain
  sget = sgetPlain

instance Binary LabelOffset where
  put (LabelOffset_Off a) = putWord8 0 >> put a
  put (LabelOffset_Var a) = putWord8 1 >> put a
  get = do t <- getWord8
           case t of
             0 -> liftM LabelOffset_Off get
             1 -> liftM LabelOffset_Var get

instance Serialize LabelOffset where
  sput = sputPlain
  sget = sgetPlain




instance Binary TyQu where
  put (TyQu_Forall a) = putWord8 0 >> put a
  put (TyQu_Exists a) = putWord8 1 >> put a
  put (TyQu_Plain  a) = putWord8 1 >> put a
  get = do tag <- getWord8
           case tag of
             0 -> liftM  TyQu_Forall   get
             1 -> liftM  TyQu_Exists   get
             2 -> liftM  TyQu_Plain    get

instance Serialize TyQu where
  sput = sputPlain
  sget = sgetPlain



instance Serialize Ty where
  sput (Ty_Con   a      ) = sputWord8 0  >> sput a
  sput (Ty_App   a b    ) = sputWord8 1  >> sput a >> sput b
  sput (Ty_Ann   a b    ) = sputWord8 2  >> sput a >> sput b
  sput (Ty_Var   a b    ) = sputWord8 3  >> sput a >> sput b
  sput (Ty_Any          ) = sputWord8 4
  sput (Ty_TBind a b c d) = sputWord8 5  >> sput a >> sput b >> sput c >> sput d
  sput (Ty_Ext   a b c  ) = sputWord8 6  >> sput a >> sput b >> sput c
  sput (Ty_Pred  a      ) = sputWord8 7  >> sput a
  sput (Ty_Lam   a b    ) = sputWord8 8  >> sput a >> sput b
  sput (Ty_Impls a      ) = sputWord8 9  >> sput a
  sput (Ty_Dbg   a      ) = sputWord8 10 >> sput a
  sget = do tag <- sgetWord8
            case tag of
              0  -> liftM  Ty_Con   sget
              1  -> liftM2 Ty_App   sget sget
              2  -> liftM2 Ty_Ann   sget sget
              3  -> liftM2 Ty_Var   sget sget
              4  -> return Ty_Any
              5  -> liftM4 Ty_TBind sget sget sget sget
              6  -> liftM3 Ty_Ext   sget sget sget
              7  -> liftM  Ty_Pred  sget
              8  -> liftM2 Ty_Lam   sget sget
              9  -> liftM  Ty_Impls sget
              10 -> liftM  Ty_Dbg   sget

instance Serialize TyAnn where
  sput (TyAnn_Empty       ) = sputWord8 0
  sput (TyAnn_Mono        ) = sputWord8 1
  sput (TyAnn_Strictness a) = sputWord8 2  >> sput a
  sget = do tag <- sgetWord8
            case tag of
              0 -> return TyAnn_Empty
              1 -> return TyAnn_Mono
              2 -> liftM  TyAnn_Strictness sget

instance Binary TyVarCateg where
  put = putEnum8
  get = getEnum8

instance Serialize TyVarCateg where
  sput = sputPlain
  sget = sgetPlain

instance Serialize Pred where
  sput (Pred_Class  a  ) = sputWord8 0 >> sput a
  sput (Pred_Pred   a  ) = sputWord8 1 >> sput a
  sput (Pred_Lacks  a b) = sputWord8 2 >> sput a >> sput b
  sput (Pred_Arrow  a b) = sputWord8 3 >> sput a >> sput b
  sput (Pred_Eq     a b) = sputWord8 4 >> sput a >> sput b
  sput (Pred_Var    a  ) = sputWord8 5 >> sput a
  sput (Pred_Preds  a  ) = sputWord8 6 >> sput a
  sget = do tag <- sgetWord8
            case tag of
              0 -> liftM  Pred_Class   sget
              1 -> liftM  Pred_Pred    sget
              2 -> liftM2 Pred_Lacks   sget sget
              3 -> liftM2 Pred_Arrow   sget sget
              4 -> liftM2 Pred_Eq      sget sget
              5 -> liftM  Pred_Var     sget
              6 -> liftM  Pred_Preds   sget

instance Serialize Label where
  sput (Label_Lab  a) = sputWord8 0 >> sput a
  sput (Label_Var  a) = sputWord8 1 >> sput a
  sget = do tag <- sgetWord8
            case tag of
              0 -> liftM  Label_Lab   sget
              1 -> liftM  Label_Var   sget

instance Serialize PredSeq where
  sput (PredSeq_Nil          ) = sputWord8 0
  sput (PredSeq_Cons  a b    ) = sputWord8 1  >> sput a >> sput b
  sput (PredSeq_Var   a      ) = sputWord8 2  >> sput a
  sget = do tag <- sgetWord8
            case tag of
              0  -> return PredSeq_Nil
              1  -> liftM2 PredSeq_Cons  sget sget
              2  -> liftM  PredSeq_Var   sget

{-
instance Binary PredSeq where
  put = putList (PredSeq_Nil ==) (\(PredSeq_Cons a b) -> (a,b))
  get = getList PredSeq_Nil PredSeq_Cons
-}

instance Serialize CHRPredOcc where
  -- Range info is stripped on the fly
  sput (CHRPredOcc a b _) = sput a >> sput b
  -- Range info is stripped on the fly
  sget = liftM2 (\a b -> CHRPredOcc a b emptyRange) sget sget

instance Serialize Impls where
  sput (Impls_Nil             ) = sputWord8 0
  sput (Impls_Tail a b        ) = sputWord8 1  >> sput a >> sput b
  sput (Impls_Cons a b c d e f) = sputWord8 2  >> sput a >> sput b >> sput c >> sput d >> sput e >> sput f
  sget = do tag <- sgetWord8
            case tag of
              0  -> return Impls_Nil
              1  -> liftM2 Impls_Tail  sget sget
              2  ->
                    liftM6 Impls_Cons  sget sget sget sget sget sget


-- Impls -------------------------------------------------------
data Impls = Impls_Tail {iv_Impls_Tail :: !(ImplsVarId),proveOccs_Impls_Tail :: !(([ImplsProveOcc]))}
           | Impls_Cons {iv_Impls_Cons :: !(ImplsVarId),pr_Impls_Cons :: !(Pred),pv_Impls_Cons :: !(PredOccId),prange_Impls_Cons :: !(Range),proveOccs_Impls_Cons :: !(([ImplsProveOcc])),tl_Impls_Cons :: !(Impls)}
           | Impls_Nil {}
           deriving ( Data,Eq,Ord,Show,Typeable)
-- Label -------------------------------------------------------
data Label = Label_Lab {nm_Label_Lab :: !(HsName)}
           | Label_Var {lv_Label_Var :: !(LabelVarId)}
           deriving ( Data,Eq,Ord,Show,Typeable)
-- LabelAGItf --------------------------------------------------
data LabelAGItf = LabelAGItf_AGItf {lab_LabelAGItf_AGItf :: !(Label)}
                deriving ( Data,Eq,Ord,Show,Typeable)
-- Pred --------------------------------------------------------
data Pred = Pred_Class {ty_Pred_Class :: !(Ty)}
          | Pred_Pred {ty_Pred_Pred :: !(Ty)}
          | Pred_Lacks {ty_Pred_Lacks :: !(Ty),lab_Pred_Lacks :: !(Label)}
          | Pred_Arrow {args_Pred_Arrow :: !(PredSeq),res_Pred_Arrow :: !(Pred)}
          | Pred_Eq {tyL_Pred_Eq :: !(Ty),tyR_Pred_Eq :: !(Ty)}
          | Pred_Var {pv_Pred_Var :: !(TyVarId)}
          | Pred_Preds {seq_Pred_Preds :: !(PredSeq)}
          deriving ( Data,Eq,Ord,Show,Typeable)
-- PredSeq -----------------------------------------------------
data PredSeq = PredSeq_Cons {hd_PredSeq_Cons :: !(Pred),tl_PredSeq_Cons :: !(PredSeq)}
             | PredSeq_Nil {}
             | PredSeq_Var {av_PredSeq_Var :: !(TyVarId)}
             deriving ( Data,Eq,Ord,Show,Typeable)
-- Ty ----------------------------------------------------------
data Ty = Ty_Con {nm_Ty_Con :: !(HsName)}
        | Ty_App {func_Ty_App :: !(Ty),arg_Ty_App :: !(Ty)}
        | Ty_Ann {ann_Ty_Ann :: !(TyAnn),ty_Ty_Ann :: !(Ty)}
        | Ty_Dbg {info_Ty_Dbg :: !(String)}
        | Ty_Any {}
        | Ty_Var {tv_Ty_Var :: !(TyVarId),categ_Ty_Var :: !(TyVarCateg)}
        | Ty_TBind {qu_Ty_TBind :: !(TyQu),tv_Ty_TBind :: !(TyVarId),l1_Ty_TBind :: !(Ty),ty_Ty_TBind :: !(Ty)}
        | Ty_Ext {ty_Ty_Ext :: !(Ty),nm_Ty_Ext :: !(HsName),extTy_Ty_Ext :: !(Ty)}
        | Ty_Pred {pr_Ty_Pred :: !(Pred)}
        | Ty_Lam {tv_Ty_Lam :: !(TyVarId),ty_Ty_Lam :: !(Ty)}
        | Ty_Impls {impls_Ty_Impls :: !(Impls)}
        deriving ( Data,Eq,Ord,Show,Typeable)
-- TyAGItf -----------------------------------------------------
data TyAGItf = TyAGItf_AGItf {ty_TyAGItf_AGItf :: !(Ty)}
             deriving ( Data,Eq,Ord,Show,Typeable)
-- TyAnn -------------------------------------------------------
data TyAnn = TyAnn_Empty {}
           | TyAnn_Strictness {s_TyAnn_Strictness :: !(Strictness)}
           | TyAnn_Mono {}
           deriving ( Data,Eq,Ord,Show,Typeable)
-- TyQu --------------------------------------------------------
data TyQu = TyQu_Forall {mlev_TyQu_Forall :: !(MetaLev)}
          | TyQu_Exists {mlev_TyQu_Exists :: !(MetaLev)}
          | TyQu_Plain {mlev_TyQu_Plain :: !(MetaLev)}
          deriving ( Data,Eq,Ord,Show,Typeable)
-- TyVarCateg --------------------------------------------------
data TyVarCateg = TyVarCateg_Plain {}
                | TyVarCateg_Fixed {}
                | TyVarCateg_Meta {}
                deriving ( Data,Enum,Eq,Ord,Show,Typeable)