-- 
-- (c) Susumu Katayama
--

\begin{code}


{-# OPTIONS -cpp -funbox-strict-fields #-}
module MagicHaskeller.Types(Type(..), Kind, TyCon, TyVar, TypeName, Typed(..), tyvars, Subst, plusSubst, 
            emptySubst, apply, mgu, varBind, match, maxVarID, normalizeVarIDs, normalize, unChin,
            Decoder(..), typer, typee, negateTVIDs, limitType, saferQuantify, quantify, quantify', unquantify, lookupSubst, unifyFunAp,
            alltyvars, mapTV, size, unitSubst, applyCheck, assertsubst, substOK, eqType, getRet, getArity, getArities, getAritiesRet, splitArgs, getArgs, pushArgs, popArgs, mguFunAp, revSplitArgs, revGetArgs, module Data.Int
           ) where
import Data.List
import Control.Monad
import Data.Char(ord)
#ifdef QUICKCHECK
import Test.QuickCheck -- this is since 6.4
-- import Debug.QuickCheck
#endif
import Data.Int

-- import Debug.Trace

infixr :->, :>

trace :: p -> a -> a
trace p
_ = a -> a
forall a. a -> a
id


{- Heap profiling with -hy (i.e. by types) flag the -O0 code shows Type (and TyVar) could be improved (by using #Int's),
   but still I think that is not essential. I think recomputation (without memoization) and improvement in Runnable.hs should be tried.
-}


-- :> is same as :-> except FMType.lhs assumes it is a type constructor.
data Type = TV {-# UNPACK #-} !TyVar | TC {-# UNPACK #-} !TyCon | TA Type Type | Type :> Type | Type :-> Type | Type :=> Type
        deriving (Type -> Type -> Bool
(Type -> Type -> Bool) -> (Type -> Type -> Bool) -> Eq Type
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Type -> Type -> Bool
$c/= :: Type -> Type -> Bool
== :: Type -> Type -> Bool
$c== :: Type -> Type -> Bool
Eq, Eq Type
Eq Type
-> (Type -> Type -> Ordering)
-> (Type -> Type -> Bool)
-> (Type -> Type -> Bool)
-> (Type -> Type -> Bool)
-> (Type -> Type -> Bool)
-> (Type -> Type -> Type)
-> (Type -> Type -> Type)
-> Ord Type
Type -> Type -> Bool
Type -> Type -> Ordering
Type -> Type -> Type
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Type -> Type -> Type
$cmin :: Type -> Type -> Type
max :: Type -> Type -> Type
$cmax :: Type -> Type -> Type
>= :: Type -> Type -> Bool
$c>= :: Type -> Type -> Bool
> :: Type -> Type -> Bool
$c> :: Type -> Type -> Bool
<= :: Type -> Type -> Bool
$c<= :: Type -> Type -> Bool
< :: Type -> Type -> Bool
$c< :: Type -> Type -> Bool
compare :: Type -> Type -> Ordering
$ccompare :: Type -> Type -> Ordering
$cp1Ord :: Eq Type
Ord, ReadPrec [Type]
ReadPrec Type
Int -> ReadS Type
ReadS [Type]
(Int -> ReadS Type)
-> ReadS [Type] -> ReadPrec Type -> ReadPrec [Type] -> Read Type
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Type]
$creadListPrec :: ReadPrec [Type]
readPrec :: ReadPrec Type
$creadPrec :: ReadPrec Type
readList :: ReadS [Type]
$creadList :: ReadS [Type]
readsPrec :: Int -> ReadS Type
$creadsPrec :: Int -> ReadS Type
Read)

size :: Type -> Int
size :: Type -> Int
size (TC TyCon
_) = Int
1
size (TV TyCon
_) = Int
1 -- but potentially large.
size (TA Type
t0 Type
t1)  = Type -> Int
size Type
t0 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Type -> Int
size Type
t1
size (Type
t0 :> Type
t1)  = Type -> Int
size Type
t0 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Type -> Int
size Type
t1
size (Type
t0 :-> Type
t1) = Type -> Int
size Type
t0 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Type -> Int
size Type
t1

{-
-- sizeCheck is normally id, but if the size is too large it fails.
sizeCheck :: Type -> Type
sizeCheck ty = sc 100 ty
    where sc 0 _ = error ("sizeCheck: " ++ show ty)
          sc n (TA t0 t1) = 
-}

{- I comment this out because this is unused (except in Classification.tex, where arityOf is redefined) and confusing along with |:>|.
arityOf :: Type -> Int
arityOf (t1 :-> t0) = 1 + arityOf t0
arityOf _ = 0 -- including :>
-}

#ifdef QUICKCHECK
instance Arbitrary Type where
    arbitrary = sized arbType

arbType 0 = oneof [liftM TV arbitrary, liftM TC arbitrary]
arbType n = frequency [ (8, arbType 0),
                        (2, liftM2 TA    (arbType (n `div` 2)) (arbType (n `div` 2))),
                        (2, liftM2 (:->) (arbType (n `div` 2)) (arbType (n `div` 2))) ]
#endif

-- {-# INLINE mapTV #-}
mapTV :: (TyVar -> TyVar) -> Type -> Type
mapTV :: (TyCon -> TyCon) -> Type -> Type
mapTV TyCon -> TyCon
f Type
t = -- if t/=t then undefined else
            Type -> Type
mtv Type
t
    where mtv :: Type -> Type
mtv (TA Type
t0 Type
t1)  = Type -> Type -> Type
TA (Type -> Type
mtv Type
t0) (Type -> Type
mtv Type
t1)
          mtv (Type
t1 :=> Type
t0) = (Type -> Type
mtv Type
t1) Type -> Type -> Type
:=> (Type -> Type
mtv Type
t0)
          mtv (Type
t1 :-> Type
t0) = (Type -> Type
mtv Type
t1) Type -> Type -> Type
:-> (Type -> Type
mtv Type
t0)
          mtv (Type
t1 :> Type
t0)  = (Type -> Type
mtv Type
t1) Type -> Type -> Type
:>  (Type -> Type
mtv Type
t0)
          mtv (TV TyCon
tv)     = TyCon -> Type
TV (TyCon -> TyCon
f TyCon
tv)
          mtv tc :: Type
tc@(TC TyCon
_)   = Type
tc

negateTVIDs :: Type -> Type
negateTVIDs :: Type -> Type
negateTVIDs   = (TyCon -> TyCon) -> Type -> Type
mapTV (\TyCon
tvid -> -TyCon
1 TyCon -> TyCon -> TyCon
forall a. Num a => a -> a -> a
- TyCon
tvid)

-- limitType is like counting the size of a type, but is specialised to limit it.
limitType :: a -> Type -> a
limitType a
n (TC TyCon
_)    = a
na -> a -> a
forall a. Num a => a -> a -> a
-a
1
limitType a
n (TV TyCon
_)    = a
na -> a -> a
forall a. Num a => a -> a -> a
-a
1
limitType a
n (Type
u :-> Type
t) = a -> Type -> Type -> a
lt a
n Type
t Type
u
limitType a
n (Type
u :> Type
t)  = a -> Type -> Type -> a
lt a
n Type
t Type
u
limitType a
n (TA Type
t Type
u)  = a -> Type -> Type -> a
lt a
n Type
t Type
u

lt :: a -> Type -> Type -> a
lt a
n Type
t Type
u = case a -> Type -> a
limitType a
n Type
t of a
m | a
m a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
0     -> a -> Type -> a
limitType a
m Type
u
                                   | Bool
otherwise -> -a
1

alltyvars :: Type -> Subst -> [TyVar]
alltyvars :: Type -> Subst -> [TyCon]
alltyvars Type
ty Subst
s = Type -> Subst -> [TyCon] -> [TyCon]
alltyvars' Type
ty Subst
s []
alltyvars' :: Type -> Subst -> [TyVar] -> [TyVar]
alltyvars' :: Type -> Subst -> [TyCon] -> [TyCon]
alltyvars' (TV TyCon
tv)   Subst
s = case Subst -> TyCon -> Maybe Type
forall (m :: * -> *). MonadPlus m => Subst -> TyCon -> m Type
lookupSubst Subst
s TyCon
tv of Just Type
t  -> Type -> Subst -> [TyCon] -> [TyCon]
alltyvars' Type
t Subst
s
                                                  Maybe Type
Nothing -> (TyCon
tvTyCon -> [TyCon] -> [TyCon]
forall a. a -> [a] -> [a]
:)
alltyvars' (TC TyCon
tc)   Subst
s = [TyCon] -> [TyCon]
forall a. a -> a
id
alltyvars' (TA Type
t Type
u)  Subst
s = Type -> Subst -> [TyCon] -> [TyCon]
alltyvars' Type
t Subst
s ([TyCon] -> [TyCon]) -> ([TyCon] -> [TyCon]) -> [TyCon] -> [TyCon]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Subst -> [TyCon] -> [TyCon]
alltyvars' Type
u Subst
s
alltyvars' (Type
u :> Type
t)  Subst
s = Type -> Subst -> [TyCon] -> [TyCon]
alltyvars' Type
t Subst
s ([TyCon] -> [TyCon]) -> ([TyCon] -> [TyCon]) -> [TyCon] -> [TyCon]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Subst -> [TyCon] -> [TyCon]
alltyvars' Type
u Subst
s
alltyvars' (Type
u :-> Type
t) Subst
s = Type -> Subst -> [TyCon] -> [TyCon]
alltyvars' Type
t Subst
s ([TyCon] -> [TyCon]) -> ([TyCon] -> [TyCon]) -> [TyCon] -> [TyCon]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Subst -> [TyCon] -> [TyCon]
alltyvars' Type
u Subst
s
alltyvars' (Type
u :=> Type
t) Subst
s = Type -> Subst -> [TyCon] -> [TyCon]
alltyvars' Type
t Subst
s -- Is this enough?

