content: {-+
  This module defined various classes and auxiliary types that are used
  throughout the type checker.
  -}
  module TiClasses where
  import TiMonad(IM,KEnv)
  import TiSolve(TypeConstraint)
  import TiTypes
  import HsLiteral(HsLiteral)
  --import HasBaseStruct(hsIf)
  --import DefinedNames(DefinedNames)
  import TiKinds(KindConstraint)
  import TiInstanceDB(Instance)
  --import List(nub)
  import MUtils
  import AccList
  --import Substitute
  --import SrcLoc
  
  type TypedDecls i ds = Typing ds (DeclsType i)
  type TypedTopDecls i ds = Typing ds ([Instance i],DeclsType i)
  type DeclsType i = ([TAssump i],[Assump i])
  
  type TAssump i = Typing (HsIdentI i) (Kind,TypeInfo i)
  
  nilDeclsType = ([],[]) -- ::DeclsType i
  
  --(+++) :: DeclsType i->DeclsType i->DeclsType i
  (xs1,ys1)+++(xs2,ys2) = (xs1++xs2,ys1++ys2)
  concDeclsType = foldr (+++) nilDeclsType
  
  class AddDeclsType i d | d->i where
    addDeclsType :: DeclsType i -> d -> d
    rmDeclsType :: d -> d
  
    addDeclsType _ d = d
    rmDeclsType = id
  
  {-
  Although their syntax are different, and they are type checked differently,
  the base syntax uses *the same* type for, top level declarations,
  local declarations, declarations in class definitions and declarations
  in instance definitions. Obviously we can't use the same overloaded function
  for type checking all of them...
  -}
  type CheckDecls i s r = s -> TI i (TypedDecls i r)
  type CheckTopDecls i s r = s -> TI i (TypedTopDecls i r)
  type CheckInstDecls i s r = [Assump i] -> s -> TI i r
  
  class TypeCheckDecls i s r {-| s->r-} where
    tcTopDecls :: (s->s) -> CheckTopDecls i s r
    tcInstDecls :: CheckInstDecls i s r
     --,tcLocalDecls' --, tcClassDecls
  
    --tcLocalDecls' = tcTopDecls
  tcLocalDecls ds = fmap (snd.snd) # tcTopDecls id ds
     -- discard instance db and kind env
  
  class TypeCheckDecl i s r where
    tcDecl :: [Typed i (HsIdentI i)] -> s -> TI i r
  
  class CheckRecursion i d where checkRecursion :: [d] -> TI i ()
  
  type TI i = IM i (TypeConstraint i)
  type KI i = IM i KindConstraint
  class TypeCheck i s r {-| s->r-} where tc :: s -> TI i r
  class KindCheck i t r | t->r where kc :: t -> KI i r
  
  class DeclInfo i d | d->i where
    explicitlyTyped :: [Kinded (HsIdentI i)] -> [Typing (HsIdentI i) (TypeInfo i)] -> [Pred i] -> d -> DeclsType i
  --isTypeDecl :: d -> Bool
    isUnrestricted :: Bool -> d -> Bool
    keepAmbigTypes :: d -> Bool
  
    keepAmbigTypes d = False
  
  class HasMethodSigs ds where splitMethodSigs :: ds -> (ds,ds)
  {-
  class GetSigs i c tp ds | ds->i c tp where
    getSigs :: ds -> [(SrcLoc,[i],c,tp)]
  -}
  {-
  instance KindCheck t r=> KindCheck [t] [r] where
    kc = mapM kc
    
  instance (KindCheck t1 r1,
  	  KindCheck t2 r2) => KindCheck (t1,t2) (r1,r2) where
    kc (t1,t2) = (,) # kc t1 <# kc t2
  -}
  --instance TypeCheck i s r => TypeCheck i [s] [r] where tc = mapM tc
  
  class HasId i e | e->i where
    ident :: HsIdentI i -> e
    isId :: e -> Maybe (HsIdentI i)
  
  var x = ident (HsVar x)
  con c = ident (HsCon c)
  
  isVar e = do HsVar x <- isId e
  	     return x
  
  --class HasLit e where lit :: HsLiteral -> e
  
  class HasId i e => HasCoreSyntax i e | e->i where
    app :: e -> e -> e
    tuple,list :: [e] -> e
  --paren :: e -> e
  
  class HasTypeAnnot i e | e->i where
    typeAnnot :: e -> Type i -> e
    typeAnnot e t = e -- default: no decoration
  
  --typedIf t cnd thn els = typeAnnot (hsIf cnd thn els) t
  
  class HasCoreSyntax i e => HasTypeApp i e | e->i where
    spec :: HsIdentI i -> Scheme i -> [Type i] -> e
    spec x sc ts = ident x -- default: no decoration
  
  class HasAbstr i e | e->i where
    abstract :: [i] -> e -> e
  
  class (HasAbstr i s) => HasLocalDef i e s | s->e i where
    letvar :: Typing i (Type i) -> e -> s -> s
  {-
  smartLetvar x@(i:>:_) e =
      case isId e of
        Just _ -> esubst1 var e i
        _ -> letvar x e
  -}
  --letvar x e1 e2 = abstract [x] e2 `app` e1
  
  instance HasAbstr i e => HasAbstr i [e] where
    abstract = map . abstract
  
  instance HasLocalDef i e s => HasLocalDef i e [s] where
    letvar x e1 = map (letvar x e1)
  
  infixr 5 `consDef`
  class HasDef ds d | ds->d where
    nullDef :: ds -> Bool
    noDef :: ds
    consDef :: d -> ds -> ds
    appendDef :: ds -> ds -> ds
    filterDefs :: (d->Bool) -> ds -> ds
    toDefs :: [d] -> ds
  
    toDefs = foldr consDef noDef
  
  concatDefs ds = foldr appendDef noDef ds
  oneDef d = consDef d noDef
  
  class HasDefs ds d | ds->d where fromDefs :: ds -> [d]
  instance HasDefs [d] d where fromDefs = id
  
  --class Decorate s i where decorate :: i -> s -> s
  
  class EnvFrom ds env | ds->env where accEnv :: ds -> env -> env
  
  envFrom ds = accEnv ds nilDeclsType
  
  instance EnvFrom d env => EnvFrom [d] env where accEnv = accList accEnv
  