content: -- $Id: BaseTypeCheckRec.hs,v 1.2 2001/09/29 00:08:23 diatchki Exp $
  
  module BaseTypeCheckRec where
  
  import BaseSyntaxStruct
  import TypeGenerics
  import List(nub)
  
  --------------------------------------------------------------------
  
  
  type Type a   = U a Kind T
  type NGV a    = [(HsName, U a Kind T)]
  type Env a    = [(HsName, Scheme Kind (U a Kind T))]
  type Genfun a = String -> Im a Error HsName
  type Alt      = HsAlt HsDecl HsExp HsPat
  type Stmt     = HsStmt HsDecl HsExp HsPat
  
  
  type EnvNew a = [Assump HsName Kind (U a Kind T)]
  
  data GEnv a = GEnv [(HsName,Class a)] (NGV a) [Assump HsName Kind (U a Kind T)]
  
  data Class a = Class HsName [Class a] [Inst a] 
  type Inst a  = ([Pred (U a Kind T)], (Pred (U a Kind T)))
  
  name  (GEnv cs ngv ass) x = let Class nm sup inst = look cs x in nm
  super (GEnv cs ngv ass) x = let Class nm sup inst = look cs x in sup
  insts (GEnv cs ngv ass) x = let Class nm sup inst = look cs x in ass 
  
  
  ------------------------------------------------------------------------
  -- Instance declaration to make the T functor from HsSyn.hs appropriate
  -- for doing type checking ala Hmx.hs
  
  instance G T where
    seqG = seqT
    mapG = mapT
    accG = accT
    
  instance Name T HsName where
    isName (HsTyVar s) = Just s
    isName _ = Nothing
    fromName s = HsTyVar s
    
  instance Gensym a HsName where
    newGensym  =
      do { seed <- newRef (1::Int)
         ; let gensym s = do { n <- readVar seed
                             ; writeVar seed (n+1)
                             ; return (UnQual (s ++ (show n)))
                             }
           in return gensym
         } 
         
    gensym s = do { n <- nextN   
                  ; return (UnQual (s ++ (show n)))
                  }
  
  data Error 
      = MatchError String (Vis T) (Vis T)
      | KErr String (Vis K) (Vis K)   
     
  instance TypeError Error T Kind where 
    hmxError s x y = 
      do { (nms,[x',y']) <- visible (generic []) [x,y]
         ; raise (MatchError s x' y')
         }
  
  -----------------------------------------------------------
  
  type NGVars a = [(HsName,U a Kind T)]
  
  emptyNGVars :: NGVars a
  emptyNGVars = []
  
  extendNGVars :: HsName -> U a Kind T -> NGVars a -> NGVars a
  extendNGVars s t ngvars = (s,t):ngvars
  
  generic :: NGVars a -> U a Kind T -> Im a e Bool 
  generic ngvars v = do { b <- occursInList v ngvars; return (not b) }
       where occursInList v l =
              do { (TVar v') <- prune v
                 ; bools <- mapM (\ (a,b) -> occursIn v' b) l
                 ; return (or bools)
                 }
         
  --------- Show Instances ----------------------------------
                               
  instance Show(U a k T) where 
    showsPrec n (S x) = shows x
    showsPrec n (TGen m) = showString "%" . shows m
    showsPrec n (TVar _) = showString "?"
  
  instance Show(Vis T) where 
    showsPrec n (VN a) = showString a
    showsPrec n (VS x) = shows x  
    
  
  instance Show a => Show(Pred a) where
    show (IsIn n ts) = "(" ++ n ++ " " ++ (show ts) ++ ")"
  
  instance Show a => Show (Scheme Kind a) where
    show (Sch x p t) = "(all " ++ (show x) ++"." ++ (show p) ++ " => " ++ (show t) ++ ")"  
  
  
  ----------------------- Instantiate unification ------------------------------
  
  unifyShape unify ( x @ (S tx)) (y @ (S ty)) =
    case (tx,ty) of
     (HsTyFun x1 x2,HsTyFun y1 y2) ->
        do { xs <- unify x1 y1 
           ; ys <- unify x2 y2 
           ; return (xs++ys) }     
     (HsTyTuple xs,HsTyTuple ys) ->
        if (length xs) == (length ys)  
           then do { xss <- mapM (uncurry unify) (zip xs ys)
                   ; return (concat xss)
                   }
           else hmxError "TupleLengthMatch" x y
     (HsTyApp x1 x2,HsTyApp y1 y2) ->
        do { xs <- unify x1 y1 
           ; ys <- unify x2 y2 
           ; return (xs++ys) }   
     (HsTyVar n1,HsTyVar n2) ->
        if n1 == n2 
           then return []
           else hmxError "NameMatch" x y 
     (HsTyCon n1,HsTyCon n2) ->
        if n1 == n2 
           then return []
           else hmxError "NameMatch" x y          
     (tx,ty) -> hmxError "ShapeMatch"  x y
        
  
  unify :: (U a Kind T) -> (U a Kind T) ->  Im a Error [p]
  unify = unifier (hmxError "OccursCheck") unifyShape
       
       
  ------------------ Kind inference -----------------------
  data Sort = Sort
  type Knd a = U a Sort K
  
  instance G K where
    mapG = mapK
    seqG = seqK
    accG f = flip (accK f)
  
  instance TypeError Error K Sort where
    hmxError s x y = 
      do { (nms,[x',y']) <- visible (\ x -> return False) [x,y]
         ; raise (KErr s x' y')
         }
  
  unifyK unify ( x @ (S tx)) (y @ (S ty)) =
    case (tx,ty) of
     (Kstar,Kstar) -> return []
     (Kfun x1 x2,Kfun y1 y2) ->
        do { xs <- unify x1 y1 
           ; ys <- unify x2 y2 
           ; return (xs++ys) }   
     (tx,ty) -> hmxError "KindShapeMatch"  x y
        
  unifyKind :: (U a Sort K) -> (U a Sort K) ->  Im a Error [p]
  unifyKind = unifier (hmxError "OccursCheck") unifyK
  
  star = S Kstar 
  
  inferK :: (HsName -> U a Sort K) -> U a Sort K -> HsType -> Im a Error (U a Sort K)
  inferK env hint (Typ typ) =
    case typ of
      (HsTyFun x y) ->
         do { x' <- inferK env star x
            ; y' <- inferK env star y
            ; unifyKind hint star
            ; return hint
            }
      (HsTyTuple ts) ->
         do { sequence (map (inferK env star) ts)
            ; unifyKind hint star
            ; return star
            }
      (HsTyApp x y) ->
         do { a <- newVar Sort
            ; b <- newVar Sort
            ; x' <- inferK env (S(Kfun a hint)) x
            ; y' <- inferK env a y
            ; return hint
            }
      (HsTyVar nm) ->
         do { unifyKind hint (env nm)
            ; return hint
            }
      (HsTyCon nm) ->  
         do { unifyKind hint (env nm)
            ; return hint
            }
  
  kindOf :: (HsName -> U a Sort K) -> HsType -> Im a Error Kind
  kindOf envf x = do { hint <- newVar Sort
                     ; inferK envf hint x
                     ; k <- uaSortK_to_Kind hint
                     ; return k
                     }
         
  ----------------------------------------------------------------------------
  -- After Kind inference some of the Kind Vars may still be un-instantiated
  -- Since we do not have a "polymorphic" Kind system we must instantiate
  -- these Kind vars. We fix them to kind "Knd Kstar", and then turn the 
  -- resulting (U a Sort K)  thing into a "Kind" type.
  
  uaSortK_to_Kind :: (U a Sort K) -> Im a e Kind
  uaSortK_to_Kind (S x) = do { x' <- seqG(mapG uaSortK_to_Kind x); return (Knd x')}
  uaSortK_to_Kind (TGen m) = error "no TGen in kinds"
  uaSortK_to_Kind (t @ (TVar x)) = follow finish uaSortK_to_Kind t
      where finish :: (Tyvar a Sort K) -> Im a e Kind
            finish (Tyvar ref s) = do { writeVar ref (Just star)
                                      ; return (Knd Kstar) }
                   
       
  --------------- Environment function and types --------------------------
  
  
  extend f s t = (s,t) : f
  
  lambdaExt :: [(name,Scheme a c)] -> name -> c -> [(name,Scheme a c)]
  lambdaExt env vname vtyp = extend env vname (Sch [] [] vtyp)
  
  envf [] s = error ("variable not found: "++(show s)++"\n")
  envf ((x,t):m) s = if x==s then t else envf m s
  
  -------- Type constructors and types of literal constants ------------
  
  tArrow x y = S(HsTyFun x y)
  tTuple ts = S(HsTyTuple ts)
  tInteger = S(HsTyCon (UnQual "Integer"))
  tChar = S(HsTyCon (UnQual "Char"))
  tString = tlist tChar
  tRational = S(HsTyCon (UnQual "Rational"))
  tBool = S(HsTyCon (UnQual "Bool"))
  
  tStringHash = S(HsTyCon (UnQual "stringHash"))
  tCharHash = S(HsTyCon (UnQual "CharHash"))
  tIntHash = S(HsTyCon (UnQual "IntHash"))
  tRationalHash = S(HsTyCon (UnQual "RationalHash"))
  tlist x =  S(HsTyApp tlistCon x)
  tlistCon = (S(HsTyCon (UnQual "[]")))
  
  tcode x =  S(HsTyApp tcodeCon x)
  tcodeCon = (S(HsTyCon (UnQual "Code")))
  
  litTyp (HsInt _)        = tInteger
  litTyp (HsChar _)       = tChar
  litTyp (HsString _)     = tString
  litTyp (HsFrac _)       = tRational
  litTyp (HsCharPrim _)   = tCharHash
  litTyp (HsStringPrim _) = tStringHash
  litTyp (HsIntPrim _)    = tIntHash
  litTyp (HsFloatPrim _)  = tRationalHash
  litTyp (HsDoublePrim _) = tRationalHash
  
  ------------------------ Predefined Class predicates ----------------
  
  num x = IsIn "Num" [x] 
  monad x = IsIn "Monad" [x]
  enum x = IsIn "Enum" [x]
  
  -------------------------------------------------------------------------
  -- unArrow [p1,p2,p3] (t1 -> t2 -> t3 -> t4) ---> (t4,[(p1,t1),(p2,t2),(p3,t3)])
  
  unArrow :: [HsPat] -> Type a -> Im a Error (Type a,[(HsPat,Type a)])
  unArrow ps t = do { t' <- col t; flat ps t' }
    where flat (p:ps) (S(HsTyFun dom rng)) = 
            do { (t,ts) <- (flat ps rng) ; return (t,(p,dom) : ts) }
          flat [] t = return (t,[])
          flat (p:ps) t = error "Too many arguments to pattern"
  
  
  patExtTup [] env = return ([],[],[])
  patExtTup ((p,t):m) env = 
      do { (t1,e1,c1) <- patExt p t env
         ; (ts,e2,cs) <- patExtTup m env 
         ; return(t1:ts,e1++e2,c1 ++ cs)
         }
  
  patExtList []    elemtyp env cs = return (tlist elemtyp,[],cs)
  patExtList (p:m) elemtyp env cs = 
      do { (t1,e1,c1) <- patExt p elemtyp env
         ; (listOfelem,e2,cs) <- patExtList m elemtyp env c1
         ; return(listOfelem,e1 ++ e2,c1++cs)
         }
  
  
  patExt :: HsPat -> Type a -> Env a -> Im a Error (Type a,NGV a,[Pred (Type a)])
  patExt (Pat p) typ env =
    case p of
     (HsPVar name) -> return (typ,[(name,typ)],[])
     (HsPLit l) -> 
        do { let t = litTyp l
           ; cs <- unify t typ
           ; return (t,[],cs)
           }
     (HsPNeg x) -> error "whats this?"
     (HsPInfixApp x n y) -> patExt (Pat(HsPApp n [x,y])) typ env 
     (HsPApp nm ps) -> 
        do { (cs1 :=> ctyp) <- instan (envf env nm) 
           ; (t,patTypeList) <- unArrow ps ctyp
           ; cs2 <- unify t typ
           ; (ts2,env2,cs3) <- patExtTup patTypeList env 
           ; return (t,env2,cs1 ++ cs2 ++ cs3)
           }
     (HsPTuple ps) ->
        do { ts <- sequence (map (\ x -> (newVar kstar)) ps)
           ; cs2 <- unify (tTuple ts) typ
           ; (ts,ngv3,cs3) <- patExtTup (zip ps ts) env
           ; return (tTuple ts,ngv3,cs2 ++ cs3)
           }         
     (HsPList ps ) -> 
        do { elemtyp <- newVar kstar
           ; (listtyp,ngv2,cs) <- patExtList ps elemtyp env []
           ; cs2 <- unify listtyp (tlist elemtyp)
           ; return (listtyp,ngv2,cs ++ cs2)
           }        
     (HsPParen x) -> patExt x typ env
     (HsPRec n pairs) -> error "not yet"
     (HsPRecUpdate nm pairs) -> error "not yet"
     (HsPAsPat name x) ->
        do { (t,ngv1,cs1) <- patExt x typ env
           ; return (t,(name,t):ngv1,cs1)
           }
     (HsPWildCard) -> do { t <- newVar kstar ; return (t,[],[]) }
     (HsPIrrPat x) -> patExt x typ env
  
  inferPats :: [HsPat] -> NGV a -> Env a ->  
                 Im a Error ([Type a],NGV a,Env a,[Pred (Type a)])
  inferPats ps ngvars env =
    do { pairs <- sequence (map (\ p -> do { t <- newVar kstar; return (p,t) }) ps)
       ; (t1,ngv1,cs1) <- patExtTup pairs env
       ; return (t1,ngv1 ++ ngvars,g ngv1 env,cs1)
       }  where g [] env = env
                g ((v,t):more) env = lambdaExt (g more env) v t
    
  inferPat p ngvars env hint =
    do { (_,ngv1,cs1) <- patExt p hint env
       ; return (ngv1 ++ ngvars,g ngv1 env,cs1)
       }  where g [] env = env
                g ((v,t):more) env = lambdaExt (g more env) v t
      
  -------------------------------------------------------------
      
  
  infer :: Genfun a -> NGV a -> Env a -> Type a ->
              HsExp -> Im a Error (Type a,[Pred (Type a)])            
  infer gensym ngvars env hint (exp @ (Exp e)) =
    let check env hint x = infer gensym ngvars env hint x 
    in
    case e of
      HsVar nm -> 
        do { (cs :=> t) <- instan (envf env nm)
           ; cs2 <- unify t hint
           ; return (t,cs ++ cs2)
           }
      HsCon nm -> 
        do { (cs :=> t) <- instan (envf env nm)
           ; cs2 <- unify t hint
           ; return (t,cs++cs2)
           }
      HsLit n -> 
        do { let t = litTyp n
           ; cs <- unify t hint
           ; return (t,cs)
           }         
      HsInfixApp x f y -> check env hint (Exp(HsApp (Exp (HsApp f x)) y))
      HsApp f x ->
        do { xtyp <- newVar kstar
           ; let ftyp = tArrow xtyp hint   
           ; (_,cs2) <- check env xtyp x
           ; (_,cs3) <- check env ftyp f
           ; return (hint,cs2++cs3)
           }
      HsNegApp x ->
        do { (t,cs) <- check env hint x
           ; return (t,num t : cs)
           }
      HsLambda ps x ->
        do { (ptyps,ngv2,env2,cs) <- inferPats ps ngvars env
           ; result <- newVar kstar
             -- f [t1,t2,t3] r --> (t1 -> t2 -> t3 -> r)
           ; let f [] rng = rng
                 f (t:ts) rng = tArrow t (f ts rng)
           ; (_,cs2) <- infer gensym ngv2 env2 result x
           ; return (f ptyps result,cs ++ cs2)
           }  
      HsLet ds e -> 
        do { (ngv2,env2,cs2) <- inferDecls gensym ngvars env ds
           ; infer gensym  ngv2 env2 hint e
           }
      HsIf x y z -> 
        do { t <- newVar kstar
           ; (_,cs1) <- check env tBool x
           ; (_,cs2) <- check env t y
           ; (_,cs3) <- check env t z
           ; return (t,cs1 ++ cs2 ++ cs3)
           }    
      HsCase e alts -> 
        do { argtyp <- newVar kstar
           ; (ptyp,cs1) <- check env argtyp e
           ; csAll <- mapM (inferAlt gensym ngvars env ptyp hint) alts
           ; return (hint, cs1 ++ concat csAll)
           }
      HsDo stmt -> 
        do { mtyp <- newVar (karrow kstar kstar)
           ; let m x =  (S(HsTyApp mtyp x))
           ; a <- newVar kstar
           ; cs2 <- unify hint (m a)
           ; cs3 <- inferStmt gensym ngvars env mtyp (m a) False stmt
           ; return (hint,(monad mtyp) : cs2 ++ cs3)
           }
      HsTuple xs -> 
        do { pairs <- sequence (map (\ x -> do { t <- newVar kstar; return (t,x) }) xs)
           ; let tupletyp = tTuple(map fst pairs)
           ; cs1 <- unify hint tupletyp
           ; ts <- mapM (uncurry (check env)) pairs
           ; return (hint,foldr (\ (t,c) cs -> c ++ cs) cs1 ts)
           }
      HsList xs -> 
        do { elemtyp <- newVar kstar
           ; cs1 <- unify hint (tlist elemtyp)
           ; pairs <- mapM (check env elemtyp) xs
           ; return (hint,foldr (\ (t,c) cs -> c ++ cs) cs1 pairs)
           }
      HsParen x -> check env hint x
      HsRightSection oper arg ->  -- i.e.  (+ 3) }
        do { ltyp <- newVar kstar
           ; rtyp <- newVar kstar
           ; anstyp <- newVar kstar
           ; cs1 <- unify (tArrow ltyp anstyp) hint
           ; (_,cs2) <- check env (tArrow ltyp (tArrow rtyp anstyp)) oper
           ; (_,cs3) <- check env rtyp arg
           ; return (hint,cs1 ++ cs2 ++ cs3)
           }
      HsLeftSection arg oper ->  -- i.e. (3 +)
        do { ltyp <- newVar kstar
           ; rtyp <- newVar kstar
           ; anstyp <- newVar kstar
           ; cs1 <- unify (tArrow rtyp anstyp) hint
           ; (_,cs2) <- check env (tArrow ltyp (tArrow rtyp anstyp)) oper
           ; (_,cs3) <- check env ltyp arg
           ; return (hint,cs1 ++ cs2 ++ cs3)
           }
      HsRecConstr name fields -> error "not yet"
      HsRecUpdate arg fields -> error "not yet" 
      HsEnumFrom x ->                     -- [x ..] :: Enum a => [a]
        do { a <- newVar kstar
           ; cs1 <- unify hint (tlist a)
           ; (_,cs2) <- check env a x
           ; return (hint,(enum a) : cs1 ++ cs2)
           }
      HsEnumFromTo x y ->                 -- [x .. y] :: Enum a => a -> a -> [a]
        do { a <- newVar kstar
           ; cs0 <- unify hint (tlist a)
           ; (_,cs1) <- check env a x
           ; (_,cs2) <- check env a y
           ; return (hint,(enum a) : cs0 ++ cs1 ++ cs2)
           }
      HsEnumFromThen x y ->              -- [x, y ..] :  Enum a => a -> a -> [a] 
        do { a <- newVar kstar
           ; cs0 <- unify hint (tlist a)
           ; (_,cs1) <- check env a x
           ; (_,cs2) <- check env a y
           ; return (hint,(enum a) : cs0 ++ cs1 ++ cs2)
           }
      HsEnumFromThenTo x y z ->          -- [x,y .. z] :: Enum a => a -> a -> a -> [a] 
        do { a <- newVar kstar
           ; cs0 <- unify hint (tlist a)
           ; (_,cs1) <- check env a x
           ; (_,cs2) <- check env a y
           ; (_,cs3) <- check env a z
           ; return (hint,(enum a) : cs0 ++ cs1 ++ cs2 ++ cs3)
           }
      HsListComp stmt -> 
        do { let mtyp = tlistCon
           ; let m x = (S(HsTyApp mtyp x))
           ; a <- newVar kstar
           ; cs2 <- unify hint (m a)
           ; cs3 <- inferStmt gensym ngvars env mtyp a True stmt
           ; return (hint,cs2 ++ cs3)
           }
      HsExpTypeSig loc e qt -> 
        do { s <-  hsQual2Sch qt
           ; (cs1 :=> typ) <- instan s
           ; cs2 <- unify typ hint
           ; (_,cs3) <- check env typ e
           ; return (typ,cs1 ++ cs2 ++ cs3)
           }
      HsAsPat nm e -> error "pattern only"
      HsWildCard -> error "pattern only"
      HsIrrPat e -> error "pattern only"
      HsMetaBracket e ->  --  MetaHUGS extension <| exp |> 
        do { a <- newVar kstar
           ; cs1 <- unify hint (tcode a)
           ; (_,cs2) <- check env a e
           ; return (hint,cs1 ++ cs2)
           }
      HsMetaEscape e ->   --  MetaHUGS extansion ^exp 
        do { (_,cs1) <- check env (tcode hint) e
           ; return (hint,cs1)
           }
  
  
  ----------------------------------------------------------------------------------
  -- inferStmt is used to infer the type of both Do stmts and list comprehensions
  -- [ A | p <- e ; f ]  has the same structure as (do { P <- e; f ; A })
  -- but the type rules differ slightly for both "A" and "f". We've parameterized
  -- inferStmt to handle this
  
  inferStmt :: Genfun a -> NGV a -> Env a -> Type a -> Type a -> Bool ->
             Stmt -> Im a Error [Pred (Type a)]
  inferStmt gensym ngvars env mtyp lasttyp isListComp stmt = 
    let m x = (S(HsTyApp mtyp x)) in
    case stmt of
      HsGenerator p e next ->  --    p <- e ; next
        do { ptyp <- newVar kstar
           ; (_,cs2) <- infer gensym ngvars env (m ptyp) e
           ; (ngv2,env2,cs3) <- inferPat p ngvars env ptyp
           ; cs4 <- inferStmt gensym ngv2 env2 mtyp lasttyp isListComp next
           ; return (cs2 ++ cs3 ++ cs4)
           }        
      HsQualifier e next ->   --  e ; next
        do { typ <- if isListComp then return tBool else fmap m (newVar kstar)
           ; (_,cs2) <- infer gensym ngvars env typ e
           ; return cs2
           }
      HsLetStmt ds next ->   -- let ds ; next
        do { (ngv2,env2,cs2) <- inferDecls gensym ngvars env ds
           ; cs3 <- inferStmt gensym ngv2 env2 mtyp lasttyp isListComp next
           ; return (cs2 ++ cs3)
           }
      HsLast e -> do { (_,cs) <- infer gensym ngvars env lasttyp e; return cs }
  
   
  inferAlt :: Genfun a -> NGV a -> Env a -> Type a -> Type a ->
             Alt -> Im a Error [Pred (Type a)]
  inferAlt gensym ngvars env pathint bodyhint (HsAlt s p rhs ds) =
    do { (ngv2,env2,cs2) <- inferPat p ngvars env pathint
       ; (ngv3,env3,cs3) <- inferDecls gensym ngv2 env2 ds
       ; (_,cs4) <- 
            case rhs of
              (HsBody e) -> infer gensym ngv3 env3 bodyhint e
              (HsGuard ms) -> g ms
                  where g [] = return (bodyhint,[])
                        g ((s,guard,e):ws) =
                            do { (_,cs4) <- infer gensym ngv3 env3 tBool guard
                               ; (t,cs5) <- infer gensym ngv3 env3 bodyhint e
                               ; (_,cs6) <- g ws
                               ; return (t,cs4 ++ cs5 ++ cs6)
                               }
       ; return (cs2 ++ cs3 ++ cs4)
       }
  
  
           
  inferDecls :: Genfun a -> NGV a -> Env a -> 
              [HsDecl] -> Im a Error (NGV a,Env a,[Pred (Type a)])
  inferDecls gensym ngvars env ds = return (ngvars,env,[])            
  
   
  ---------------------------------------------------------------------
  -- The Parser produces HsQualType data structures, we must turn these
  -- into Scheme data structures, while doing to we should kind-check
  -- all the type information.
  
  hsQual2Sch (HsQualType preds x) = scheme preds x
  hsQual2Sch (HsUnQualType t) = scheme [] t
  
  scheme :: [(HsName,HsName)] -> HsType -> Im a Error (Scheme Kind (U a Kind T))
  scheme preds t = 
     do { newks <- sequence(map (const (newVar Sort)) names)
                -- A new Kind var for each of the free type variables in "t"
        ; let env = zip names newks -- Map each Type Var to its kind Var
        ; mainK <- kindOf (look env) t
        ; argKs <- sequence (map uaSortK_to_Kind newks)
        ; return (Sch argKs (map transPred preds) (trans sub t))
        }           
    where names = namesT t  -- All the free Type Variables in "t"
          sub = zipWith (\ t n -> (t,TGen n)) names [0..]
          trans sub (Typ (HsTyVar nm)) = look sub nm
          trans sub (Typ z) = (S(mapT (trans sub) z))
          transPred (cla,arg) = IsIn (show cla) [trans sub (Typ(HsTyVar arg))]
  
  