diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,31 @@
+Copyright (c) 2007,2008 Spencer Janssen
+Copyright (c) 2007,2008 Don Stewart
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions
+are met:
+
+1. Redistributions of source code must retain the above copyright
+   notice, this list of conditions and the following disclaimer.
+
+2. Redistributions in binary form must reproduce the above copyright
+   notice, this list of conditions and the following disclaimer in the
+   documentation and/or other materials provided with the distribution.
+
+3. Neither the name of the author nor the names of his contributors
+   may be used to endorse or promote products derived from this software
+   without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS OR
+IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+DISCLAIMED.  IN NO EVENT SHALL THE AUTHORS OR CONTRIBUTORS BE LIABLE FOR
+ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS
+OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)
+HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT,
+STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
+ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+POSSIBILITY OF SUCH DAMAGE.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,5 @@
+#!/usr/bin/runhaskell
+
+import Distribution.Simple
+
+main = defaultMainWithHooks defaultUserHooks
diff --git a/TypeIlluminator.cabal b/TypeIlluminator.cabal
new file mode 100644
--- /dev/null
+++ b/TypeIlluminator.cabal
@@ -0,0 +1,22 @@
+name:                TypeIlluminator
+version:             0.0
+synopsis:            TypeIlluminator is a prototype tool exploring debugging of type errors/
+description:         TypeIlluminator is a prototype tool implementing the ideas presented in the paper
+                     Compositional Explanation of Types and Algorithmic Debugging of Type Errors.
+                     It constructs the type explanation graph for programs written in a simple
+                     Haskell-like language and enables free navigation through the graph
+                     in various ways and algorithmic debugging.
+category:            Compilers/Interpreters
+license:             BSD3
+license-file:        LICENSE
+author:              Olaf Chitil
+maintainer:          Olaf Chitil <O.Chitil@kent.ac.uk>
+homepage:            http://www.cs.kent.ac.uk/people/staff/oc/TypeIlluminator/
+build-depends:       base, haskell98
+build-type:          Simple
+
+executable:          typeilluminator
+main-is:             TypeIlluminator.hs
+
+ghc-options:         -O2 -Wall -optl-Wl,-s
+ghc-prof-options:    -prof -auto-all
diff --git a/TypeIlluminator.hs b/TypeIlluminator.hs
new file mode 100644
--- /dev/null
+++ b/TypeIlluminator.hs
@@ -0,0 +1,1608 @@
+{-
+Compositional explanation of types and algorithmic debugging of type errors
+author: Olaf Chitil
+created: 22.02.2001
+
+Part of the code is derived from Mark Jones' Typing Haskell in Haskell
+
+`Typing Haskell in Haskell' is Copyright (c) Mark P Jones,
+and the Oregon Graduate Institute of Science and Technology,
+1999-2000, All rights reserved, and is distributed as
+free software under the following license.
+
+Redistribution and use in source and binary forms, with or
+without modification, are permitted provided that the following
+conditions are met:
+
+- Redistributions of source code must retain the above copyright
+notice, this list of conditions and the following disclaimer.
+
+- Redistributions in binary form must reproduce the above
+copyright notice, this list of conditions and the following
+disclaimer in the documentation and/or other materials provided
+with the distribution.
+
+- Neither name of the copyright holders nor the names of its
+contributors may be used to endorse or promote products derived
+from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND THE
+CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES,
+INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF
+MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDERS OR THE
+CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT
+NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
+LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
+CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT,
+STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF
+ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+-}
+
+module Main where
+
+import List (nub, (\\), intersect, union, partition)
+import Maybe (catMaybes,isNothing)
+import Char (isAlpha,digitToInt)
+import Monad (MonadPlus(..),msum,when)
+-- import Debug.Trace (trace)
+
+-----------------------------------------------------------------------------
+-- Conversion to String:
+-----------------------------------------------------------------------------
+
+maxIdLength :: Int
+maxIdLength = 15
+
+subWidth :: Int
+subWidth = 30
+
+fixWidth :: String -> String
+fixWidth s
+  | l < subWidth = s ++ replicate (subWidth-l) ' '
+  | otherwise     = take (subWidth-6) s ++ " ...  "
+  where
+  l = length s
+
+test :: Bool -> String -> String
+test b s = if b then s else ""
+
+pparens :: Bool -> String -> String
+pparens True x = '(': x ++ ")"
+pparens False x = x
+
+
+ppContext :: Int -> [Pred] -> String
+ppContext _ [] = ""
+ppContext n preds = "\nContext:" ++ replicate n ' ' ++ ppPreds preds
+
+
+ppStep :: Bool {- with fragment -} -> Bool {- with children -}
+       -> Typing -> [Typing] -> String
+ppStep f c tyg tygs =
+  (if not f && not c then ppSTyping tyg else ppTyping f tyg) ++
+    test (c && (not . null $ tygs)) ("\n  because" ++ ppTypings f tygs)
+
+ppTypings :: Bool {- with fragment -} -> [Typing] -> String
+ppTypings _ tygs@(TyExpr _ _ : _) =
+  test qual
+    ("\nContext:    " ++ concatMap (fixWidth . ppPreds . preds) tygs) ++
+  "\nExpression: " ++ concatMap (fixWidth . ppExpr False . exp) tygs ++
+  "\nType:       " ++ concatMap (fixWidth . ppType False . ty) tygs ++
+  ppMonoEnvs 5 (map env tygs)
+  where
+  exp (TyExpr e _) = e
+  preds (TyExpr _ (p :=> _)) = p
+  ty (TyExpr _ (_ :=> (_,t))) = t
+  env (TyExpr _ (_ :=> (e,_))) = e
+  qual = not . null . concatMap preds $ tygs
+ppTypings f tygs@(TyAlt _ _ : _) =
+  test f ("\nEquation:  " ++ concatMap (fixWidth . ppAlt . alt) tygs) ++
+  test qual ("\nContext:   " ++ concatMap (fixWidth . ppPreds . preds) tygs) ++
+  ppMonoEnvs 4 (map env tygs)
+  where
+  alt (TyAlt a _) = a
+  preds (TyAlt _ (p :=> _)) = p
+  env (TyAlt _ (_ :=> e)) = e
+  qual = not . null . concatMap preds $ tygs
+ppTypings f tygs@(TyDef _ _ : _) =
+  test f ("\nDefinition: " ++ concatMap (fixWidth . ppDef . def) tygs) ++
+  test qual
+    ("\nContext:    " ++ concatMap (fixWidth . ppPreds . preds) tygs) ++
+  ppMonoEnvs 5 (map env tygs)
+  where
+  def (TyDef a _) = a
+  preds (TyDef _ (p :=> _)) = p
+  env (TyDef _ (_ :=> e)) = e
+  qual = not . null . concatMap preds $ tygs
+ppTypings f tygs@(TyBindGroup _ _ : _) =
+  test f ("\nDefinitions: " ++ concatMap (fixWidth . ppBindGroup . bg) tygs) ++
+  test qual
+    ("\nContext:     " ++ concatMap (fixWidth . ppPreds . preds) tygs) ++
+  ppPolyEnvs 8 (map penv tygs) ++
+  ppMonoEnvs 8 (map env tygs)
+  where
+  bg (TyBindGroup b _) = b
+  preds (TyBindGroup _ (p :=> _)) = p
+  env (TyBindGroup _ (_ :=> (e,_))) = e
+  penv (TyBindGroup _ (_ :=> (_,p))) = p
+  qual = not . null . concatMap preds $ tygs
+ppTypings _ _ = error "ppTypings"
+
+ppEnv2 :: Int -> Int -> Int -> [(String,String)] -> String
+ppEnv2 l ind _ xs = concatMap line xs
+  where
+  line (i,t) = '\n' : replicate ind ' ' ++ fixLength l i ++ "  " ++ t
+
+ppMonoEnvs :: Int -> [MonoEnv] -> String
+ppMonoEnvs l envs
+  | all null envs = ""
+  | otherwise = "\nwith " ++ drop 6 (ppEnv2 l 5 maxIdLength (map line ids))
+  where
+  ids = foldr union [] . map dom $ envs
+  line i = (i,concatMap (fixWidth . ppMType i) envs)
+  ppMType i env = case find i env of
+                    Just ty -> ppType False ty
+                    Nothing -> ""
+
+ppPolyEnvs :: Int -> [PolyEnv] -> String
+ppPolyEnvs l envs
+  | all null envs = ""
+  | otherwise =
+      "\nDefining " ++ drop 10 (ppEnv2 l 9 maxIdLength (map line ids))
+  where
+  ids = foldr union [] . map dom $ envs
+  line i = (i,concatMap (fixWidth . ppMType i) envs)
+  ppMType i env =
+    case find i env of
+      Just (Tree (TyPolyVar polyTy) _) -> ppPolyType polyTy
+      Nothing -> ""
+
+ppSContextS :: [Pred] -> String
+ppSContextS preds = test (not . null $ preds) (ppPreds preds ++ " =>")
+
+ppSTyping :: Typing -> String
+ppSTyping (TyExpr expr (preds :=> (monoEnv,ty))) =
+  ppSContextS preds ++
+  "\n" ++ fixLength l e ++ " :: " ++ ppType False ty ++
+  ppSMonoEnv l monoEnv
+  where
+  l = 10 `max` length e
+  e = ppExpr False expr
+ppSTyping (TyAlt _ (preds :=> monoEnv)) =
+  ppSContextS preds ++
+  ppSMonoEnv 10 monoEnv
+ppSTyping (TyDef _ (preds :=> monoEnv)) =
+  ppSContextS preds ++
+  ppSMonoEnv 10 monoEnv
+ppSTyping (TyBindGroup _ (preds :=> (monoEnv,polyEnv))) =
+  ppSContextS preds ++
+  ppSPolyEnv 10 polyEnv ++
+  ppSMonoEnv 10 monoEnv
+ppSTyping tyg = ppTyping False tyg
+
+ppTyping :: Bool {- with fragment -} -> Typing -> String
+ppTyping _ (TyExpr expr (preds :=> (monoEnv,ty))) =
+  ppContext 4 preds ++
+  "\nExpression: " ++ ppExpr False expr ++
+  "\nType:       " ++ ppType False ty ++
+  ppMonoEnv monoEnv
+ppTyping f (TyAlt alt (preds :=> monoEnv)) =
+  test f ("\nEquation: " ++ ppAlt alt) ++
+  ppContext 2 preds ++
+  ppMonoEnv monoEnv
+ppTyping f (TyDef def (preds :=> monoEnv)) =
+  test f ("\nDefinition: " ++ ppDef def) ++
+  ppContext 4 preds ++
+  ppMonoEnv monoEnv
+ppTyping f (TyBindGroup bg (preds :=> (monoEnv,polyEnv))) =
+  test f ("\nDefinitions: " ++ ppBindGroup bg) ++
+  ppContext 5 preds ++
+  ppPolyEnv polyEnv ++ ppMonoEnv monoEnv
+ppTyping f (TyProgram _ polyEnv) =
+  "\nWhole Program" ++ test f (ppPolyEnv polyEnv)
+ppTyping _ (TyPolyVar (preds :=> (monoEnv,t))) =
+  "\nPolyVar: " ++
+  ppContext 1 preds ++
+  "\nType:    " ++ ppType False t ++
+  ppMonoEnv monoEnv
+ppTyping _ (TyUExpr msg expr) =
+  "\nError: " ++ msg ++ ("\nin expression: " ++ ppExpr False expr)
+ppTyping _ (TyUAlt msg alt) =
+  "\nError: " ++ msg ++ ("\nin equation: " ++ ppAlt alt)
+ppTyping _ (TyUDef msg def) =
+  "\nError: " ++ msg ++ ("\nin definition: " ++ ppDef def)
+ppTyping _ (TyUBindGroup msg bg) =
+  "\nError: " ++ msg ++ ("\nin definitions: " ++ ppBindGroup bg)
+ppTyping _ (TyUProgram msg _) =
+  "\nError: " ++ msg ++ ("\nin whole program.")
+
+ppKind :: Bool -> Kind -> String
+
+ppKind _ Star = "*"
+ppKind b (Kfun k1 k2) =
+  pparens b (ppKind (not b) k1 ++ "->" ++ ppKind False k2)
+
+ppPreds :: [Pred] -> String
+ppPreds [] = ""
+ppPreds preds = foldr1 (\x xs -> x ++ ", " ++ xs) . map ppPred $ preds
+
+ppPred :: Pred -> String
+ppPred (IsIn classId ty) = classId ++ " " ++ ppType True ty
+
+ppType :: Bool -> Type -> String
+
+ppType _ (TVar (Tyvar i _)) = i
+ppType _ (TCon (Tycon i _)) = i
+ppType _ (TAp (TCon (Tycon "[]" _)) t) = '[' : ppType False t ++ "]"
+ppType b (TAp (TAp (TCon (Tycon "(->)" _)) t1)  t2) =
+  pparens b $ ppType (not b) t1 ++ "->" ++ ppType False t2
+ppType b (TAp t1 t2) = pparens b $ ppType True t1 ++ ' ' : ppType True t2
+ppType _ (TGen n) = show n
+
+ppPolyType :: Qual (MonoEnv,Type) -> String
+ppPolyType (preds :=> (monoEnv,t)) =
+  test (not . null $ preds) (ppPreds preds ++ " => ") ++
+  ppType False t ++
+  test (not . null $ monoEnv)
+    (" | " ++
+     (foldr1 (\t s -> t ++ ", " ++ s) .
+      map (\(i :>: t) -> i ++ " :: " ++ ppType False t) $ monoEnv))
+
+ppSPolyEnv :: Int -> PolyEnv -> String
+ppSPolyEnv l env = ppSEnv l (map pair env)
+  where
+  pair (i :>: Tree (TyPolyVar polyTy) _) =
+    (i,ppPolyType polyTy)
+
+ppPolyEnv :: PolyEnv -> String
+ppPolyEnv env =
+  "\nDefining " ++ drop 10 (ppEnv 9 maxIdLength (map pair env))
+  where
+  pair (i :>: Tree (TyPolyVar polyTy) _) =
+    (i,ppPolyType polyTy)
+
+
+ppSMonoEnv :: Int -> MonoEnv -> String
+ppSMonoEnv l env = ppSEnv l (map pair env)
+  where
+  pair (i :>: t) = (i,ppType False t)
+
+ppMonoEnv :: MonoEnv -> String
+ppMonoEnv env
+  | null env = ""
+  | otherwise = "\nwith " ++ drop 6 (ppEnv 5 maxIdLength (map pair env))
+  where
+  pair (i :>: t) = (i,ppType False t)
+
+
+ppSEnv :: Int -> [(String,String)] -> String
+ppSEnv l xs = concatMap line xs
+  where
+  line (i,t) = '\n' : fixLength l i ++ " :: " ++ t
+
+ppEnv :: Int -> Int -> [(String,String)] -> String
+ppEnv ind idl xs = concatMap line xs
+  where
+  line (i,t) = '\n' : replicate ind ' ' ++ fixLength l i ++ "  " ++ t
+  l = idl `min` (foldr max 0 . map length . map fst $ xs)
+
+
+fixLength :: Int -> String -> String
+
+fixLength l xs
+  | l > length xs = xs ++ replicate (l - length xs) ' '
+  | otherwise = take l xs
+
+
+ppLiteral :: Literal -> String
+
+ppLiteral (LitInt i) = show i
+ppLiteral (LitChar c) = [c]
+
+
+ppExpr :: Bool -> Expr -> String
+
+ppExpr _ (Var i) | not (isAlpha (head i)) = '(' : i ++ ")"
+ppExpr _ (Var i) = i
+ppExpr _ (Lit l) = ppLiteral l
+ppExpr _ (Const i)
+  | not (isAlpha (head i)) && head i /= '[' && head i /= '(' = '(' : i ++ ")"
+ppExpr _ (Const i) = i
+ppExpr b (Ap (Ap (Const i) e1) e2)
+  | not (isAlpha (head i)) =
+    pparens b $ ppExpr True e1 ++ ' ' : i ++ ' ' : ppExpr True e2
+ppExpr b (Ap (Ap (Var i) e1) e2)
+  | not (isAlpha (head i)) =
+    pparens b $ ppExpr True e1 ++ ' ' : i ++ ' ' : ppExpr True e2
+ppExpr b (Ap e1 e2) =
+  pparens b $ ppExpr True e1 ++ ' ' : ppExpr True e2
+
+ppAlt :: Alt -> String
+ppAlt (e1,e2) = ppExpr False e1 ++ " = " ++ ppExpr False e2
+
+ppDef :: Def -> String
+ppDef (alt:_) = ppAlt alt ++ " ..."
+
+
+ppBindGroup :: BindGroup -> String
+
+ppBindGroup (BG defs) = concatMap showVar boundVars
+  where
+  showVar i = i ++ " "
+  boundVars = nub . concatMap defVars $ defs
+
+ppProgram :: Program -> String
+ppProgram prog = concatMap ppBindGroup prog
+
+ppDef2 :: Def -> String
+ppDef2 alts = concatMap (('\n':) . ppAlt) alts
+
+ppBindGroup2 :: BindGroup -> String
+ppBindGroup2 (BG defs) = concatMap (('\n':) . ppDef2) defs
+
+ppProgram2 :: Program -> String
+ppProgram2 prog = concatMap ppBindGroup2 prog
+
+-----------------------------------------------------------------------------
+-- Tree:
+-----------------------------------------------------------------------------
+
+data Tree a = Tree a [Tree a]
+
+instance Types a => Types (Tree a) where
+  -- work only on root element
+  apply s (Tree e ts) = Tree (apply s e) ts
+  tv (Tree s _) = tv s
+
+data TreeCont a = Empty | TreeCont a [Tree a] (TreeCont a) [Tree a]
+
+treeElem :: Tree a -> a
+treeElem (Tree e _) = e
+
+-- dirty trick:
+
+instance Eq a => Eq (Tree a) where
+  Tree x _ == Tree y _ = x == y
+
+instance Eq (TreeCont a) where
+  _ == _ = True
+
+type TreePos a = (Tree a,TreeCont a)
+
+-- produce all children TreePoss
+children :: TreePos a -> [TreePos a]
+children (Tree x ts,cont) = map pick [0..(length ts - 1)]
+  where
+  pick n = (t,TreeCont x lts cont rts)
+    where
+    (lts,t:rts) = splitAt n ts
+
+-- parent and sibling TreePoss
+parentSibs :: TreePos a -> ([TreePos a],Maybe (TreePos a),[TreePos a])
+parentSibs (_,Empty) = ([],Nothing,[])
+parentSibs (t,TreeCont x lts cont rts) =
+  (map (build . addRts) . splits $ lts
+  ,Just (Tree x (lts++t:rts),cont)
+  ,map (build . addLts) . splits $ rts)
+  where
+  splits :: [a] -> [([a],a,[a])]
+  splits [] = []
+  splits (z:zs) = ([],z,zs) : map (\(us,v,ws)->(z:us,v,ws)) (splits zs)
+  addRts (ys,v,ws) = (ys,v,ws++t:rts)
+  addLts (ys,v,ws) = (lts++t:ys,v,ws)
+  build (ys,v,ws) = (v,TreeCont x ys cont ws)
+
+
+printStep :: Bool {- with fragment -} -> Bool {- with children -}
+          -> Bool {- only show poly vars -}
+          -> TreePos Typing -> IO ()
+printStep f c v tp@((Tree e _),_) = do
+  putStrLn $
+    ppStep f c (rename e) (map (rename . (\(Tree tyg _,_) -> tyg)) children)
+  where
+  children = getChildren v tp
+
+
+walkTree :: Tree Typing -> IO ()
+walkTree tree = walk True True True [] [] (tree,Empty)
+
+walk :: Bool {- with fragment -} -> Bool {- with children -}
+     -> Bool {- only show poly vars -} -> Oracle
+     -> [(Oracle,TreePos Typing)] -> TreePos Typing -> IO ()
+walk f c v oracle history tp@((Tree e _),_) = do
+  putStr "\n"
+  when errorLocated
+    (putStr (if v then "\nERROR LOCATED! Wrong definition of:"
+                  else "\nERROR LOCATED! Wrong program fragment:"))
+  printStep f c v tp
+  if errorLocated && v
+    then do
+      putStr "\nSwitch to detailed level of program fragments."
+      walk f c False oracle ((oracle,tp):history) (algNo False oracle tp)
+    else do
+      putStr (if f || c then "> "
+                        else "Is(are) intended type(s) an instance? (y/n) ")
+      choose
+  where
+  errorLocated = sourceOfError v oracle tp
+  children = getChildren v tp
+  choose = do
+    i <- getChar
+    case i of
+      '?' -> do
+               putStrLn $
+                 "\nManual navigation:" ++
+                 "\nu - up\nd - down\nl - left\nr - right" ++
+                 "\nb - back (undo)\ns - start" ++
+                 "\nnAlgorithmic debugging:" ++
+                 "\ny - intended type is an instance" ++
+                 "\nn - intended type is not an instance" ++
+                 "\nY - not sure about instance, continue as if it is" ++
+                 "\nN - not sure about instance, continue as if it is not" ++
+                 "\na - amnesia; forget all y/n answers" ++
+                 "\nnToggles:\nf - (don't) show program fragment" ++
+                 "\nc - (don't) show children" ++
+                 "\nv - show only polymorphic variables" ++
+                 "\n\nq - quit"
+               walk f c v oracle history tp
+      'b' -> if null history
+               then walk f c v oracle history tp
+               else walk f c v oracle' history' tp'
+             where
+             (oracle',tp'):history' = history
+      's' -> if null history
+               then walk f c v oracle history tp
+               else walk f c v oracle' [] tp'
+             where
+             (oracle',tp') = last history
+      'f' -> do
+               putStrLn
+                 (if f then "\nDon't show program fragment."
+                       else "\nShow program fragment.")
+               walk (not f) c v oracle history tp
+      'c' -> do
+               putStrLn
+                 (if c then "\nDon't show children." else "\nShow children.")
+               walk f (not c) v oracle history tp
+      'v' -> do
+               putStrLn
+                 (if v then "\nShow all typings."
+                       else "\nShow only typings of polymorphic variables.")
+               walk f c (not v) oracle history tp
+      'q' -> return ()
+      'u' -> ifPossible $ goUp v tp
+      'd' -> ifPossible $ goDown v tp
+      'l' -> ifPossible $ goLeft v tp
+      'r' -> ifPossible $ goRight v tp
+      'y' -> let oracle' = addToOracle (e,True) oracle
+             in walk f c v oracle' ((oracle',tp):history) (algYes v oracle' tp)
+      'n' -> let oracle' = addToOracle (e,False) oracle
+             in walk f c v oracle' ((oracle',tp):history) (algNo v oracle' tp)
+      'Y' -> walk f c v oracle ((oracle,tp):history) (algYes v oracle tp)
+      'N' -> walk f c v oracle ((oracle,tp):history) (algNo v oracle tp)
+      'a' -> do
+               putStrLn "\nAmnesia: forget all y/n answers."
+               walk f c v [] history tp
+      _ -> let n = digitToInt i in
+           if i >= '1' && i <= '9' && n <= length children
+             then walk f c v oracle ((oracle,tp):history) (children!!(n-1))
+             else choose
+  ifPossible :: Maybe (TreePos Typing) -> IO ()
+  ifPossible (Just tp') = walk f c v oracle ((oracle,tp):history) tp'
+  ifPossible Nothing   = choose
+
+getChildren :: Bool {- only polyvars -} -> TreePos Typing -> [TreePos Typing]
+getChildren True  = polyChildren
+getChildren False = children
+
+goLeft :: Bool {- only polyvars -} -> TreePos Typing -> Maybe (TreePos Typing)
+goLeft True tp = polyLeft tp
+goLeft False (t,TreeCont ec (l@(_:_)) cont' r) =
+  Just (last l,TreeCont ec (init l) cont' (t:r))
+goLeft _ _ = Nothing
+
+goRight :: Bool {- only polyvars -} -> TreePos Typing -> Maybe (TreePos Typing)
+goRight True tp = polyRight tp
+goRight False (t,TreeCont ec l cont' (t':ts')) =
+  Just (t',TreeCont ec (l++[t]) cont' ts')
+goRight _ _ = Nothing
+
+goDown :: Bool {- only polyvars -} -> TreePos Typing -> Maybe (TreePos Typing)
+goDown True tp = polyDown tp
+goDown False (Tree e (t:ts),cont) = Just (t,TreeCont e [] cont ts)
+goDown _ _ = Nothing
+
+goUp :: Bool {- only polyvars -} -> TreePos Typing -> Maybe (TreePos Typing)
+goUp True tp = polyUp tp
+goUp False (t,TreeCont ec left contcont right) =
+  Just (Tree ec (left++[t]++right), contcont)
+goUp _ _ = Nothing
+
+
+goNotTrueChild :: Bool {- only polyvars -}
+               -> Oracle -> TreePos Typing -> Maybe (TreePos Typing)
+goNotTrueChild v oracle tp =
+  if null notTrue then Nothing else Just (head notTrue)
+  where
+  children = getChildren v tp
+  notTrue = filter (\tp -> lookupOracle tp oracle /= Just True)
+    children
+
+
+algNo :: Bool {- only polyvars -}
+      -> Oracle -> TreePos Typing -> TreePos Typing
+algNo v oracle tp = case goNotTrueChild v oracle tp of
+                      Just tp' -> algNext v oracle tp'
+                      Nothing -> tp
+
+algYes :: Bool {- only polyvars -}
+       -> Oracle -> TreePos Typing -> TreePos Typing
+algYes v oracle tp = case goRight v tp of
+                       Just tp' -> algNext v oracle tp'
+                       Nothing -> case goUp v tp of
+                                    Just tp' -> algNext v oracle tp'
+                                    Nothing -> error "altNext: impossible"
+
+algNext :: Bool {- only polyvars -}
+        -> Oracle -> TreePos Typing -> TreePos Typing
+algNext v oracle tp =
+  case lookupOracle tp oracle of
+    Nothing -> tp
+    Just True -> algYes v oracle tp
+    Just False -> algNo v oracle tp
+
+sourceOfError :: Bool {- only polyvars -} -> Oracle -> TreePos Typing -> Bool
+sourceOfError v oracle tp =
+  lookupOracle tp oracle == Just False &&
+  isNothing (goNotTrueChild v oracle tp)
+
+
+-----------------------------------------------------------------------------
+-- Oracle:
+-----------------------------------------------------------------------------
+
+type Oracle = [(Typing,Bool)]  -- answers to y/n questions
+
+addToOracle :: (Typing,Bool) -> Oracle -> Oracle
+addToOracle (tyg,b) oracle = (tyg,b):oracle
+
+lookupOracle :: TreePos Typing -> Oracle -> Maybe Bool
+lookupOracle (Tree (TyExpr (Var _) _) [],_) _ = Just True  -- simple var
+lookupOracle (Tree tyg _,_) oracle
+  | untypable tyg = Just False
+  | otherwise = lookup tyg oracle
+
+-----------------------------------------------------------------------------
+-- Polymorphic variable children:
+-----------------------------------------------------------------------------
+
+polySelfChildren ::TreePos Typing -> [TreePos Typing]
+polySelfChildren = go . (:[])
+
+polyChildren :: TreePos Typing  -> [TreePos Typing]
+polyChildren = go . children
+
+-- recursively search for poly vars
+go :: [TreePos Typing] -> [TreePos Typing]
+go [] = []
+go (tp@(Tree (TyExpr (Var _) _) (_:_),_) : tps) = tp : go tps
+go (tp : tps) = go (children tp ++ go tps)
+
+
+polyParentSibs :: TreePos Typing
+               -> ([TreePos Typing],Maybe (TreePos Typing),[TreePos Typing])
+polyParentSibs tp =
+  case mtp of
+    Nothing -> ps
+    Just (Tree (TyExpr (Var _) _) (_:_),_) -> ps
+    Just (Tree tyg _,_) | untypable tyg -> ps
+    Just tp' -> let (ltps',mtp',rtps') = polyParentSibs tp'
+                in (ltps'++ltps,mtp',rtps++rtps')
+  where
+  ps@(ltps,mtp,rtps) = parentSibs tp
+
+polyUp :: TreePos Typing -> Maybe (TreePos Typing)
+polyUp tp = mtp
+  where
+  (_,mtp,_) = polyParentSibs tp
+
+polyDown :: TreePos Typing -> Maybe (TreePos Typing)
+polyDown tp = if null tps then Nothing else Just (head tps)
+  where
+  tps = polyChildren tp
+
+polyLeft :: TreePos Typing -> Maybe (TreePos Typing)
+polyLeft tp = if null polyLtps then Nothing else Just (last polyLtps)
+  where
+  polyLtps = concatMap polySelfChildren ltps
+  (ltps,_,_) = polyParentSibs tp
+
+polyRight :: TreePos Typing -> Maybe (TreePos Typing)
+polyRight tp = if null polyRtps then Nothing else Just (head polyRtps)
+  where
+  polyRtps = concatMap polySelfChildren rtps
+  (_,_,rtps) = polyParentSibs tp
+
+
+-----------------------------------------------------------------------------
+-- Derivation:
+-----------------------------------------------------------------------------
+
+data Typing = TyExpr Expr (Qual (MonoEnv,Type))
+            | TyAlt Alt (Qual MonoEnv)
+            | TyDef Def (Qual MonoEnv)
+            | TyBindGroup BindGroup (Qual (MonoEnv, PolyEnv))
+            | TyPolyVar (Qual (MonoEnv,Type))
+            | TyProgram Program PolyEnv
+            | TyUExpr String Expr -- String is error message
+            | TyUAlt String Alt
+            | TyUDef String Def
+            | TyUBindGroup String BindGroup
+            | TyUProgram String Program
+
+instance Eq Typing where
+  TyExpr e1 q1 == TyExpr e2 q2 = e1 == e2 && q1 == q2
+  TyAlt _ m1 == TyAlt _ m2 = m1 == m2
+  TyDef _ m1 == TyDef _ m2 = m1 == m2
+  TyAlt _ m1 == TyDef _ m2 = m1 == m2
+  TyDef _ m1 == TyAlt _ m2 = m1 == m2
+  TyBindGroup _ q1 == TyBindGroup _ q2 = q1 == q2
+  TyPolyVar q1 == TyPolyVar q2 = q1 == q2
+  TyProgram _ e1 == TyProgram _ e2 = e1 == e2
+  TyUExpr s1 e1 == TyUExpr s2 e2 = s1 == s2 && e1 == e2
+  TyUAlt s1 e1 == TyUAlt s2 e2 = s1 == s2 && e1 == e2
+  TyUDef s1 e1 == TyUDef s2 e2 = s1 == s2 && e1 == e2
+  TyUBindGroup s1 e1 == TyUBindGroup s2 e2 = s1 == s2 && e1 == e2
+  TyUProgram s1 e1 == TyUProgram s2 e2 = s1 == s2 && e1 == e2
+  _ == _ = False
+
+instance Types Typing where
+  apply s (TyExpr e qEnvTy) = TyExpr e (apply s qEnvTy)
+  apply s (TyAlt alt qEnv) = TyAlt alt (apply s qEnv)
+  apply s (TyDef def qEnv) = TyDef def (apply s qEnv)
+  apply s (TyBindGroup bg qEnvPolyEnv) =
+    TyBindGroup bg (apply s qEnvPolyEnv)
+  apply s (TyPolyVar qEnvTy) = TyPolyVar (apply s qEnvTy)
+  apply s (TyProgram prog qEnvPolyEnv) = TyProgram prog (apply s qEnvPolyEnv)
+  apply _ other = other
+
+  tv (TyExpr _ qEnvTy) = tv qEnvTy
+  tv (TyAlt _ qEnv) = tv qEnv
+  tv (TyDef _ qEnv) = tv qEnv
+  tv (TyBindGroup _ qEnvPolyEnv) = tv qEnvPolyEnv
+  tv (TyPolyVar qEnvTy) =  tv qEnvTy
+  tv (TyProgram _ qEnvPolyEnv) = tv qEnvPolyEnv
+  tv _ = []
+
+
+
+rename :: Types t => t -> t
+{-
+Rename all free type variables to a,b,c,...
+-}
+
+rename ty = apply freeSubst ty
+  where
+  freeTyVars = tv ty
+  freeKinds = map kind freeTyVars
+  newTyVars = map TVar $ zipWith Tyvar (map (:[]) ['a'..]) freeKinds
+  freeSubst = zip freeTyVars newTyVars
+
+
+untypable :: Typing -> Bool
+untypable (TyUExpr _ _) = True
+untypable (TyUAlt _ _) = True
+untypable (TyUDef _ _) = True
+untypable (TyUBindGroup _ _) = True
+untypable (TyUProgram _ _) = True
+untypable _ = False
+
+type Derivation = Tree Typing
+
+
+-----------------------------------------------------------------------------
+-- Id:          Error Monad
+-----------------------------------------------------------------------------
+
+data Error a = Correct a | Wrong String
+
+instance Monad Error where
+  return = Correct
+  (Correct a) >>= f = f a
+  (Wrong s) >>= _ = Wrong s
+  fail = Wrong
+
+instance MonadPlus Error where
+  mzero = Wrong "mzero"
+  (Wrong _) `mplus` y = y
+  x `mplus` _ = x
+
+error2TI :: Error a -> TI String a
+error2TI (Correct x) = return x
+error2TI (Wrong msg) = errorMsg msg
+
+-----------------------------------------------------------------------------
+-- Id:          Identifiers
+-----------------------------------------------------------------------------
+
+type Id  = String
+enumId  :: Int -> Id
+enumId n = "v" ++ show n
+
+-----------------------------------------------------------------------------
+-- Kind:                Kinds
+-----------------------------------------------------------------------------
+
+data Kind  = Star | Kfun Kind Kind
+             deriving (Eq,Show)
+
+
+-----------------------------------------------------------------------------
+-- Type:                Types
+-----------------------------------------------------------------------------
+
+data Type  = TVar Tyvar
+           | TCon Tycon
+           | TAp  Type Type
+           | TGen Int
+             deriving (Eq,Show)
+
+
+data Tyvar = Tyvar Id Kind
+             deriving (Eq,Show)
+
+data Tycon = Tycon Id Kind
+             deriving (Eq,Show)
+
+tUnit :: Type
+tUnit    = TCon (Tycon "()" Star)
+tChar :: Type
+tChar    = TCon (Tycon "Char" Star)
+tInt :: Type
+tInt     = TCon (Tycon "Int" Star)
+tInteger :: Type
+tInteger = TCon (Tycon "Integer" Star)
+tFloat :: Type
+tFloat   = TCon (Tycon "Float" Star)
+tDouble :: Type
+tDouble  = TCon (Tycon "Double" Star)
+
+tList :: Type
+tList    = TCon (Tycon "[]" (Kfun Star Star))
+tArrow :: Type
+tArrow   = TCon (Tycon "(->)" (Kfun Star (Kfun Star Star)))
+tTuple2 :: Type
+tTuple2  = TCon (Tycon "(,)" (Kfun Star (Kfun Star Star)))
+
+tString    :: Type
+tString     = list tChar
+
+infixr      4 `fn`
+fn         :: Type -> Type -> Type
+a `fn` b    = TAp (TAp tArrow a) b
+
+list       :: Type -> Type
+list t      = TAp tList t
+
+pair       :: Type -> Type -> Type
+pair a b    = TAp (TAp tTuple2 a) b
+
+
+class HasKind t where
+  kind :: t -> Kind
+instance HasKind Tyvar where
+  kind (Tyvar _ k) = k
+instance HasKind Tycon where
+  kind (Tycon _ k) = k
+instance HasKind Type where
+  kind (TCon tc) = kind tc
+  kind (TVar u)  = kind u
+  kind (TAp t _) = case (kind t) of
+                     (Kfun _ k) -> k
+
+-----------------------------------------------------------------------------
+-- Subst:       Substitutions
+-----------------------------------------------------------------------------
+
+type Subst  = [(Tyvar, Type)]
+
+nullSubst  :: Subst
+nullSubst   = []
+
+(+->)      :: Tyvar -> Type -> Subst
+u +-> t     = [(u, t)]
+
+class Types t where
+  apply :: Subst -> t -> t
+  tv    :: t -> [Tyvar]
+
+instance Types Type where
+  apply s (TVar u)  = case lookup u s of
+                       Just t  -> t
+                       Nothing -> TVar u
+  apply s (TAp l r) = TAp (apply s l) (apply s r)
+  apply _ t         = t
+
+  tv (TVar u)  = [u]
+  tv (TAp l r) = tv l `union` tv r
+  tv _         = []
+
+instance Types a => Types [a] where
+  apply s = map (apply s)
+  tv      = nub . concat . map tv
+
+instance (Types a, Types b) => Types (a,b) where
+  apply s (x,y) = (apply s x, apply s y)
+  tv (x,y)      = nub (tv x ++ tv y)
+
+
+infixr 4 @@
+(@@)       :: Subst -> Subst -> Subst
+s1 @@ s2    = [ (u, apply s1 t) | (u,t) <- s2 ] ++ s1
+
+
+merge      :: Monad m => Subst -> Subst -> m Subst
+merge s1 s2 = if agree then return (s1++s2) else fail "merge fails"
+ where agree = all (\v -> apply s1 (TVar v) == apply s2 (TVar v))
+                   (map fst s1 `intersect` map fst s2)
+
+
+-----------------------------------------------------------------------------
+-- Unify:       Unification
+-----------------------------------------------------------------------------
+
+mgu     :: Monad m => Type -> Type -> m Subst
+varBind :: Monad m => Tyvar -> Type -> m Subst
+
+mgu (TAp l r) (TAp l' r') = do s1 <- mgu l l'
+                               s2 <- mgu (apply s1 r)
+                                         (apply s1 r')
+                               return (s2 @@ s1)
+mgu (TVar u) t        = varBind u t
+mgu t (TVar u)        = varBind u t
+mgu (TCon tc1) (TCon tc2) | tc1==tc2 = return nullSubst
+mgu (TGen x) (TGen y) = if x /= y then error "TGen" else return nullSubst
+mgu _ _             = fail "different type constructors cannot be unified"
+
+varBind u t
+  | t == TVar u      = return nullSubst
+  | u `elem` tv t    = fail "unification would lead to infinite type"
+  | kind u == kind t = return (u +-> t)
+  | otherwise        = fail "kinds of types do not agree"
+
+
+match :: Monad m => Type -> Type -> m Subst
+match (TAp l r) (TAp l' r') = do sl <- match l l'
+                                 sr <- match r r'
+                                 merge sl sr
+match (TVar u)   t | kind u == kind t = return (u +-> t)
+match (TCon tc1) (TCon tc2)
+         | tc1==tc2         = return nullSubst
+match _ _                 = fail "types do not match"
+
+
+multiAssumptionEnv :: [MonoEnv] -> Env [Type]
+
+multiAssumptionEnv ass =
+  let vars = nub . concatMap dom $ ass
+  in map combineTypes vars
+
+  where
+  combineTypes :: Id -> Assump [Type]
+  combineTypes i = let scs = catMaybes . map (find i) $ ass in i :>: scs
+
+
+unifyMonoEnvs :: [Qual MonoEnv] -> Error (Qual MonoEnv)
+unifyMonoEnvs qEnvs = do
+  (env,s) <- unifyMonoEnvs' envs
+  return ((nub . apply s . concat $ contexts) :=> env)
+  where
+  (contexts,envs) = unzip . map (\(pred :=> env)->(pred,env)) $ qEnvs
+
+
+unifyMonoEnvs' :: [MonoEnv] -> Error (MonoEnv,Subst)
+unifyMonoEnvs' ass =
+  unifyMultiAssumptionEnv (multiAssumptionEnv ass)
+
+
+unifyMultiAssumptionEnv :: Env [Type] -> Error (MonoEnv,Subst)
+unifyMultiAssumptionEnv [] = return ([],nullSubst)
+unifyMultiAssumptionEnv ((i :>: scs) : as) = do
+  (sc,s) <- unifyTypes scs
+  (as',s') <- unifyMultiAssumptionEnv (apply s as)
+  return (apply s' (i :>: sc) : as',s'@@s)
+
+
+unifyTypings :: [Qual (MonoEnv,Type)] -> Error (Qual (MonoEnv,Type))
+unifyTypings qEnvTys = do
+  (t,s) <- unifyTypes ts
+  (monoEnv,s2) <- unifyMonoEnvs' (apply s monoEnvs)
+  return ((nub . apply (s2@@s) $ concat contexts) :=> (monoEnv,apply s2 t))
+  where
+  (contexts,monoEnvs,ts) =
+    unzip3 . map (\(preds :=> (monoEnv,ty)) -> (preds,monoEnv,ty)) $ qEnvTys
+
+
+unify2Types :: Type -> Type -> Error (Type,Subst)
+unify2Types t1 t2 = do
+  unifier <- mgu t1 t2
+  return (apply unifier t1,unifier)
+
+
+unifyTypes :: [Type] -> Error (Type,Subst)
+unifyTypes = unifySeq unify2Types
+
+
+unifySeq :: Types a => (a -> a -> Error (a,Subst))
+                    -> [a] -> Error (a,Subst)
+unifySeq _ [] = error "unifySeq of empty list"
+unifySeq _ [x] = return (x,nullSubst)
+unifySeq unify (x:y:ys) = do
+  (z,s) <- unify x y
+  (z',s') <- unifySeq unify (z : map (apply s) ys)
+  return (z',s'@@s)
+
+-----------------------------------------------------------------------------
+-- Pred:                Predicates
+-----------------------------------------------------------------------------
+
+data Qual t = [Pred] :=> t
+              deriving Eq
+
+data Pred   = IsIn Id Type
+              deriving Eq
+
+type Context = [Pred]
+
+instance Types t => Types (Qual t) where
+  apply s (ps :=> t) = apply s ps :=> apply s t
+  tv (ps :=> t)      = tv ps `union` tv t
+
+instance Types Pred where
+  apply s (IsIn c t) = IsIn c (apply s t)
+  tv (IsIn _ t)      = tv t
+
+mguPred, matchPred :: Monad m => Pred -> Pred -> m Subst
+mguPred             = lift mgu
+matchPred           = lift match
+
+lift :: Monad m => (Type -> Type -> m a) -> Pred -> Pred -> m a
+lift m (IsIn i t) (IsIn i' t')
+         | i == i'   = m t t'
+         | otherwise = fail "classes differ"
+
+type Class    = ([Id], [Inst])  -- superclasses and instances
+type Inst     = Qual Pred
+
+-----------------------------------------------------------------------------
+
+data ClassEnv = ClassEnv { classes  :: Id -> Error Class,
+                           defaults :: [Type] }
+
+super     :: ClassEnv -> Id -> [Id]
+super ce i = case classes ce i of Correct (is, _) -> is
+
+insts     :: ClassEnv -> Id -> [Inst]
+insts ce i = case classes ce i of Correct (_, its) -> its
+
+correct :: Error a -> Bool
+correct (Correct _) = True
+correct (Wrong _) = False
+
+modify       :: ClassEnv -> Id -> Class -> ClassEnv
+modify ce i c = ce{classes = \j -> if i==j then return c
+                                           else classes ce j}
+
+initialEnv :: ClassEnv
+initialEnv  = ClassEnv { classes  = \_ -> fail "class not defined",
+                         defaults = [tInteger, tDouble] }
+
+type EnvTransformer = ClassEnv -> Error ClassEnv
+
+infixr 5 <:>
+(<:>) :: EnvTransformer -> EnvTransformer -> EnvTransformer
+f <:> g = \ce -> do
+  ce' <- f ce
+  g ce'
+
+addClass                              :: Id -> [Id] -> EnvTransformer
+addClass i is ce
+ | correct (classes ce i)              = fail "class already defined"
+ | any (not . correct . classes ce) is = fail "superclass not defined"
+ | otherwise                           = return (modify ce i (is, []))
+
+addPreludeClasses :: EnvTransformer
+addPreludeClasses  = addCoreClasses <:> addNumClasses
+
+addCoreClasses ::   EnvTransformer
+addCoreClasses  =   addClass "Eq" []
+                <:> addClass "Ord" ["Eq"]
+                <:> addClass "Show" []
+                <:> addClass "Read" []
+                <:> addClass "Bounded" []
+                <:> addClass "Enum" []
+                <:> addClass "Functor" []
+                <:> addClass "Monad" []
+
+addNumClasses  ::   EnvTransformer
+addNumClasses   =   addClass "Num" ["Eq", "Show"]
+                <:> addClass "Real" ["Num", "Ord"]
+                <:> addClass "Fractional" ["Num"]
+                <:> addClass "Integral" ["Real", "Enum"]
+                <:> addClass "RealFrac" ["Real", "Fractional"]
+                <:> addClass "Floating" ["Fractional"]
+                <:> addClass "RealFloat" ["RealFrac", "Floating"]
+
+addInst                        :: [Pred] -> Pred -> EnvTransformer
+addInst ps p@(IsIn i _) ce
+ | not (correct (classes ce i)) = fail "no class for instance"
+ | any (overlap p) qs           = fail "overlapping instance"
+ | otherwise                    = return (modify ce i c)
+   where its = insts ce i
+         qs  = [ q | (_ :=> q) <- its ]
+         c   = (super ce i, (ps:=>p) : its)
+
+overlap       :: Pred -> Pred -> Bool
+overlap p q    = correct (mguPred p q)
+
+exampleInsts ::  EnvTransformer
+exampleInsts =   addPreludeClasses
+             <:> addInst [] (IsIn "Ord" tUnit)
+             <:> addInst [] (IsIn "Ord" tChar)
+             <:> addInst [] (IsIn "Ord" tInt)
+             <:> addInst [IsIn "Ord" (TVar (Tyvar "a" Star)),
+                          IsIn "Ord" (TVar (Tyvar "b" Star))]
+                         (IsIn "Ord" (pair (TVar (Tyvar "a" Star))
+                                           (TVar (Tyvar "b" Star))))
+
+-----------------------------------------------------------------------------
+
+bySuper :: ClassEnv -> Pred -> [Pred]
+bySuper ce p@(IsIn i t)
+ = p : concat [ bySuper ce (IsIn i' t) | i' <- super ce i ]
+
+byInst                   :: MonadPlus m => ClassEnv -> Pred -> m [Pred]
+byInst ce p@(IsIn i _)    = msum [ tryInst it | it <- insts ce i ]
+ where tryInst (ps :=> h) = do u <- matchPred h p
+                               return (map (apply u) ps)
+
+entail        :: ClassEnv -> [Pred] -> Pred -> Bool
+entail ce ps p = any (p `elem`) (map (bySuper ce) ps) ||
+                 case byInst ce p of
+                   Wrong _ -> False
+                   Correct qs -> all (entail ce ps) qs
+
+-----------------------------------------------------------------------------
+
+inHnf :: Pred -> Bool
+inHnf (IsIn _ t) = hnf t
+ where hnf (TVar _)  = True
+       hnf (TCon _) = False
+       hnf (TAp t _) = hnf t
+
+toHnfs :: Monad m => ClassEnv -> [Pred] -> m [Pred]
+toHnfs ce ps = do pss <- mapM (toHnf ce) ps
+                  return (concat pss)
+
+toHnf :: Monad m => ClassEnv -> Pred -> m [Pred]
+toHnf ce p | inHnf p   = return [p]
+           | otherwise = case byInst ce p of
+                           Nothing -> fail "context reduction"
+                           Just ps -> toHnfs ce ps
+
+simplify :: ClassEnv -> [Pred] -> [Pred]
+simplify ce = loop []
+ where loop rs []                            = rs
+       loop rs (p:ps) | entail ce (rs++ps) p = loop rs ps
+                      | otherwise            = loop (p:rs) ps
+
+reduce      :: [Pred] -> TI String [Pred]
+reduce ps = do
+  ce <- getClassEnv
+  qs <- error2TI $ toHnfs ce ps
+  return (simplify ce qs)
+
+scEntail        :: ClassEnv -> [Pred] -> Pred -> Bool
+scEntail ce ps p = any (p `elem`) (map (bySuper ce) ps)
+
+
+-----------------------------------------------------------------------------
+-- Environments:
+-----------------------------------------------------------------------------
+
+data Assump t = Id :>: t deriving (Eq,Show)
+
+type Env t = [Assump t]
+
+type MonoEnv = Env Type
+
+type PolyEnv = Env Derivation
+
+
+instance Types t => Types (Assump t) where
+  apply s (i :>: sc) = i :>: (apply s sc)
+  tv (_ :>: sc)      = tv sc
+
+dom :: Env t -> [Id]
+dom as = [ i | (i :>: _) <- as]
+
+without :: Env t -> [Id] -> Env t
+without as is = [ a | a@(i:>:_) <- as, i `notElem` is]
+
+find     :: Id -> Env t -> Maybe t
+find i as = headMaybe [ sc | (i':>:sc) <- as, i==i' ]
+
+headMaybe :: [a] -> Maybe a
+headMaybe [] = Nothing
+headMaybe (x:_) = Just x
+
+-----------------------------------------------------------------------------
+-- TIMonad:     Type inference monad
+-----------------------------------------------------------------------------
+
+newtype TI a b = TI (ClassEnv -> Int -> Either a (Int, b))
+
+instance Monad (TI a) where
+  return x   = TI (\_ n -> Right (n,x))
+  TI c >>= f = TI (\ce n ->
+                   case c ce n of
+                     Right (m,x) -> let TI fx = f x in fx ce m
+                     Left x      -> Left x)
+
+runTI      :: ClassEnv -> TI Derivation Derivation -> Derivation
+runTI ce (TI c) =
+  case c ce 0 of
+    Right (_,result) -> result
+    Left result      -> result
+
+
+newTVar    :: Kind -> TI a Type
+newTVar k   = TI (\_ n ->
+                  let v = Tyvar (enumId n) k
+                  in  Right (n+1, TVar v))
+
+getClassEnv :: TI a ClassEnv
+getClassEnv = TI (\ce n -> Right (n,ce))
+
+errorMsg :: String -> TI String a
+errorMsg msg = TI (\_ _ -> Left msg)
+
+errorDer :: Derivation -> TI Derivation a
+errorDer x = TI (\_ _ -> Left x)
+
+updateError :: (b -> c) -> TI b a -> TI c a
+updateError f (TI g) =
+  TI (\ce n -> case g ce n of
+                 Left b -> Left (f b)
+                 Right a -> Right a)
+
+-----------------------------------------------------------------------------
+-- TIMain:      Type Inference Algorithm
+-----------------------------------------------------------------------------
+-----------------------------------------------------------------------------
+-- Lit:         Literals
+-----------------------------------------------------------------------------
+
+data Literal = LitInt  Integer
+             | LitChar Char
+  deriving Eq
+
+tiLit :: Literal -> TI Derivation Derivation
+tiLit l@(LitChar _) = return $ Tree (TyExpr (Lit l) ([] :=> ([],tChar))) []
+tiLit l@(LitInt _)  = do
+  tvar <- newTVar Star
+  return $ Tree (TyExpr (Lit l) ([IsIn "Num" tvar] :=> ([],tvar))) []
+
+
+-----------------------------------------------------------------------------
+
+data Expr = Var   Id
+          | Lit   Literal
+          | Const Id
+          | Ap    Expr Expr
+          | Let   BindGroup Expr
+  deriving Eq
+
+infixl `Ap`
+
+
+substNewTyVars :: Typing -> TI a Typing
+
+substNewTyVars ty = do
+  let freeTyVars = tv ty
+      freeKinds = map kind freeTyVars
+  freeNew <- mapM newTVar freeKinds
+  let freeSubst = zip freeTyVars freeNew
+  return $ apply freeSubst ty
+
+
+
+tiExpr :: PolyEnv -> Expr -> TI Derivation Derivation
+
+tiExpr polyEnv e@(Var i)
+ = case find i polyEnv of
+     Just (Tree typing trees) -> do
+       TyPolyVar predMonoEnvTy <- substNewTyVars typing
+       return $ Tree (TyExpr e predMonoEnvTy) trees
+     Nothing -> do
+       t <- newTVar Star
+       return $ Tree (TyExpr e ([] :=> ([i :>: t],t))) []
+
+tiExpr polyEnv e@(Const i)
+ = case find i polyEnv of
+     Just (Tree typing _) -> do
+       TyPolyVar predMonoEnvTy <- substNewTyVars typing
+       return $ Tree (TyExpr e predMonoEnvTy) []
+     Nothing -> error "undefined data constructor"
+
+tiExpr _ (Lit l)
+ = tiLit l
+
+tiExpr polyEnv e@(Ap e1 e2) = do
+  d1@(Tree (TyExpr _ qty1) _) <- tiExpr polyEnv e1
+  d2@(Tree (TyExpr _ (pred2 :=> (monoEnv2,ty2))) _) <- tiExpr polyEnv e2
+  t <- newTVar Star
+  case unifyTypings [qty1,pred2 :=> (monoEnv2,ty2 `fn` t)] of
+    Correct (preds :=> (monoEnv,TAp (TAp _ _) tyRes)) ->
+      return $ Tree (TyExpr e (preds :=> (monoEnv,tyRes))) [d1,d2]
+    Wrong msg -> errorDer $ Tree (TyUExpr msg e) [d1,d2]
+
+tiExpr polyEnv e@(Let bg e1) = do
+  d1@(Tree (TyBindGroup _ (predBg :=> (usedEnvBg,defEnvBg))) _)
+    <- tiBindGroup polyEnv bg
+  d2@(Tree (TyExpr _ qtyE1@(_ :=> (_,tyE1))) _)
+    <- tiExpr (defEnvBg ++ polyEnv) e1
+  case unifyTypings [predBg :=> (usedEnvBg,tyE1),qtyE1] of
+    Correct qEnvTy ->
+      return $ Tree (TyExpr e qEnvTy) [d1,d2]
+    Wrong msg -> errorDer $ Tree (TyUExpr msg e) [d1,d2]
+
+-----------------------------------------------------------------------------
+
+type Alt = (Expr, Expr)
+
+tiAlt :: PolyEnv -> Alt -> TI Derivation Derivation
+tiAlt polyEnv (lhs,rhs) = do
+  let localVars = vars lhs \\ (defVars lhs)
+  let polyEnv' = polyEnv `without` localVars
+  d1@(Tree (TyExpr _ qTyLhs) _)
+    <- tiExpr polyEnv' lhs
+  d2@(Tree (TyExpr _ qTyRhs) _)
+    <- tiExpr polyEnv' rhs
+  case unifyTypings [qTyLhs,qTyRhs] of
+    Correct (preds :=> (usedEnv,_)) ->
+      return $ Tree (TyAlt (lhs,rhs)
+                      (preds :=> (usedEnv `without` localVars)))
+                    [d1,d2]
+    Wrong msg -> errorDer $ Tree (TyUAlt msg (lhs,rhs)) [d1,d2]
+
+
+
+type Def = [Alt]
+
+tiDef :: PolyEnv -> Def -> TI Derivation Derivation
+tiDef polyEnv alts = do
+  derivations <- mapM (tiAlt polyEnv) alts
+  let qUsedEnvs = map getQEnv $ derivations
+  case unifyMonoEnvs qUsedEnvs of
+    Correct (preds :=> usedEnv) ->
+      return $ Tree (TyDef alts (preds :=> usedEnv)) derivations
+    Wrong msg -> errorDer $ Tree (TyUDef msg alts) derivations
+  where
+  getQEnv (Tree (TyAlt _ qEnv) _ ) = qEnv
+
+
+
+vars :: Expr {-Pat-} -> [Id]
+
+vars (Var i) = [i]
+vars (Lit _) = []
+vars (Const _) = []
+vars (Ap e1 e2) = vars e1 ++ vars e2
+vars (Let _ _) = error "vars: pattern"
+
+
+class Define a where
+  defVars :: a -> [Id]
+
+instance Define Expr {- lhs of function def -} where
+  defVars (Var f) = [f]
+  defVars (Ap f _) = defVars f
+  defVars _ = error "defVars: not a pattern"
+
+instance Define a => Define (a,b) where
+  defVars (a,_) = defVars a
+
+instance Define a => Define [a] where
+  defVars = concatMap defVars
+
+
+-----------------------------------------------------------------------------
+-- Defaulting:
+-----------------------------------------------------------------------------
+
+split :: [Tyvar] -> [Tyvar] -> [Pred] -> TI String ([Pred], [Pred])
+split fs gs ps = do
+  ce <- getClassEnv
+  ps' <- reduce ps
+  let (ds, rs) = partition (all (`elem` fs) . tv) ps'
+  rs' <- error2TI $ defaultedPreds ce (fs++gs) rs
+  return (ds, rs \\ rs')
+
+type Ambiguity       = (Tyvar, [Pred])
+
+ambiguities         :: ClassEnv -> [Tyvar] -> [Pred] -> [Ambiguity]
+ambiguities _ vs ps = [ (v, filter (elem v . tv) ps) | v <- tv ps \\ vs ]
+
+numClasses :: [Id]
+numClasses  = ["Num", "Integral", "Floating", "Fractional",
+               "Real", "RealFloat", "RealFrac"]
+
+stdClasses :: [Id]
+stdClasses  = ["Eq", "Ord", "Show", "Read", "Bounded", "Enum", "Ix",
+               "Functor", "Monad", "MonadPlus"] ++ numClasses
+
+candidates           :: ClassEnv -> Ambiguity -> [Type]
+candidates ce (v, qs) = [ t' | let is = [ i | IsIn i _ <- qs ]
+                                   ts = [ t | IsIn _ t <- qs ],
+                               all ((TVar v)==) ts,
+                               any (`elem` numClasses) is,
+                               all (`elem` stdClasses) is,
+                               t' <- defaults ce,
+                               all (entail ce []) [ IsIn i t' | i <- is ] ]
+
+withDefaults :: Monad m => ([Ambiguity] -> [Type] -> a)
+                  -> ClassEnv -> [Tyvar] -> [Pred] -> m a
+withDefaults f ce vs ps
+    | any null tss  = fail "cannot resolve ambiguity"
+    | otherwise     = return (f vps (map head tss))
+      where vps = ambiguities ce vs ps
+            tss = map (candidates ce) vps
+
+defaultedPreds :: Monad m => ClassEnv -> [Tyvar] -> [Pred] -> m [Pred]
+defaultedPreds  = withDefaults (\vps _ -> concat (map snd vps))
+
+defaultSubst   :: [Tyvar] -> [Pred] -> PolyEnv -> TI String PolyEnv
+defaultSubst vs ps env = do
+  ce <- getClassEnv
+  s <- withDefaults (\vps ts -> zip (map fst vps) ts) ce vs ps
+  return $ apply s env
+
+-----------------------------------------------------------------------------
+-- BindGroup
+-----------------------------------------------------------------------------
+
+newtype BindGroup = BG [Def] deriving Eq
+
+
+tiBindGroup :: PolyEnv -> BindGroup -> TI Derivation Derivation
+tiBindGroup polyEnv bg@(BG defs) = do
+  let boundVars = nub . concatMap defVars $ defs
+  derivations <- mapM (tiDef (polyEnv `without` boundVars)) defs
+  let qEnvs = map getQEnv derivations
+  case unifyMonoEnvs qEnvs of
+    Wrong msg -> errorDer $ Tree (TyUBindGroup msg bg) derivations
+    Correct (defsPreds :=> occEnv) -> do
+      let (defsEnv,usedEnv) =
+            partition (\(x :>: _) -> x `elem` boundVars) occEnv
+          usedEnvTyVars = tv usedEnv
+          defsTyVars = [tv ty | (_ :>: ty) <- defsEnv]
+      (ds,rs) <- updateError (\s -> (Tree (TyUBindGroup s bg) derivations))
+                  (split usedEnvTyVars (foldr1 intersect defsTyVars) defsPreds)
+      let (deferredPreds,retainedPreds)
+             | restricted bg = (ds++rs,[])
+             | otherwise     = (ds,rs)
+
+      return $
+        Tree (TyBindGroup bg (deferredPreds :=>
+               (usedEnv
+               ,[ f :>: Tree (TyPolyVar
+                               (retainedPreds :=>
+                                 (reduceMonoEnv (tv ty) usedEnv,ty)))
+                          derivations
+                | f :>: ty <- defsEnv ])))
+          derivations
+  where
+  getQEnv (Tree (TyDef _ qEnv) _) = qEnv
+
+restricted   :: BindGroup -> Bool
+restricted (BG defs) = any simple defs
+  where
+  simple = isVar . fst . head
+  isVar (Var _) = True
+  isVar _       = False
+
+
+reduceMonoEnv :: [Tyvar] -> MonoEnv -> MonoEnv
+-- Remove unnecessary variables from a monomorphic environment
+reduceMonoEnv ids monoEnv = filter (hasTyVarsFrom ids) monoEnv
+  where
+  hasTyVarsFrom :: [Tyvar] -> Assump Type -> Bool
+  hasTyVarsFrom ids a = not . null $ ids `intersect` tv a
+
+tiSeq :: (PolyEnv -> term -> TI a Derivation)
+      -> PolyEnv -> [term] -> TI a [Derivation]
+tiSeq _ _ []
+ = return $ []
+tiSeq ti polyEnv (bs:bss)
+ = do d1@(Tree (TyBindGroup _ (_ :=> (_, polyEnv'))) _)  <- ti polyEnv bs
+      derivations <- tiSeq ti (polyEnv' ++ polyEnv) bss
+      return $ d1:derivations
+
+-----------------------------------------------------------------------------
+-- TIProg:      Type Inference for Whole Programs
+-----------------------------------------------------------------------------
+
+type Program = [BindGroup]
+
+tiProgram :: PolyEnv -> Program -> Derivation
+tiProgram polyEnv bgs =
+ runTI ((\(Correct x) -> x) (exampleInsts initialEnv)) $ do
+  derivations <- tiSeq tiBindGroup polyEnv bgs
+  let (preds,defEnv) = case unzip (map getPredsDefEnv derivations) of
+                         (predss,defEnvs) -> (concat predss,concat defEnvs)
+  remainingPreds <- updateError (\s -> (Tree (TyUProgram s bgs) derivations))
+                      (reduce preds)
+  defEnv' <- updateError (\s -> (Tree (TyUProgram s bgs) derivations))
+               (defaultSubst [] remainingPreds defEnv)
+  return $ Tree (TyProgram bgs defEnv') derivations
+  where
+  getPredsDefEnv (Tree (TyBindGroup _ (preds :=> ([],polyEnv))) _) =
+    (preds,polyEnv)
+
+
+-----------------------------------------------------------------------------
+-- Main:
+-----------------------------------------------------------------------------
+
+inter :: Program -> IO ()
+inter prog = do
+  putStr "\n\n1 Free navigation through the graph"
+  putStr "\n2 Algorithmic debugging"
+  putStr "\nq Quit"
+  putStr "\nSelect (1 or 2 or q): "
+  c <- getChar
+  case c of
+    '1' -> do
+      putStrLn "\nPress ? for help"
+      walk True True False [] [] (tiProgram env prog,Empty)
+      inter prog
+    '2' -> do
+      putStrLn "\nPress ? for help"
+      let tree = tiProgram env prog
+      printStep False False True (tree,Empty)
+      walk False False True [] [] (algNo True [] (tree,Empty))
+      inter prog
+    'q' -> return ()
+    _ -> inter prog
+
+main :: IO ()
+main = do
+  putStr "\n\nTypeIlluminator Version 13.09.01\nwritten by Olaf Chitil\n\n"
+  putStrLn . concatMap (\(n,p) -> "\n\n" ++ show n ++ ppProgram2 p) .
+    zip [(1::Int)..] $ progs
+  putStr ("\nPlease choose an example program (1-" ++ show numProgs ++ ") ")
+  c <- getChar
+  let i = digitToInt c
+  if c > '0' && c <= '9' && i <= numProgs
+    then inter (progs !! (i-1))
+    else main
+  where
+  numProgs = length progs
+  progs = [progStart,prog2,prog3,progClass1,progClass2]
+
+-----------------------------------------------------------------------------
+-- Tests:
+-----------------------------------------------------------------------------
+
+tyVarA :: Type
+tyVarA = TVar (Tyvar "a" Star)
+tyVarB :: Type
+tyVarB = TVar (Tyvar "b" Star)
+tyVarC :: Type
+tyVarC = TVar (Tyvar "c" Star)
+
+tIO :: Type
+tIO = TCon (Tycon "IO" (Kfun Star Star))
+tBool :: Type
+tBool = TCon (Tycon "Bool" Star)
+
+consNil :: Expr
+consNil = Const "[]"
+consCons :: Expr
+consCons = Const ":"
+
+
+global :: Type -> Tree Typing
+global t = Tree (TyPolyVar ([] :=> ([],t))) []
+globalPreds :: [Pred] -> Type -> Tree Typing
+globalPreds preds t = Tree (TyPolyVar (preds :=> ([],t))) []
+
+
+env :: PolyEnv
+env =
+  ["[]" :>: global (TAp tList tyVarA)
+  ,":" :>: global (tyVarA `fn` (TAp tList tyVarA) `fn`  (TAp tList tyVarA))
+  ,"False" :>: global tBool
+  ,"True" :>: global tBool
+  ,"()" :>: global tUnit
+  ,"." :>: global ((tyVarA `fn` tyVarB) `fn` (tyVarC `fn` tyVarA) `fn`
+                     (tyVarC `fn` tyVarB))
+  ,"print" :>: globalPreds [IsIn "Show" tyVarA] (tyVarA `fn` TAp tIO tUnit)
+  ,"putStr" :>: global (tString `fn` TAp tIO tUnit)
+  ,"show" :>: globalPreds [IsIn "Show" tyVarA] (tyVarA `fn` tString)
+  ,"div" :>: globalPreds [IsIn "Integral" tyVarA]
+               (tyVarA `fn` tyVarA `fn` tyVarA)
+  ,"map" :>: global ((tyVarA `fn` tyVarB) `fn` TAp tList tyVarA `fn` TAp tList tyVarA)
+  ,"++" :>: global (TAp tList tyVarA `fn` TAp tList tyVarA `fn` TAp tList tyVarA)
+  ,"toUpper" :>: global (tChar `fn` tChar)
+  ,":" :>: global (tyVarA `fn` TAp tList tyVarA `fn` TAp tList tyVarA)
+  ,"[]" :>: global (TAp tList tyVarA)
+  ]
+
+
+defStart :: Def
+defStart = [(Var "start" `Ap` Var "xs" `Ap` Var "ys"
+           ,((Var ".") `Ap` (Var "map" `Ap` Var "toUpper") `Ap` (Var "++"))
+            `Ap` Var "xs" `Ap` Var "ys")]
+
+progStart :: [BindGroup]
+progStart = [BG [defStart]]
+
+
+defReverse :: Def
+defReverse = [(Ap (Var "reverse") consNil, consNil)
+             ,(Ap (Var "reverse") (Ap (Ap consCons (Var "x")) (Var "xs"))
+              ,Ap (Ap (Var "++") (Ap (Var "reverse") (Var "xs"))) (Var "x"))]
+
+
+defLast :: Def
+defLast = [(Ap (Var "last") (Var "xs"), Ap (Var "head") (Ap (Var "reverse") (Var "xs")))]
+
+defInit :: Def
+defInit = [(Ap (Var "init") (Var "xs"), Ap (Var "reverse") (Ap (Var "tail") (Ap (Var "reverse") (Var "xs"))))]
+
+defRotateR :: Def
+defRotateR = [(Ap (Var "rotateR") (Var "xs"), Ap (Ap consCons (Ap (Var "last") (Var "xs"))) (Ap (Var "init") (Var "xs")))]
+
+defHead :: Def
+defHead = [(Ap (Var "head") (Ap (Ap consCons (Var "x")) (Var "xs"))
+           ,Var "x")]
+
+defTail :: Def
+defTail = [(Ap (Var "tail") (Ap (Ap consCons (Var "x")) (Var "xs"))
+           ,Var "xs")]
+
+prog2 :: Program
+prog2 = [BG [defHead], BG [defTail], BG [defReverse], BG [defLast], BG [defInit], BG [defRotateR]]
+
+prog3 :: Program
+prog3 = [BG [defReverse]]
+
+
+defClass1 :: Def
+defClass1 = [(Var "class1"
+          ,((Var ".") `Ap` (Var "print") `Ap` (Var "div"))
+           `Ap` (Lit (LitInt 42)))]
+
+progClass1 :: [BindGroup]
+progClass1 = [BG [defClass1]]
+
+defClass2 :: Def
+defClass2 = [(Var "class2"
+             ,((Var ".")
+              `Ap` ((Var ".") `Ap` (Var "putStr") `Ap` (Var "show"))
+              `Ap` ((Var "div") `Ap` (Lit (LitInt 42))))
+              `Ap` (Lit (LitInt 2)))]
+
+progClass2 :: [BindGroup]
+progClass2 = [BG [defClass2]]
+
+
+-----------------------------------------------------------------------------
+
+
+