-- These can sometimes be VERY time-consuming, because they are used by mgu, varBind, etc.
{-# INLINE tyvars  #-}
{-# INLINE tyvars' #-}
tyvars :: Type -> [TyVar]
tyvars :: Type -> [TyCon]
tyvars Type
ty = Type -> [TyCon] -> [TyCon]
tyvars' Type
ty []
tyvars' :: Type -> [TyVar] -> [TyVar]
tyvars' :: Type -> [TyCon] -> [TyCon]
tyvars' (TV TyCon
tv)   = (TyCon
tvTyCon -> [TyCon] -> [TyCon]
forall a. a -> [a] -> [a]
:)
tyvars' (TC TyCon
tc)   = [TyCon] -> [TyCon]
forall a. a -> a
id
tyvars' (TA Type
t Type
u)  = Type -> [TyCon] -> [TyCon]
tyvars' Type
t ([TyCon] -> [TyCon]) -> ([TyCon] -> [TyCon]) -> [TyCon] -> [TyCon]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> [TyCon] -> [TyCon]
tyvars' Type
u
tyvars' (Type
u :> Type
t)  = Type -> [TyCon] -> [TyCon]
tyvars' Type
t ([TyCon] -> [TyCon]) -> ([TyCon] -> [TyCon]) -> [TyCon] -> [TyCon]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> [TyCon] -> [TyCon]
tyvars' Type
u
tyvars' (Type
u :-> Type
t) = Type -> [TyCon] -> [TyCon]
tyvars' Type
t ([TyCon] -> [TyCon]) -> ([TyCon] -> [TyCon]) -> [TyCon] -> [TyCon]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> [TyCon] -> [TyCon]
tyvars' Type
u
tyvars' (Type
u :=> Type
t) = Type -> [TyCon] -> [TyCon]
tyvars' Type
t

