content: {-+
  This module defines some basic type checking functions, and some utility
  functions, notably functions for type checking applications (#tapp#) and
  identifiers (#inst# et al), introducing fresh type/kind variables,
  recording constraints on types/kinds and instantiating type schemes.
  -}
  module TiUtil where
  import TiMonad
  import TiTypes
  import TiSolve(TypeConstraint(..))
  import TiNames(ValueId,TypeVar,dictName,dictName')
  import TiClasses
  import TiKinds(KindConstraint(..))
  import TiFresh
  import HasBaseStruct
  import HsConstants(mod_Prelude,tuple)
  import BaseSyntax(srcLoc,TI(..))
  import TypedIds(NameSpace(..))
  import PrettyPrint hiding (var)
  import MUtils
  
  --import IOExts(trace) -- debug
  
  -- How to type check applications:
  -- tapp :: HasCoreSyntax e => TI (Typed e) -> TI (Typed e) -> TI (Typed e)
  fun `tapp` arg =
    do (f:>:tf) <- fun
       (a:>:ta) <- arg
       r <- appt tf ta
       f `app` a >: r
   where
      -- First case is an optional optimization
      appt (Typ (HsTyFun fa fr)) ta = do fa =:= ta
  				       return fr
      appt tf ta = do r <- tfresh
  	            tf =:= ta `hsTyFun` r
  		    return r
  
  --typedTuple :: HasCoreSyntax e => [Typed e] -> Typed e
  typedTuple ets =
      do t <- tupleType ts
         TiClasses.tuple es>:t
    where es:>:ts = unzipTyped ets
  
  --tcList :: HasCoreSyntax e => [Typed e] -> TI (Typed e)
  tcList ets =
    do let es:>:ts = unzipTyped ets
       t <- allSame ts
       listType <- getListType
       list es >: listType t
  
  tupleType ts =
     do t <- prelTypeName (HsConstants.tuple (length ts-1))
        return $ foldl hsTyApp (hsTyId t) ts
  
  getListType = hsTyApp . hsTyId # prelTypeName "[]"
  getBoolType = hsTyId # prelTypeName "Bool"
  
  allSame [] = tfresh
  allSame (t:ts) = mapM_ (t=:=) ts >> return t
  
  stdValue = stdName ValueNames
  stdType  = stdName ClassOrTypeNames
  stdClass = stdType
  
  prelValue     = stdValue . (,) mod_Prelude
  prelTypeName  = stdType  . (,) mod_Prelude
  prelClassName = prelTypeName
  prelTy n = hsTyId # prelTypeName n
  
  instStd = inst @@ stdValue
  instStd_srcloc s = inst_srcloc s @@ stdValue
  instPrel = inst @@ prelValue
  instPrel_srcloc s = inst_srcloc s @@ prelValue
  
  --inst :: HasCoreSyntax i e => HsIdentI i -> TiMonad.TI i (Typed i e)
  inst x = inst_loc' Nothing x
  inst_loc x = inst_loc' (Just (srcLoc x)) x
  inst_srcloc s = inst_loc' (Just s)
  
  inst_loc' s x =
    do sc@(Forall ags gs qt) <- sch x
       vs <- freshvars gs
       let ctx:=> t = freshen' vs (tdom gs) qt
       ds <- newdicts s ctx
       foldl1 app (spec x sc (map tyvar vs):map var ds) >: t
  
  inst_field f =
    do ctx:=>t <- instsch f
       ds <- newdicts Nothing ctx -- use srcLoc f!!
       return t -- hmm
  
  instsch f = sinst =<< sch f
  sinst (Forall ags gs qt) =
    do vs <- freshvars gs
       return (freshen' vs (tdom gs) qt)
  
  freshvars gs =
      do vs <- freshlist (length gs)
         addvars (zipTyped (vs:>:ks))
         return vs
    where
      vs0:>:ks = unzipTyped gs
  
  freshInst :: (TypeVar i,Fresh i,ValueId i)
            => Scheme i -> TiClasses.TI i ([Typing i (Pred i)],Type i)
  freshInst (Forall ags gs qt) =
    do ctx:=>t <- freshen (tdom gs) qt
       ds <- map dictName # freshlist (length ctx)
       return (zipTyped ((ds{-::[QId]-}):>:ctx),t)
  
  newdicts s ds = mapM (newdict s) ds
  newdict s pred = do d <- flip dictName' s # fresh
  	            addinst (d:>:pred)
  		    return d
  
  {-
  freshdicts ctx =
    do idns <- map dictName # freshlist (length ctx)
       return (zipWith (:>:) idns ctx)
  -}
  
  freshen gs t =
    do vs <- freshlist (length gs)
       return (freshen' vs gs t)
  
  freshen' vs gs t = apply s t
    where s = S [(g,tyvar v) | (g,v) <- zip gs vs]
  
  
  allfresh t = freshen (tv t) t
  
  varinst x =
    do Forall [] [] ([] :=> t) <- sch (HsVar x)
       return t
  
  
  infix 4 =:=,=*=
  t1 =:= t2 = constrain (t1:=:t2)
  k1 =*= k2 = constrain (k1:=*k2)
  
  addinst = constrain . Inst
  addkinst ki = do --trace (pp $ "addkinst"<+>ki) $ return ()
                   constrain (KInst ki)
  
  -- Introduce new types of kind *:
  tintro xs = do ts <- freshlist (length xs)
  	       addtypes ts
  	       return (zipTyped (xs:>:ts))
  
  -- Introduce monomorphic type schemes for types of kind *:
  schintro xs = map (fmap mono) # tintro xs
  
  -- Introduce new kind variables:
  kintro xs = do ts <- freshlist (length xs)
  	       return (zipTyped (xs:>:ts))
  
  tfresh = do t <- fresh
  	    addtype t
  	    return t
  
  addvars = mapM_ (addkinst.emap tyvar)
  addtypes ts = mapM_ addtype ts
  addtype t = addkinst (t:>:kstar)
  