[remove dead methods mgu and unify
Helmut Grohne <grohne@cs.uni-bonn.de>**20150326085742
 Ignore-this: d98f91fb948f90ed82745fbe8d3c368c
] 
<
[implement specialise using match rather than mgu
Helmut Grohne <grohne@cs.uni-bonn.de>**20150326085416
 Ignore-this: e03ffe1eff3e86719bf0a4b39e04a763
 
 When specialise is called, its first parameter is the result type of an
 application obtained from a type signature. Its second parameter is the type of
 a function or constructor looked up from the context. The difference between
 mgu and match here is that we forbid the function type to restrict the result
 type further, which makes sense as the user explicitly requested the result
 type using a type signature.
] 
> hunk ./src/Syntax/Class/Unifier.hs 53
-                                   
-    mgu ::  (Error e, MonadError e m) => t -> t -> C m (Subst t)
-    
-    mguL :: (Error e, MonadError e m) => [t] -> [t] -> C m (Subst t)
-    mguL   []   []    = return nullSubst
-    mguL (t:ts)(u:us) = do s1 <- mgu t u
-                           s2 <- mguL (applyL s1 ts)(applyL s1 us)
-                           return (s1@@s2)
-    
-    unify :: (Error e, MonadError e m) => t -> t -> C m t
-    unify t1 t2 = mgu t1 t2 >>= return . flip apply t1
hunk ./src/Syntax/UnifyExp.hs 38
-
-    mgu v@(TWildE i1 _) t = checkUnify v t >> varBind v t
-    mgu t v@(TWildE i1 _) = checkUnify t v >> varBind v t
-    mgu v@(TVarE _ _) t   = checkUnify v t >> varBind v t
-    mgu t v@(TVarE _ _)   = checkUnify t v >> varBind v t
-    mgu s t               = if sameSymAtRoot s t 
-                             then (mguL `on` subterms) s t
-                             else nomatch "mgu (226)"  $ (show s) ++ "\n" ++
-                                                         (show t) ++ "\n"
-
-
-
-
-    
--- | Auxiliary to bind terms to variable, check for consistency 
+-- | Auxiliary to bind terms to variable, check for consistency
hunk ./src/Syntax/UnifyTy.hs 5
-    checkMatch, checkUnify, specialise,
+    checkMatch, specialise,
hunk ./src/Syntax/UnifyTy.hs 31
-checkUnify s t = on unify typeOf s t >> return ()
-     
+
hunk ./src/Syntax/UnifyTy.hs 55
-    mgu (VarT n) t               = return $ n <~ t
-    mgu t (VarT n)               = return $ n <~ t
-    mgu (ForallT c (VarT n)) t   = check (n <~ t) c >> return (n <~ t)
-    mgu t (ForallT c (VarT n))   = check (n <~ t) c >> return (n <~ t)
-    mgu (ForallT c (AppT l r)) t = mgu (AppT (quantify l c) (quantify r c)) t
-    mgu t (ForallT c (AppT l r)) = mgu t (AppT (quantify l c) (quantify r c))
-    mgu (AppT l r) (AppT l' r')  = do sl <- mgu l l'
-                                      sr <- mgu r r'
-                                      return $ sl @@ sr
-    mgu (ConT n) (ConT n')
-        | n == n'                = return nullSubst
-    mgu t1 t2                    = throwError . strMsg $ "Type " ++ show t1 ++
-                                              " and type " ++ show t2 ++
-                                              " do not unify"
-