-- use this instead of QType
maxVarID :: Type -> TyVar
maxVarID :: Type -> TyCon
maxVarID (TV TyCon
tv)   = TyCon
tv
maxVarID (TC TyCon
_)    = -TyCon
1 -- assume non-negative.
maxVarID (TA Type
t Type
u)  = Type -> TyCon
maxVarID Type
t TyCon -> TyCon -> TyCon
forall a. Ord a => a -> a -> a
`max` Type -> TyCon
maxVarID Type
u
maxVarID (Type
t :> Type
u)  = Type -> TyCon
maxVarID Type
t TyCon -> TyCon -> TyCon
forall a. Ord a => a -> a -> a
`max` Type -> TyCon
maxVarID Type
u
maxVarID (Type
t :-> Type
u) = Type -> TyCon
maxVarID Type
t TyCon -> TyCon -> TyCon
forall a. Ord a => a -> a -> a
`max` Type -> TyCon
maxVarID Type
u
maxVarID (Type
_ :=> Type
u) =                  Type -> TyCon
maxVarID Type
u
{- higher-order kind$B$O9M$($J$$$H$$$&$+!$(B(*->*)->*$B$H(B*->*$B$r6hJL$7$J$$!J7?0z?t$N?t$N$_9MN8$9$k!K!%$=$N>e$G!$(Btype Kind = Int$B$H$9$k!%(BMemo$B$9$k$H$-$K(BKind$B$G(Bindex$B$7$?$$$C$F$N$H!$7?0z?t$N(BKind$B$O?dO@$G$-$J$$$N$G!%(B

$B$d$C$Q@53N$K$O!$!V(B(*->*)->*$B$H(B*->*$B$r6hJL$7$J$$!W$G$O$J$/!$!V(B(*->*)->* (higher order kind)$B$rG'$a$J$$!W$H$$$&$Y$-!%(B
TyApp t u$B$K$*$$$F!$(Bu::*$B$r2>Dj$7$F$7$^$C$F$$$k$N$G!%(B

data Kind = Star | Kind ::-> Kind deriving (Show, Eq, Ord, Read)
instance Arbitrary Kind where
    arbitrary = sized arbKind

arbKind 0 = return Star
arbKind n = frequency [ (4, return Star),
                        (1, liftM2 (::->) (arbKind (n `div` 2)) (arbKind (n `div` 2))) ]
-}
type Kind = Int

 -- comparison between cs and ds is done in TypeLib, comparing types of different vars.

type TyVar = Int8
type TyCon = TyVar -- TyCon should be the same or bigger than TyVar, because the quantify function converts TyVar into TyCon

type TypeName = String

-- Encoder and Decoder are partly moved to FMType.lhs

-- TyVar should be shared, so it is returned by the decoder.
-- $B$"$H!"(BdecoList$B$O$R$@$j$+$i$_$.$K$N$S$F$$$C$?$[$&$,$$$$$N$+!)(B

data Decoder = Dec [TyVar] TyVar
               deriving Int -> Decoder -> ShowS
[Decoder] -> ShowS
Decoder -> String
(Int -> Decoder -> ShowS)
-> (Decoder -> String) -> ([Decoder] -> ShowS) -> Show Decoder
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Decoder] -> ShowS
$cshowList :: [Decoder] -> ShowS
show :: Decoder -> String
$cshow :: Decoder -> String
showsPrec :: Int -> Decoder -> ShowS
$cshowsPrec :: Int -> Decoder -> ShowS
Show

{-# INLINE normalizeVarIDs #-}
-- FMType$B!$(BMemoTree$B$J$I$G(Bindex$B$9$k$H$-$N$?$a$K!$(BvarID$B$r(B0,1,...$B$K(Broot$BB&$+$i=g$K@55,2=$9$k(B
normalizeVarIDs :: Type -> TyVar -> (Type, Decoder)
normalizeVarIDs :: Type -> TyCon -> (Type, Decoder)
normalizeVarIDs Type
ty TyCon
mx = let decoList :: [TyCon]
decoList = [TyCon] -> [TyCon]
forall a. Eq a => [a] -> [a]
nub ([TyCon] -> [TyCon]) -> [TyCon] -> [TyCon]
forall a b. (a -> b) -> a -> b
$ Type -> [TyCon]
tyvars Type
ty
                            tup :: [(TyCon, TyCon)]
tup      = [TyCon] -> [TyCon] -> [(TyCon, TyCon)]
forall a b. [a] -> [b] -> [(a, b)]
zip [TyCon]
decoList [TyCon
0..]
                            encoType :: Type
encoType = (TyCon -> TyCon) -> Type -> Type
mapTV (\TyCon
tv -> case TyCon -> [(TyCon, TyCon)] -> Maybe TyCon
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup TyCon
tv [(TyCon, TyCon)]
tup of Just TyCon
n  -> TyCon
n) Type
ty
                            len :: TyCon
len      = [TyCon] -> TyCon
forall i a. Num i => [a] -> i
genericLength [TyCon]
decoList
                            margin :: TyCon
margin   = -- trace ("normalizeVarIDs: mx == "++show mx++ " and len = " ++ show len) $
                                       TyCon
mx TyCon -> TyCon -> TyCon
forall a. Num a => a -> a -> a
+ TyCon
1 TyCon -> TyCon -> TyCon
forall a. Num a => a -> a -> a
- TyCon
len
                        in -- trace ("len = " ++ show len) $ $B$[$H$s$I$N%1!<%9$G(B0$B$+(B1$B!$$?$^!<$K(B2$B$+(B3
                           (Type
encoType, [TyCon] -> TyCon -> Decoder
Dec [TyCon]
decoList TyCon
margin)
normalize :: Type -> Type
normalize Type
ty = (Type, Decoder) -> Type
forall a b. (a, b) -> a
fst ((Type, Decoder) -> Type) -> (Type, Decoder) -> Type
forall a b. (a -> b) -> a -> b
$ Type -> TyCon -> (Type, Decoder)
normalizeVarIDs Type
ty (String -> TyCon
forall a. HasCallStack => String -> a
error String
"undef of normalize")

eqType :: Type -> Type -> Bool
eqType :: Type -> Type -> Bool
eqType Type
t0 Type
t1 = Type -> Type
normalize Type
t0 Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type -> Type
normalize Type
t1


-- quantify freezes tyvars into tycons whose IDs are negative.
saferQuantify, quantify, quantify', unquantify :: Type -> Type
saferQuantify :: Type -> Type
saferQuantify = Type -> Type
quantify (Type -> Type) -> (Type -> Type) -> Type -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Type
negUnquantify
negUnquantify :: Type -> Type
negUnquantify (TC TyCon
i) | TyCon
i TyCon -> TyCon -> Bool
forall a. Ord a => a -> a -> Bool
< TyCon
0 = TyCon -> Type
TV (TyCon -> Type) -> TyCon -> Type
forall a b. (a -> b) -> a -> b
$ TyCon -> TyCon
forall a b. (Integral a, Num b) => a -> b
fromIntegral TyCon
i
negUnquantify (TA Type
t Type
u) = Type -> Type -> Type
TA (Type -> Type
negUnquantify Type
t) (Type -> Type
negUnquantify Type
u)
negUnquantify (Type
u :-> Type
t) = Type -> Type
negUnquantify Type
u Type -> Type -> Type
:-> Type -> Type
negUnquantify Type
t
negUnquantify (Type
u :> Type
t)  = Type -> Type
negUnquantify Type
u Type -> Type -> Type
:> Type -> Type
negUnquantify Type
t
negUnquantify (Type
u :=> Type
t) = String -> Type
forall a. HasCallStack => String -> a
error String
"negUnquantify: applied to types with contexts"
negUnquantify Type
t = Type
t

quantify :: Type -> Type
quantify Type
ty = Type -> Type
quantify' (Type -> Type
normalize Type
ty)
quantify' :: Type -> Type
quantify' (TV TyCon
iD) = TyCon -> Type
TC (TyCon -> Type) -> TyCon -> Type
forall a b. (a -> b) -> a -> b
$ TyCon -> TyCon
forall a b. (Integral a, Num b) => a -> b
fromIntegral (-TyCon
iDTyCon -> TyCon -> TyCon
forall a. Num a => a -> a -> a
-TyCon
1)
quantify' tc :: Type
tc@(TC TyCon
_) = Type
tc
quantify' (TA Type
t Type
u)  = Type -> Type -> Type
TA (Type -> Type
quantify' Type
t) (Type -> Type
quantify' Type
u)
quantify' (Type
u :-> Type
t) = Type -> Type
quantify' Type
u Type -> Type -> Type
:-> Type -> Type
quantify' Type
t
quantify' (Type
u :> Type
t)  = Type -> Type
quantify' Type
u Type -> Type -> Type
:>  Type -> Type
quantify' Type
t

-- unquantify is used only as a preprocessor of normalize, when used as a preprocessor of quantify. See notes on Nov. 17, 2006.
unquantify :: Type -> Type
unquantify (TC TyCon
tc) | TyCon
tc TyCon -> TyCon -> Bool
forall a. Ord a => a -> a -> Bool
< TyCon
0 = TyCon -> Type
TV (TyCon -> Type) -> TyCon -> Type
forall a b. (a -> b) -> a -> b
$ TyCon -> TyCon
forall a b. (Integral a, Num b) => a -> b
fromIntegral (-TyCon
1TyCon -> TyCon -> TyCon
forall a. Num a => a -> a -> a
-TyCon
tc)
unquantify (TA Type
t Type
u) = Type -> Type -> Type
TA (Type -> Type
unquantify Type
t) (Type -> Type
unquantify Type
u)
unquantify (Type
u :-> Type
t) = Type -> Type
unquantify Type
u Type -> Type -> Type
:-> Type -> Type
unquantify Type
t
unquantify (Type
u :> Type
t) = Type -> Type
unquantify Type
u Type -> Type -> Type
:> Type -> Type
unquantify Type
t
unquantify (Type
u :=> Type
t) = String -> Type
forall a. HasCallStack => String -> a
error String
"unquantify: applied to types with contexts"
unquantify Type
t = Type
t

{-
mbQuantify ty = return (quantify ty)
-}
{-
encodeSubst :: Encoder -> Subst -> Subst
encodeSubst = plusSubst
-}
unifyFunAp :: String -> Type -> Type -> Type
unifyFunAp String
str Type
t Type
u = case Type -> Type -> Maybe Type
forall (m :: * -> *). MonadPlus m => Type -> Type -> m Type
uniFunAp Type
t Type
u of Just Type
v -> String -> Type -> Type
forall p a. p -> a -> a
trace (String
str String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
". unify "String -> ShowS
forall a. [a] -> [a] -> [a]
++Type -> String
forall a. Show a => a -> String
show Type
t String -> ShowS
forall a. [a] -> [a] -> [a]
++String
" and "String -> ShowS
forall a. [a] -> [a] -> [a]
++Type -> String
forall a. Show a => a -> String
show Type
u) Type
v
                                          Maybe Type
Nothing -> String -> Type
forall a. HasCallStack => String -> a
error (String
str String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
". unifyFunAp: t = "String -> ShowS
forall a. [a] -> [a] -> [a]
++Type -> String
forall a. Show a => a -> String
show Type
tString -> ShowS
forall a. [a] -> [a] -> [a]
++String
", and u = "String -> ShowS
forall a. [a] -> [a] -> [a]
++Type -> String
forall a. Show a => a -> String
show Type
u)
uniFunAp :: MonadPlus m => Type -> Type -> m Type
uniFunAp :: Type -> Type -> m Type
uniFunAp (Type
a:->Type
r) Type
t = do Subst
subst <- Type -> Type -> m Subst
forall (m :: * -> *). MonadPlus m => Type -> Type -> m Subst
mgu (Type -> Type
getRet Type
a) (Type -> Type
getRet Type
t)
                        Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst -> Type -> Type
apply Subst
subst Type
r)
uniFunAp (Type
a:=>Type
r) Type
t = Type -> Type -> m Type
forall (m :: * -> *). MonadPlus m => Type -> Type -> m Type
uniFunAp (Type
aType -> Type -> Type
:->Type
r) Type
t
uniFunAp Type
f Type
t = m Type
forall (m :: * -> *) a. MonadPlus m => m a
mzero -- error ("uniFunAp: f = "++show f++" and t = "++show t)


mguFunAp :: MonadPlus m => Type -> Type -> m Type
mguFunAp :: Type -> Type -> m Type
mguFunAp Type
t0 Type
t1 = String -> m Type -> m Type
forall p a. p -> a -> a
trace (String
"mguFunAp t0 = "String -> ShowS
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show Type
t0String -> ShowS
forall a. [a] -> [a] -> [a]
++String
", and t1 = "String -> ShowS
forall a. [a] -> [a] -> [a]
++Type -> String
forall a. Show a => a -> String
show Type
t1) (m Type -> m Type) -> m Type -> m Type
forall a b. (a -> b) -> a -> b
$
                 case Type -> TyCon
maxVarID Type
t1 TyCon -> TyCon -> TyCon
forall a. Num a => a -> a -> a
+ TyCon
1 of TyCon
mx -> Type -> Type -> m Type
forall (m :: * -> *). MonadPlus m => Type -> Type -> m Type
mfa ((TyCon -> TyCon) -> Type -> Type
mapTV (TyCon
mxTyCon -> TyCon -> TyCon
forall a. Num a => a -> a -> a
+) Type
t0) Type
t1
mfa :: Type -> Type -> m Type
mfa (Type
a:->Type
r) Type
t = do Subst
subst <- Type -> Type -> m Subst
forall (m :: * -> *). MonadPlus m => Type -> Type -> m Subst
mgu Type
a Type
t
--                   return (apply subst r)
                   let retv :: Type
retv = (Subst -> Type -> Type
apply Subst
subst Type
r)
                   String -> m Type -> m Type
forall p a. p -> a -> a
trace (String
"retv = "String -> ShowS
forall a. [a] -> [a] -> [a]
++Type -> String
forall a. Show a => a -> String
show Type
retv) (m Type -> m Type) -> m Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
retv
mfa (Type
a:>Type
r)  Type
t = Type -> Type -> m Type
mfa (Type
aType -> Type -> Type
:->Type
r) Type
t -- mguFunAp is only used by PolyDynamic
mfa (Type
a:=>Type
r) Type
t = Type -> Type -> m Type
mfa (Type
aType -> Type -> Type
:->Type
r) Type
t -- mguFunAp is only used by PolyDynamic
mfa t :: Type
t@(TV TyCon
_) Type
_ = Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
t -- mguFunAp assumes different name spaces
mfa Type
f       Type
t = m Type
forall (m :: * -> *) a. MonadPlus m => m a
mzero



pushArgsCPS :: Integral i => (i -> i -> [Type] -> Type -> a) -> [Type] -> Type -> a
pushArgsCPS :: (i -> i -> [Type] -> Type -> a) -> [Type] -> Type -> a
pushArgsCPS i -> i -> [Type] -> Type -> a
f = i -> i -> [Type] -> Type -> a
pa i
0 i
0
  where 
        pa :: i -> i -> [Type] -> Type -> a
pa i
c i
n [Type]
args (Type
t0:->Type
t1)        = i -> i -> [Type] -> Type -> a
pa i
c (i
ni -> i -> i
forall a. Num a => a -> a -> a
+i
1) (Type
t0Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:[Type]
args) Type
t1
        pa i
c i
n [Type]
args (Type
t0:>Type
t1)         = i -> i -> [Type] -> Type -> a
pa i
c (i
ni -> i -> i
forall a. Num a => a -> a -> a
+i
1) (Type
t0Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:[Type]
args) Type
t1
        pa i
c i
n [Type]
args (Type
t0:=>Type
t1)        = i -> i -> [Type] -> Type -> a
pa (i
ci -> i -> i
forall a. Num a => a -> a -> a
+i
1) i
n (Type
t0Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:[Type]
args) Type
t1 -- So, the arity is not incremented in this case.
        pa i
c i
n [Type]
args Type
retty            = i -> i -> [Type] -> Type -> a
f i
c i
n [Type]
args Type
retty

pushArgs :: [Type] -> Type -> ([Type],Type)
pushArgs :: [Type] -> Type -> ([Type], Type)
pushArgs = (Integer -> Integer -> [Type] -> Type -> ([Type], Type))
-> [Type] -> Type -> ([Type], Type)
forall i a.
Integral i =>
(i -> i -> [Type] -> Type -> a) -> [Type] -> Type -> a
pushArgsCPS (\Integer
_ Integer
_ [Type]
a Type
r -> ([Type]
a,Type
r))

getRet :: Type -> Type
getRet  = (Integer -> Integer -> [Type] -> Type -> Type)
-> [Type] -> Type -> Type
forall i a.
Integral i =>
(i -> i -> [Type] -> Type -> a) -> [Type] -> Type -> a
pushArgsCPS (\Integer
_ Integer
_ [Type]
_ Type
r -> Type
r) [Type]
forall a. HasCallStack => a
undefined
getArgs :: Type -> [Type]
getArgs = (Integer -> Integer -> [Type] -> Type -> [Type])
-> [Type] -> Type -> [Type]
forall i a.
Integral i =>
(i -> i -> [Type] -> Type -> a) -> [Type] -> Type -> a
pushArgsCPS (\Integer
_ Integer
_ [Type]
a Type
_ -> [Type]
a) []
getNumCxts, getArity :: Integral i => Type -> i
getNumCxts :: Type -> i
getNumCxts = (i -> i -> [Type] -> Type -> i) -> [Type] -> Type -> i
forall i a.
Integral i =>
(i -> i -> [Type] -> Type -> a) -> [Type] -> Type -> a
pushArgsCPS (\i
c i
_ [Type]
_ Type
_ -> i
c) [Type]
forall a. HasCallStack => a
undefined
getArity :: Type -> i
getArity   = (i -> i -> [Type] -> Type -> i) -> [Type] -> Type -> i
forall i a.
Integral i =>
(i -> i -> [Type] -> Type -> a) -> [Type] -> Type -> a
pushArgsCPS (\i
_ i
i [Type]
_ Type
_ -> i
i) [Type]
forall a. HasCallStack => a
undefined
getArities :: Integral i => Type -> (i,i)
getArities :: Type -> (i, i)
getArities = (i -> i -> [Type] -> Type -> (i, i)) -> [Type] -> Type -> (i, i)
forall i a.
Integral i =>
(i -> i -> [Type] -> Type -> a) -> [Type] -> Type -> a
pushArgsCPS (\i
c i
i [Type]
_ Type
_ -> (i
c,i
i)) [Type]
forall a. HasCallStack => a
undefined
getAritiesRet :: Integral i => Type -> (i,i,Type)
getAritiesRet :: Type -> (i, i, Type)
getAritiesRet = (i -> i -> [Type] -> Type -> (i, i, Type))
-> [Type] -> Type -> (i, i, Type)
forall i a.
Integral i =>
(i -> i -> [Type] -> Type -> a) -> [Type] -> Type -> a
pushArgsCPS (\i
c i
i [Type]
_ Type
r -> (i
c,i
i,Type
r)) [Type]
forall a. HasCallStack => a
undefined


-- splitArgsCPS :: (Int -> [Type] -> Type -> a) -> Type -> a
-- splitArgsCPS f = pushArgsCPS f []

splitArgs :: Type -> ([Type],Type)
splitArgs :: Type -> ([Type], Type)
splitArgs = [Type] -> Type -> ([Type], Type)
pushArgs []

-- $B5U=g$K@Q$s$G$$$/(B. :=>$B$b(B:>$B$b$J$$$H2>Dj!%(B
revSplitArgs :: Integral i => Type -> (i,[Type],Type)
revSplitArgs :: Type -> (i, [Type], Type)
revSplitArgs (Type
t0:->Type
t1) = case Type -> (i, [Type], Type)
forall i. Integral i => Type -> (i, [Type], Type)
revSplitArgs Type
t1 of (i
n,[Type]
args,Type
ret) -> (i
ni -> i -> i
forall a. Num a => a -> a -> a
+i
1, Type
t0Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:[Type]
args, Type
ret)
revSplitArgs Type
t         = (i
0, [], Type
t)

-- $B5U=g$K@Q$s$G$$$/(B. :=>$B$b(B:>$B$b$J$$$H2>Dj!%(B
revGetArgs :: Type -> [Type]
revGetArgs :: Type -> [Type]
revGetArgs Type
ty = case Type -> (Integer, [Type], Type)
forall i. Integral i => Type -> (i, [Type], Type)
revSplitArgs Type
ty of (Integer
_,[Type]
ts,Type
_) -> [Type]
ts

popArgs :: [Type] -> Type -> Type
popArgs :: [Type] -> Type -> Type
popArgs = (Type -> [Type] -> Type) -> [Type] -> Type -> Type
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((Type -> Type -> Type) -> Type -> [Type] -> Type
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ((Type -> Type -> Type) -> Type -> Type -> Type
forall a b c. (a -> b -> c) -> b -> a -> c
flip Type -> Type -> Type
(:->)))

{- $B$R$C$/$jJV$5$J$+$C$?%P!<%8%g%s(B
popArgs = flip (foldr (:->))
splitArgs (t0:->t1) = let (ts, t) = splitArgs t1 in (t0:ts, t)
splitArgs t         = ([], t)
-}

\end{code}

data "Typed", taken from obsolete/Binding.hs

\begin{code}

data Typed a   = a ::: !Type deriving (Int -> Typed a -> ShowS
[Typed a] -> ShowS
Typed a -> String
(Int -> Typed a -> ShowS)
-> (Typed a -> String) -> ([Typed a] -> ShowS) -> Show (Typed a)
forall a. Show a => Int -> Typed a -> ShowS
forall a. Show a => [Typed a] -> ShowS
forall a. Show a => Typed a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Typed a] -> ShowS
$cshowList :: forall a. Show a => [Typed a] -> ShowS
show :: Typed a -> String
$cshow :: forall a. Show a => Typed a -> String
showsPrec :: Int -> Typed a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Typed a -> ShowS
Show, Typed a -> Typed a -> Bool
(Typed a -> Typed a -> Bool)
-> (Typed a -> Typed a -> Bool) -> Eq (Typed a)
forall a. Eq a => Typed a -> Typed a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Typed a -> Typed a -> Bool
$c/= :: forall a. Eq a => Typed a -> Typed a -> Bool
== :: Typed a -> Typed a -> Bool
$c== :: forall a. Eq a => Typed a -> Typed a -> Bool
Eq, Eq (Typed a)
Eq (Typed a)
-> (Typed a -> Typed a -> Ordering)
-> (Typed a -> Typed a -> Bool)
-> (Typed a -> Typed a -> Bool)
-> (Typed a -> Typed a -> Bool)
-> (Typed a -> Typed a -> Bool)
-> (Typed a -> Typed a -> Typed a)
-> (Typed a -> Typed a -> Typed a)
-> Ord (Typed a)
Typed a -> Typed a -> Bool
Typed a -> Typed a -> Ordering
Typed a -> Typed a -> Typed a
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a. Ord a => Eq (Typed a)
forall a. Ord a => Typed a -> Typed a -> Bool
forall a. Ord a => Typed a -> Typed a -> Ordering
forall a. Ord a => Typed a -> Typed a -> Typed a
min :: Typed a -> Typed a -> Typed a
$cmin :: forall a. Ord a => Typed a -> Typed a -> Typed a
max :: Typed a -> Typed a -> Typed a
$cmax :: forall a. Ord a => Typed a -> Typed a -> Typed a
>= :: Typed a -> Typed a -> Bool
$c>= :: forall a. Ord a => Typed a -> Typed a -> Bool
> :: Typed a -> Typed a -> Bool
$c> :: forall a. Ord a => Typed a -> Typed a -> Bool
<= :: Typed a -> Typed a -> Bool
$c<= :: forall a. Ord a => Typed a -> Typed a -> Bool
< :: Typed a -> Typed a -> Bool
$c< :: forall a. Ord a => Typed a -> Typed a -> Bool
compare :: Typed a -> Typed a -> Ordering
$ccompare :: forall a. Ord a => Typed a -> Typed a -> Ordering
$cp1Ord :: forall a. Ord a => Eq (Typed a)
Ord)

typee :: Typed a -> a
typee (a
a ::: Type
_) = a
a
typer :: Typed a -> Type
typer (a
_ ::: Type
t) = Type
t

instance Functor Typed where
  fmap :: (a -> b) -> Typed a -> Typed b
fmap a -> b
f (a
a ::: Type
t) = a -> b
f a
a b -> Type -> Typed b
forall a. a -> Type -> Typed a
::: Type
t

\end{code}

\section{Type inference tools}

\begin{code}

type Subst = [(TyVar,Type)]

showsAssoc :: [(a, a)] -> ShowS
showsAssoc [] = ShowS
forall a. a -> a
id
showsAssoc ((a
k,a
v):[(a, a)]
assocs) = (Char
' 'Char -> ShowS
forall a. a -> [a] -> [a]
:) ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> ShowS
forall a. Show a => a -> ShowS
shows a
k ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String
"\t|-> "String -> ShowS
forall a. [a] -> [a] -> [a]
++) ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> ShowS
forall a. Show a => a -> ShowS
shows a
v ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char
'\n'Char -> ShowS
forall a. a -> [a] -> [a]
:) ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(a, a)] -> ShowS
showsAssoc [(a, a)]
assocs

emptySubst :: [a]
emptySubst = []
unitSubst :: a -> b -> [(a, b)]
unitSubst a
k b
e = [(a
k, b
e)]


-- subst$B$K$/$o$($k$H$-$O(B:>$B$r(B:->$B$K$;$M$P$J$i$J$$$,!"(Bapply s (a:>b)$B$O(Bapply s a :> apply s b
match, mgu :: MonadPlus m => Type -> Type -> m Subst

match :: Type -> Type -> m Subst
match (Type
l :-> Type
r) (Type
l' :-> Type
r') = Type -> Type -> Type -> Type -> m Subst
forall (m :: * -> *).
MonadPlus m =>
Type -> Type -> Type -> Type -> m Subst
match2Ap Type
l Type
r Type
l' Type
r'
{-
match (l :-> r) (l' :> r')  = match2Ap l r l' r'
match (l :> r)  (l' :-> r') = match2Ap l r l' r'
match (l :> r)  (l' :> r')  = match2Ap l r l' r'
-}
match (TA Type
l Type
r) (TA Type
l' Type
r') = Type -> Type -> Type -> Type -> m Subst
forall (m :: * -> *).
MonadPlus m =>
Type -> Type -> Type -> Type -> m Subst
match2Ap Type
l Type
r Type
l' Type
r'
match (TV TyCon
u)   Type
t        = TyCon -> Type -> m Subst
forall (m :: * -> *). MonadPlus m => TyCon -> Type -> m Subst
varBind TyCon
u Type
t
match (TC TyCon
tc1) (TC TyCon
tc2) | TyCon
tc1TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
==TyCon
tc2 = Subst -> m Subst
forall (m :: * -> *) a. Monad m => a -> m a
return Subst
forall a. [a]
emptySubst
match Type
_        Type
_        = m Subst
forall (m :: * -> *) a. MonadPlus m => m a
mzero

match2Ap :: Type -> Type -> Type -> Type -> m Subst
match2Ap Type
l Type
r Type
l' Type
r' = do Subst
s1 <- Type -> Type -> m Subst
forall (m :: * -> *). MonadPlus m => Type -> Type -> m Subst
match Type
l Type
l'
                        Subst
s2 <- Type -> Type -> m Subst
forall (m :: * -> *). MonadPlus m => Type -> Type -> m Subst
match (Subst -> Type -> Type
apply Subst
s1 Type
r) Type
r'
                        Subst -> m Subst
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst
s2 Subst -> Subst -> Subst
`plusSubst` Subst
s1)

unChin :: Type -> Type
unChin (TA Type
l Type
r)  = Type -> Type -> Type
TA Type
l (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
unChin Type
r
unChin (Type
l :> Type
r)  = Type -> Type
unChin Type
l Type -> Type -> Type
:-> Type -> Type
unChin Type
r
unChin (Type
l :-> Type
r) = Type -> Type
unChin Type
l Type -> Type -> Type
:-> Type -> Type
unChin Type
r
unChin (Type
l :=> Type
r) =        Type
l Type -> Type -> Type
:=> Type -> Type
unChin Type
r
unChin Type
t         = Type
t

-- mgu t t' = mgu' (toChin t) (toChin t')
mgu :: Type -> Type -> m Subst
mgu (Type
l :-> Type
r) (Type
l' :-> Type
r') = Type -> Type -> Type -> Type -> m Subst
forall (m :: * -> *).
MonadPlus m =>
Type -> Type -> Type -> Type -> m Subst
mgu2Ap Type
l Type
r Type
l' Type
r'
#ifdef REALDYNAMIC
-- $B5/$3$i$J$$$O$:$@$7!$8zN($r9M$($k$H(B....
mgu (l :-> r) (l' :> r')  = mgu2Ap l r l' r'
mgu (l :> r)  (l' :-> r') = mgu2Ap l r l' r'
mgu (l :> r)  (l' :> r')  = mgu2Ap l r l' r'
#endif
mgu (TA Type
l Type
r) (TA Type
l' Type
r') = Type -> Type -> Type -> Type -> m Subst
forall (m :: * -> *).
MonadPlus m =>
Type -> Type -> Type -> Type -> m Subst
mgu2Ap Type
l Type
r Type
l' Type
r'
mgu (TV TyCon
u)   Type
t        = TyCon -> Type -> m Subst
forall (m :: * -> *). MonadPlus m => TyCon -> Type -> m Subst
varBind TyCon
u Type
t
mgu Type
t        (TV TyCon
u)   = TyCon -> Type -> m Subst
forall (m :: * -> *). MonadPlus m => TyCon -> Type -> m Subst
varBind TyCon
u Type
t
mgu (TC TyCon
tc1) (TC TyCon
tc2) | TyCon
tc1TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
==TyCon
tc2 = Subst -> m Subst
forall (m :: * -> *) a. Monad m => a -> m a
return Subst
forall a. [a]
emptySubst
mgu Type
_        Type
_        = m Subst
forall (m :: * -> *) a. MonadPlus m => m a
mzero

mgu2Ap :: Type -> Type -> Type -> Type -> m Subst
mgu2Ap Type
l Type
r Type
l' Type
r' = do Subst
s1 <- Type -> Type -> m Subst
forall (m :: * -> *). MonadPlus m => Type -> Type -> m Subst
mgu Type
l Type
l'
                      Subst
s2 <- Type -> Type -> m Subst
forall (m :: * -> *). MonadPlus m => Type -> Type -> m Subst
mgu (Subst -> Type -> Type
apply Subst
s1 Type
r) (Subst -> Type -> Type
apply Subst
s1 Type
r')
                      Subst -> m Subst
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst
s2 Subst -> Subst -> Subst
`plusSubst` Subst
s1)

varBind :: MonadPlus m => TyVar -> Type -> m Subst
varBind :: TyCon -> Type -> m Subst
varBind TyCon
_ (Type
_:=>Type
_) = m Subst
forall (m :: * -> *) a. MonadPlus m => m a
mzero
varBind TyCon
u Type
t | Type
t Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon -> Type
TV TyCon
u                     = Subst -> m Subst
forall (m :: * -> *) a. Monad m => a -> m a
return Subst
forall a. [a]
emptySubst
            | TyCon
u TyCon -> [TyCon] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (Type -> [TyCon]
tyvars Type
t)           = m Subst
forall (m :: * -> *) a. MonadPlus m => m a
mzero
            | Bool
otherwise        = Subst -> m Subst
forall (m :: * -> *) a. Monad m => a -> m a
return (TyCon -> Type -> Subst
forall a b. a -> b -> [(a, b)]
unitSubst TyCon
u Type
t)

substOK :: Subst -> Bool
substOK :: Subst -> Bool
substOK = ((TyCon, Type) -> Bool) -> Subst -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\ (TyCon
i,Type
ty) -> Bool -> Bool
not (TyCon
i TyCon -> [TyCon] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (Type -> [TyCon]
tyvars Type
ty)))


assertsubst :: String -> Subst -> Subst
assertsubst :: String -> Subst -> Subst
assertsubst String
str = \Subst
s -> if Subst -> Bool
substOK Subst
s then Subst
s else String -> Subst
forall a. HasCallStack => String -> a
error (String
str String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
": assertsubst failed. substitution = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Subst -> String
forall a. Show a => a -> String
show Subst
s)
instance Show Type where
-- classes$B$rI=<($9$k$N$,$a$s$I$$!%:G=i$K$^$H$a$J$-$c%@%a(B? ReadType$B$N$H$3$m$G(BPrinter$B$G$d$C$H$-$c3Z$@$C$?$+$b!%(B
    showsPrec :: Int -> Type -> ShowS
showsPrec Int
_ Type
ty = Integer -> Type -> ShowS
forall t. (Show t, Num t) => t -> Type -> ShowS
toString' Integer
0 Type
ty -- The kind info can be incorrect, because we assume *.
        where toString' :: t -> Type -> ShowS
toString' t
k (TV TyCon
i)   = (Char
'a'Char -> ShowS
forall a. a -> [a] -> [a]
:) ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyCon -> ShowS
forall a. Show a => a -> ShowS
shows TyCon
i -- can be used to synthesize a generically typed program.
              toString' t
k (TC TyCon
i) = (Char
'K'Char -> ShowS
forall a. a -> [a] -> [a]
:) ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t -> ShowS
forall a. Show a => a -> ShowS
shows t
k ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char
'I'Char -> ShowS
forall a. a -> [a] -> [a]
:) ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyCon -> ShowS
forall a. Show a => a -> ShowS
shows TyCon
i
              toString' t
k (TA Type
t0 Type
t1)   = Bool -> ShowS -> ShowS
showParen Bool
True (t -> Type -> ShowS
toString' (t
kt -> t -> t
forall a. Num a => a -> a -> a
+t
1) Type
t0 ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char
' 'Char -> ShowS
forall a. a -> [a] -> [a]
:) ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t -> Type -> ShowS
toString' t
0 Type
t1) -- mandatory, just in case.
              toString' t
k (Type
t0 :=> Type
t1)    = Bool -> ShowS -> ShowS
showParen Bool
True (t -> Type -> ShowS
toString' t
0 Type
t0 ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String
"=>"String -> ShowS
forall a. [a] -> [a] -> [a]
++) ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t -> Type -> ShowS
toString' t
0 Type
t1)
              toString' t
k (Type
t0 :-> Type
t1)    = Bool -> ShowS -> ShowS
showParen Bool
True (t -> Type -> ShowS
toString' t
0 Type
t0 ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String
"->"String -> ShowS
forall a. [a] -> [a] -> [a]
++) ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t -> Type -> ShowS
toString' t
0 Type
t1)
              toString' t
k (Type
t0 :> Type
t1)   = Bool -> ShowS -> ShowS
showParen Bool
True ((String
"(->) "String -> ShowS
forall a. [a] -> [a] -> [a]
++) ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t -> Type -> ShowS
toString' t
0 Type
t0 ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char
' 'Char -> ShowS
forall a. a -> [a] -> [a]
:) ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t -> Type -> ShowS
toString' t
0 Type
t1)

plusSubst :: Subst -> Subst -> Subst
Subst
s0 plusSubst :: Subst -> Subst -> Subst
`plusSubst` Subst
s1 = [(TyCon
u, -- if u `elem` tvids t then error "u is in t" else
                         --         trace ("in plusSubst, s0="++show s0) $
                         Subst -> Type -> Type
applyCheck Subst
s0 Type
t) | (TyCon
u,Type
t) <- Subst
s1] Subst -> Subst -> Subst
forall a. [a] -> [a] -> [a]
++ Subst
s0


{-
prop_merge t0 t1 u0 u1 = mgu (t0:->t1) (u0:->u1) == ((do s0 <- mgu t0 u0
                                                         s1 <- mgu t1 u1
                                                         symPlus s0 s1) :: [Subst])
-}

-- $B=[4D$7$F$$$k>l9g$O(BplusSubst$B$,(Billegal$B$K$J$j$&$k(B
-- prop_PlusSubst s0 s1 = not (isIllegalSubst s0) && not (isIllegalSubst s1) ==> not (isIllegalSubst (s0 `plusSubst` s1))

-- apply$B$r(Bmap$B$7$?>e$G7k9g$7$J$$$H!$(BvarBind$B$7$?$H$-$KB?CJ3,$N=[4D$r%A%'%C%/$G$-$J$$!%(B
-- s1$B$r$d$C$?$"$H(Bs0$B$r(Bapply

-- applyHoge s t = if isIllegalSubst s then error "Illegal in applyHoge" else apply s t
lookupSubst :: MonadPlus m => Subst -> TyVar -> m Type
lookupSubst :: Subst -> TyCon -> m Type
lookupSubst Subst
subst TyCon
i = case TyCon -> Subst -> Maybe Type
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup TyCon
i Subst
subst of Maybe Type
Nothing -> m Type
forall (m :: * -> *) a. MonadPlus m => m a
mzero
                                             Just Type
x  -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
x

apply :: Subst -> Type -> Type
apply :: Subst -> Type -> Type
apply Subst
subst Type
ty = Type -> Type
apply' Type
ty
                                      where apply' :: Type -> Type
apply' tc :: Type
tc@(TC TyCon
_)    = Type
tc
                                            apply' tg :: Type
tg@(TV TyCon
tv)
                                                = case Subst -> TyCon -> Maybe Type
forall (m :: * -> *). MonadPlus m => Subst -> TyCon -> m Type
lookupSubst Subst
subst TyCon
tv of Just Type
tt -> Type
tt
                                                                               Maybe Type
Nothing -> Type
tg
                                            apply' (TA Type
t0 Type
t1) = Type -> Type -> Type
TA (Type -> Type
apply' Type
t0) (Type -> Type
apply' Type
t1)
                                            apply' (Type
t0:->Type
t1)  = Type -> Type
apply' Type
t0 Type -> Type -> Type
:-> Type -> Type
apply' Type
t1
                                            apply' (Type
t0:>Type
t1)   = Type -> Type
apply' Type
t0 Type -> Type -> Type
:>  Type -> Type
apply' Type
t1
                                            apply' (Type
t0:=>Type
t1)  = Type -> Type
apply' Type
t0 Type -> Type -> Type
:=> Type -> Type
apply' Type
t1

applyCheck :: Subst -> Type -> Type
applyCheck Subst
subst Type
t = -- trace ("t= " ++ show t ++ " and subst = "++ show subst) $
                     Subst -> Type -> Type
apply Subst
subst Type
t


-- moved from ReadType.lhs

{- This used to be Ok, but now I want to use Int8 for TyVar.
strToVarType str
    = TV (bakaHash str)
-- This is Ok, because eventually normalizeVarIDs will be called. (But there can be Int overflow....) Also, when I coded normalizeVarIDs I assumed the tvIDs are small.
bakaHash :: String -> TyVar
bakaHash []     = 0
bakaHash (c:cs) = fromIntegral (ord c) + bakaHash cs * 131
-}
\end{code}