-- | Runtime type representation of terms with support for rank-1 polymorphic
-- types with type variables of kind *.
--
-- The essence of this module is that we use the standard 'Typeable'
-- representation of "Data.Typeable" but we introduce a special (empty) data
-- type 'TypVar' which represents type variables. 'TypVar' is indexed by an
-- arbitrary other data type, giving you an unbounded number of type variables;
-- for convenience, we define 'ANY', 'ANY1', .., 'ANY9'.
--
-- [Examples of isInstanceOf]
--
-- > -- We CANNOT use a term of type 'Int -> Bool' as 'Int -> Int'
-- > > typeOf (undefined :: Int -> Int) `isInstanceOf` typeOf (undefined :: Int -> Bool)
-- > Left "Cannot unify Int and Bool"
-- >
-- > -- We CAN use a term of type 'forall a. a -> Int' as 'Int -> Int'
-- > > typeOf (undefined :: Int -> Int) `isInstanceOf` typeOf (undefined :: ANY -> Int)
-- > Right ()
-- >
-- > -- We CAN use a term of type 'forall a b. a -> b' as 'forall a. a -> a'
-- > > typeOf (undefined :: ANY -> ANY) `isInstanceOf` typeOf (undefined :: ANY -> ANY1)
-- > Right ()
-- >
-- > -- We CANNOT use a term of type 'forall a. a -> a' as 'forall a b. a -> b'
-- > > typeOf (undefined :: ANY -> ANY1) `isInstanceOf` typeOf (undefined :: ANY -> ANY)
-- > Left "Cannot unify Succ and Zero"
-- >
-- > -- We CAN use a term of type 'forall a. a' as 'forall a. a -> a'
-- > > typeOf (undefined :: ANY -> ANY) `isInstanceOf` typeOf (undefined :: ANY)
-- > Right ()
-- >
-- > -- We CANNOT use a term of type 'forall a. a -> a' as 'forall a. a'
-- > > typeOf (undefined :: ANY) `isInstanceOf` typeOf (undefined :: ANY -> ANY)
-- > Left "Cannot unify Skolem and ->"
--
-- (Admittedly, the quality of the type errors could be improved.)
--
-- [Examples of funResultTy]
--
-- > -- Apply fn of type (forall a. a -> a) to arg of type Bool gives Bool
-- > > funResultTy (typeOf (undefined :: ANY -> ANY)) (typeOf (undefined :: Bool))
-- > Right Bool
-- >
-- > -- Apply fn of type (forall a b. a -> b -> a) to arg of type Bool gives forall a. a -> Bool
-- > > funResultTy (typeOf (undefined :: ANY -> ANY1 -> ANY)) (typeOf (undefined :: Bool))
-- > Right (ANY -> Bool) -- forall a. a -> Bool
-- >
-- > -- Apply fn of type (forall a. (Bool -> a) -> a) to argument of type (forall a. a -> a) gives Bool
-- > > funResultTy (typeOf (undefined :: (Bool -> ANY) -> ANY)) (typeOf (undefined :: ANY -> ANY))
-- > Right Bool
-- >
-- > -- Apply fn of type (forall a b. a -> b -> a) to arg of type (forall a. a -> a) gives (forall a b. a -> b -> b)
-- > > funResultTy (typeOf (undefined :: ANY -> ANY1 -> ANY)) (typeOf (undefined :: ANY1 -> ANY1))
-- > Right (ANY -> ANY1 -> ANY1)
-- >
-- > -- Cannot apply function of type (forall a. (a -> a) -> a -> a) to arg of type (Int -> Bool)
-- > > funResultTy (typeOf (undefined :: (ANY -> ANY) -> (ANY -> ANY))) (typeOf (undefined :: Int -> Bool))
-- > Left "Cannot unify Int and Bool"
{-# LANGUAGE BangPatterns #-}
module Data.Rank1Typeable
  ( -- * Basic types
    TypeRep
  , typeOf
  , splitTyConApp
  , mkTyConApp
    -- * Operations on type representations
  , isInstanceOf
  , funResultTy
  , TypeError
    -- * Type variables
  , TypVar
  , Zero
  , Succ
  , V0
  , V1
  , V2
  , V3
  , V4
  , V5
  , V6
  , V7
  , V8
  , V9
  , ANY
  , ANY1
  , ANY2
  , ANY3
  , ANY4
  , ANY5
  , ANY6
  , ANY7
  , ANY8
  , ANY9
    -- * Re-exports from Typeable
  , Typeable
  ) where

import Prelude hiding (succ)
import Control.Arrow ((***), second)
import Control.Monad (void)
import Data.Binary
import Data.Function (on)
import Data.List (intersperse, isPrefixOf)
import Data.Maybe (fromMaybe)
import Data.Typeable ( Typeable )
import qualified Data.Typeable as T
import GHC.Fingerprint

tcList, tcFun :: TyCon
tcList :: TyCon
tcList = (TyCon, [TypeRep]) -> TyCon
forall a b. (a, b) -> a
fst ((TyCon, [TypeRep]) -> TyCon) -> (TyCon, [TypeRep]) -> TyCon
forall a b. (a -> b) -> a -> b
$ TypeRep -> (TyCon, [TypeRep])
splitTyConApp (TypeRep -> (TyCon, [TypeRep])) -> TypeRep -> (TyCon, [TypeRep])
forall a b. (a -> b) -> a -> b
$ [()] -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf [()]
tcFun :: TyCon
tcFun = (TyCon, [TypeRep]) -> TyCon
forall a b. (a, b) -> a
fst ((TyCon, [TypeRep]) -> TyCon) -> (TyCon, [TypeRep]) -> TyCon
forall a b. (a -> b) -> a -> b
$ TypeRep -> (TyCon, [TypeRep])
splitTyConApp (TypeRep -> (TyCon, [TypeRep])) -> TypeRep -> (TyCon, [TypeRep])
forall a b. (a -> b) -> a -> b
$ (() -> ()) -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf (\() -> ())

--------------------------------------------------------------------------------
-- The basic type                                                             --
--------------------------------------------------------------------------------

-- | Dynamic type representation with support for rank-1 types
data TypeRep
    = TRCon TyCon
    | TRApp {-# UNPACK #-} !Fingerprint TypeRep TypeRep

data TyCon = TyCon
    { TyCon -> Fingerprint
tyConFingerprint :: {-# UNPACK #-} !Fingerprint
    , TyCon -> TypeError
tyConPackage :: String
    , TyCon -> TypeError
tyConModule :: String
    , TyCon -> TypeError
tyConName :: String
    }

-- | The fingerprint of a TypeRep
typeRepFingerprint :: TypeRep -> Fingerprint
typeRepFingerprint :: TypeRep -> Fingerprint
typeRepFingerprint (TRCon TyCon
c) = TyCon -> Fingerprint
tyConFingerprint TyCon
c
typeRepFingerprint (TRApp Fingerprint
fp TypeRep
_ TypeRep
_) = Fingerprint
fp

-- | Compare two type representations
instance Eq TyCon where
  == :: TyCon -> TyCon -> Bool
(==) = Fingerprint -> Fingerprint -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Fingerprint -> Fingerprint -> Bool)
-> (TyCon -> Fingerprint) -> TyCon -> TyCon -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` TyCon -> Fingerprint
tyConFingerprint

instance Eq TypeRep where
  == :: TypeRep -> TypeRep -> Bool
(==) = Fingerprint -> Fingerprint -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Fingerprint -> Fingerprint -> Bool)
-> (TypeRep -> Fingerprint) -> TypeRep -> TypeRep -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` TypeRep -> Fingerprint
typeRepFingerprint

--- Binary instance for 'TypeRep', avoiding orphan instances
instance Binary TypeRep where
  put :: TypeRep -> Put
put (TypeRep -> (TyCon, [TypeRep])
splitTyConApp -> (TyCon
tc, [TypeRep]
ts)) = do
    TypeError -> Put
forall t. Binary t => t -> Put
put (TypeError -> Put) -> TypeError -> Put
forall a b. (a -> b) -> a -> b
$ TyCon -> TypeError
tyConPackage TyCon
tc
    TypeError -> Put
forall t. Binary t => t -> Put
put (TypeError -> Put) -> TypeError -> Put
forall a b. (a -> b) -> a -> b
$ TyCon -> TypeError
tyConModule TyCon
tc
    TypeError -> Put
forall t. Binary t => t -> Put
put (TypeError -> Put) -> TypeError -> Put
forall a b. (a -> b) -> a -> b
$ TyCon -> TypeError
tyConName TyCon
tc
    [TypeRep] -> Put
forall t. Binary t => t -> Put
put [TypeRep]
ts
  get :: Get TypeRep
get = do
    TypeError
package <- Get TypeError
forall t. Binary t => Get t
get
    TypeError
modul   <- Get TypeError
forall t. Binary t => Get t
get
    TypeError
name    <- Get TypeError
forall t. Binary t => Get t
get
    [TypeRep]
ts      <- Get [TypeRep]
forall t. Binary t => Get t
get
    TypeRep -> Get TypeRep
forall a. a -> Get a
forall (m :: * -> *) a. Monad m => a -> m a
return (TypeRep -> Get TypeRep) -> TypeRep -> Get TypeRep
forall a b. (a -> b) -> a -> b
$ TyCon -> [TypeRep] -> TypeRep
mkTyConApp (TypeError -> TypeError -> TypeError -> TyCon
mkTyCon3 TypeError
package TypeError
modul TypeError
name) [TypeRep]
ts

-- | The type representation of any 'Typeable' term
typeOf :: Typeable a => a -> TypeRep
typeOf :: forall a. Typeable a => a -> TypeRep
typeOf = TypeRep -> TypeRep
trTypeOf (TypeRep -> TypeRep) -> (a -> TypeRep) -> a -> TypeRep
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> TypeRep
forall a. Typeable a => a -> TypeRep
T.typeOf

-- | Conversion from Data.Typeable.TypeRep to Data.Rank1Typeable.TypeRep
trTypeOf :: T.TypeRep -> TypeRep
trTypeOf :: TypeRep -> TypeRep
trTypeOf TypeRep
t = let (TyCon
c, [TypeRep]
ts) = TypeRep -> (TyCon, [TypeRep])
T.splitTyConApp TypeRep
t
              in (TypeRep -> TypeRep -> TypeRep) -> TypeRep -> [TypeRep] -> TypeRep
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl TypeRep -> TypeRep -> TypeRep
mkTRApp (TyCon -> TypeRep
TRCon (TyCon -> TypeRep) -> TyCon -> TypeRep
forall a b. (a -> b) -> a -> b
$ TyCon -> TyCon
fromTypeableTyCon TyCon
c) ([TypeRep] -> TypeRep) -> [TypeRep] -> TypeRep
forall a b. (a -> b) -> a -> b
$ (TypeRep -> TypeRep) -> [TypeRep] -> [TypeRep]
forall a b. (a -> b) -> [a] -> [b]
map TypeRep -> TypeRep
trTypeOf [TypeRep]
ts
  where
    fromTypeableTyCon :: TyCon -> TyCon
fromTypeableTyCon TyCon
c =
      Fingerprint -> TypeError -> TypeError -> TypeError -> TyCon
TyCon (TyCon -> Fingerprint
T.tyConFingerprint TyCon
c)
            (TyCon -> TypeError
T.tyConPackage TyCon
c)
            (TyCon -> TypeError
T.tyConModule TyCon
c)
            (TyCon -> TypeError
T.tyConName TyCon
c)

-- | Applies a TypeRep to another.
mkTRApp :: TypeRep -> TypeRep -> TypeRep
mkTRApp :: TypeRep -> TypeRep -> TypeRep
mkTRApp TypeRep
t0 TypeRep
t1 = Fingerprint -> TypeRep -> TypeRep -> TypeRep
TRApp Fingerprint
fp TypeRep
t0 TypeRep
t1
  where
    fp :: Fingerprint
fp = [Fingerprint] -> Fingerprint
fingerprintFingerprints [TypeRep -> Fingerprint
typeRepFingerprint TypeRep
t0, TypeRep -> Fingerprint
typeRepFingerprint TypeRep
t1]

mkTyCon3 :: String -> String -> String -> TyCon
mkTyCon3 :: TypeError -> TypeError -> TypeError -> TyCon
mkTyCon3 TypeError
pkg TypeError
m TypeError
name = Fingerprint -> TypeError -> TypeError -> TypeError -> TyCon
TyCon Fingerprint
fp TypeError
pkg TypeError
m TypeError
name
  where
    fp :: Fingerprint
fp = [Fingerprint] -> Fingerprint
fingerprintFingerprints [ TypeError -> Fingerprint
fingerprintString TypeError
s | TypeError
s <- [TypeError
pkg, TypeError
m, TypeError
name] ]

--------------------------------------------------------------------------------
-- Constructors/destructors (views)                                           --
--------------------------------------------------------------------------------

-- | Split a type representation into the application of
-- a type constructor and its argument
splitTyConApp :: TypeRep -> (TyCon, [TypeRep])
splitTyConApp :: TypeRep -> (TyCon, [TypeRep])
splitTyConApp = [TypeRep] -> TypeRep -> (TyCon, [TypeRep])
go []
  where
    go :: [TypeRep] -> TypeRep -> (TyCon, [TypeRep])
go [TypeRep]
xs (TRCon TyCon
c) = (TyCon
c, [TypeRep]
xs)
    go [TypeRep]
xs (TRApp Fingerprint
_ TypeRep
t0 TypeRep
t1) = [TypeRep] -> TypeRep -> (TyCon, [TypeRep])
go (TypeRep
t1 TypeRep -> [TypeRep] -> [TypeRep]
forall a. a -> [a] -> [a]
: [TypeRep]
xs) TypeRep
t0

-- | Inverse of 'splitTyConApp'
mkTyConApp :: TyCon -> [TypeRep] -> TypeRep
mkTyConApp :: TyCon -> [TypeRep] -> TypeRep
mkTyConApp TyCon
c = (TypeRep -> TypeRep -> TypeRep) -> TypeRep -> [TypeRep] -> TypeRep
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl TypeRep -> TypeRep -> TypeRep
mkTRApp (TyCon -> TypeRep
TRCon TyCon
c)

isTypVar :: TypeRep -> Maybe Var
isTypVar :: TypeRep -> Maybe TypeRep
isTypVar (TypeRep -> (TyCon, [TypeRep])
splitTyConApp -> (TyCon
c, [TypeRep
t])) | TyCon
c TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
typVar = TypeRep -> Maybe TypeRep
forall a. a -> Maybe a
Just TypeRep
t
isTypVar TypeRep
_ = Maybe TypeRep
forall a. Maybe a
Nothing

mkTypVar :: Var -> TypeRep
mkTypVar :: TypeRep -> TypeRep
mkTypVar TypeRep
x = TyCon -> [TypeRep] -> TypeRep
mkTyConApp TyCon
typVar [TypeRep
x]

typVar :: TyCon
typVar :: TyCon
typVar = let (TyCon
c, [TypeRep]
_) = TypeRep -> (TyCon, [TypeRep])
splitTyConApp (TypVar V0 -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf (TypVar V0
forall a. HasCallStack => a
undefined :: TypVar V0)) in TyCon
c

skolem :: TyCon
skolem :: TyCon
skolem = let (TyCon
c, [TypeRep]
_) = TypeRep -> (TyCon, [TypeRep])
splitTyConApp (Skolem V0 -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf (Skolem V0
forall a. HasCallStack => a
undefined :: Skolem V0)) in TyCon
c

--------------------------------------------------------------------------------
-- Type variables                                                             --
--------------------------------------------------------------------------------

data TypVar a deriving Typeable
data Skolem a deriving Typeable
data Zero     deriving Typeable
data Succ a   deriving Typeable

type V0 = Zero
type V1 = Succ V0
type V2 = Succ V1
type V3 = Succ V2
type V4 = Succ V3
type V5 = Succ V4
type V6 = Succ V5
type V7 = Succ V6
type V8 = Succ V7
type V9 = Succ V8

type ANY  = TypVar V0
type ANY1 = TypVar V1
type ANY2 = TypVar V2
type ANY3 = TypVar V3
type ANY4 = TypVar V4
type ANY5 = TypVar V5
type ANY6 = TypVar V6
type ANY7 = TypVar V7
type ANY8 = TypVar V8
type ANY9 = TypVar V9

--------------------------------------------------------------------------------
-- Operations on type reps                                                    --
--------------------------------------------------------------------------------

-- | If 'isInstanceOf' fails it returns a type error
type TypeError = String

-- | @t1 `isInstanceOf` t2@ checks if @t1@ is an instance of @t2@
isInstanceOf :: TypeRep -> TypeRep -> Either TypeError ()
isInstanceOf :: TypeRep -> TypeRep -> Either TypeError ()
isInstanceOf TypeRep
t1 TypeRep
t2 = Either TypeError Substitution -> Either TypeError ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (TypeRep -> TypeRep -> Either TypeError Substitution
unify (TypeRep -> TypeRep
skolemize TypeRep
t1) TypeRep
t2)

-- | @funResultTy t1 t2@ is the type of the result when applying a function
-- of type @t1@ to an argument of type @t2@
funResultTy :: TypeRep -> TypeRep -> Either TypeError TypeRep
funResultTy :: TypeRep -> TypeRep -> Either TypeError TypeRep
funResultTy TypeRep
t1 TypeRep
t2 = do
  let anyTy :: TypeRep
anyTy = TypeRep -> TypeRep
mkTypVar (TypeRep -> TypeRep) -> TypeRep -> TypeRep
forall a b. (a -> b) -> a -> b
$ V0 -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf (V0
forall a. HasCallStack => a
undefined :: V0)
  Substitution
s <- TypeRep -> TypeRep -> Either TypeError Substitution
unify (TypeError -> TypeRep -> TypeRep
alphaRename TypeError
"f" TypeRep
t1) (TypeRep -> Either TypeError Substitution)
-> TypeRep -> Either TypeError Substitution
forall a b. (a -> b) -> a -> b
$ TyCon -> [TypeRep] -> TypeRep
mkTyConApp TyCon
tcFun [TypeError -> TypeRep -> TypeRep
alphaRename TypeError
"x" TypeRep
t2, TypeRep
anyTy]
  TypeRep -> Either TypeError TypeRep
forall a. a -> Either TypeError a
forall (m :: * -> *) a. Monad m => a -> m a
return (TypeRep -> Either TypeError TypeRep)
-> TypeRep -> Either TypeError TypeRep
forall a b. (a -> b) -> a -> b
$ TypeRep -> TypeRep
normalize (TypeRep -> TypeRep) -> TypeRep -> TypeRep
forall a b. (a -> b) -> a -> b
$ Substitution -> TypeRep -> TypeRep
subst Substitution
s TypeRep
anyTy

--------------------------------------------------------------------------------
-- Alpha-renaming and normalization                                           --
--------------------------------------------------------------------------------

alphaRename :: String -> TypeRep -> TypeRep
alphaRename :: TypeError -> TypeRep -> TypeRep
alphaRename TypeError
prefix (TypeRep -> Maybe TypeRep
isTypVar -> Just TypeRep
x) =
  TypeRep -> TypeRep
mkTypVar (TyCon -> [TypeRep] -> TypeRep
mkTyConApp (TypeError -> TyCon
mkTyCon TypeError
prefix) [TypeRep
x])
alphaRename TypeError
prefix (TypeRep -> (TyCon, [TypeRep])
splitTyConApp -> (TyCon
c, [TypeRep]
ts)) =
  TyCon -> [TypeRep] -> TypeRep
mkTyConApp TyCon
c ((TypeRep -> TypeRep) -> [TypeRep] -> [TypeRep]
forall a b. (a -> b) -> [a] -> [b]
map (TypeError -> TypeRep -> TypeRep
alphaRename TypeError
prefix) [TypeRep]
ts)

tvars :: TypeRep -> [Var]
tvars :: TypeRep -> [TypeRep]
tvars (TypeRep -> Maybe TypeRep
isTypVar -> Just TypeRep
x)       = [TypeRep
x]
tvars (TypeRep -> (TyCon, [TypeRep])
splitTyConApp -> (TyCon
_, [TypeRep]
ts)) = (TypeRep -> [TypeRep]) -> [TypeRep] -> [TypeRep]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap TypeRep -> [TypeRep]
tvars [TypeRep]
ts

normalize :: TypeRep -> TypeRep
normalize :: TypeRep -> TypeRep
normalize TypeRep
t = Substitution -> TypeRep -> TypeRep
subst ([TypeRep] -> [TypeRep] -> Substitution
forall a b. [a] -> [b] -> [(a, b)]
zip (TypeRep -> [TypeRep]
tvars TypeRep
t) [TypeRep]
anys) TypeRep
t
  where
    anys :: [TypeRep]
    anys :: [TypeRep]
anys = (TypeRep -> TypeRep) -> [TypeRep] -> [TypeRep]
forall a b. (a -> b) -> [a] -> [b]
map TypeRep -> TypeRep
mkTypVar ((TypeRep -> TypeRep) -> TypeRep -> [TypeRep]
forall a. (a -> a) -> a -> [a]
iterate TypeRep -> TypeRep
succ TypeRep
zero)

    succ :: TypeRep -> TypeRep
    succ :: TypeRep -> TypeRep
succ = TyCon -> [TypeRep] -> TypeRep
mkTyConApp TyCon
succTyCon ([TypeRep] -> TypeRep)
-> (TypeRep -> [TypeRep]) -> TypeRep -> TypeRep
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TypeRep -> [TypeRep] -> [TypeRep]
forall a. a -> [a] -> [a]
:[])

    zero :: TypeRep
    zero :: TypeRep
zero = TyCon -> [TypeRep] -> TypeRep
mkTyConApp TyCon
zeroTyCon []

mkTyCon :: String -> TyCon
mkTyCon :: TypeError -> TyCon
mkTyCon = TypeError -> TypeError -> TypeError -> TyCon
mkTyCon3 TypeError
"rank1typeable" TypeError
"Data.Rank1Typeable"

succTyCon :: TyCon
succTyCon :: TyCon
succTyCon = let (TyCon
c, [TypeRep]
_) = TypeRep -> (TyCon, [TypeRep])
splitTyConApp (Succ V0 -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf (Succ V0
forall a. HasCallStack => a
undefined :: Succ Zero)) in TyCon
c

zeroTyCon :: TyCon
zeroTyCon :: TyCon
zeroTyCon = let (TyCon
c, [TypeRep]
_) = TypeRep -> (TyCon, [TypeRep])
splitTyConApp (V0 -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf (V0
forall a. HasCallStack => a
undefined :: Zero)) in TyCon
c

--------------------------------------------------------------------------------
-- Unification                                                                --
--------------------------------------------------------------------------------

type Substitution = [(Var, TypeRep)]
type Equation     = (TypeRep, TypeRep)
type Var          = TypeRep

skolemize :: TypeRep -> TypeRep
skolemize :: TypeRep -> TypeRep
skolemize (TypeRep -> Maybe TypeRep
isTypVar -> Just TypeRep
x)       = TyCon -> [TypeRep] -> TypeRep
mkTyConApp TyCon
skolem [TypeRep
x]
skolemize (TypeRep -> (TyCon, [TypeRep])
splitTyConApp -> (TyCon
c, [TypeRep]
ts)) = TyCon -> [TypeRep] -> TypeRep
mkTyConApp TyCon
c ((TypeRep -> TypeRep) -> [TypeRep] -> [TypeRep]
forall a b. (a -> b) -> [a] -> [b]
map TypeRep -> TypeRep
skolemize [TypeRep]
ts)

occurs :: Var -> TypeRep -> Bool
occurs :: TypeRep -> TypeRep -> Bool
occurs TypeRep
x (TypeRep -> Maybe TypeRep
isTypVar -> Just TypeRep
x')      = TypeRep
x TypeRep -> TypeRep -> Bool
forall a. Eq a => a -> a -> Bool
== TypeRep
x'
occurs TypeRep
x (TypeRep -> (TyCon, [TypeRep])
splitTyConApp -> (TyCon
_, [TypeRep]
ts)) = (TypeRep -> Bool) -> [TypeRep] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (TypeRep -> TypeRep -> Bool
occurs TypeRep
x) [TypeRep]
ts

subst :: Substitution -> TypeRep -> TypeRep
subst :: Substitution -> TypeRep -> TypeRep
subst Substitution
s (TypeRep -> Maybe TypeRep
isTypVar -> Just TypeRep
x)       = TypeRep -> Maybe TypeRep -> TypeRep
forall a. a -> Maybe a -> a
fromMaybe (TypeRep -> TypeRep
mkTypVar TypeRep
x) (TypeRep -> Substitution -> Maybe TypeRep
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup TypeRep
x Substitution
s)
subst Substitution
s (TypeRep -> (TyCon, [TypeRep])
splitTyConApp -> (TyCon
c, [TypeRep]
ts)) = TyCon -> [TypeRep] -> TypeRep
mkTyConApp TyCon
c ((TypeRep -> TypeRep) -> [TypeRep] -> [TypeRep]
forall a b. (a -> b) -> [a] -> [b]
map (Substitution -> TypeRep -> TypeRep
subst Substitution
s) [TypeRep]
ts)

unify :: TypeRep
      -> TypeRep
      -> Either TypeError Substitution
unify :: TypeRep -> TypeRep -> Either TypeError Substitution
unify = \TypeRep
t1 TypeRep
t2 -> Substitution -> Substitution -> Either TypeError Substitution
go [] [(TypeRep
t1, TypeRep
t2)]
  where
    go :: Substitution
       -> [Equation]
       -> Either TypeError Substitution
    go :: Substitution -> Substitution -> Either TypeError Substitution
go Substitution
acc [] =
      Substitution -> Either TypeError Substitution
forall a. a -> Either TypeError a
forall (m :: * -> *) a. Monad m => a -> m a
return Substitution
acc
    go Substitution
acc ((TypeRep
t1, TypeRep
t2) : Substitution
eqs) | TypeRep
t1 TypeRep -> TypeRep -> Bool
forall a. Eq a => a -> a -> Bool
== TypeRep
t2 = -- Note: equality check is fast
      Substitution -> Substitution -> Either TypeError Substitution
go Substitution
acc Substitution
eqs
    go Substitution
acc ((TypeRep -> Maybe TypeRep
isTypVar -> Just TypeRep
x, TypeRep
t) : Substitution
eqs) =
      if TypeRep
x TypeRep -> TypeRep -> Bool
`occurs` TypeRep
t
        then TypeError -> Either TypeError Substitution
forall a b. a -> Either a b
Left TypeError
"Occurs check"
        else Substitution -> Substitution -> Either TypeError Substitution
go ((TypeRep
x, TypeRep
t) (TypeRep, TypeRep) -> Substitution -> Substitution
forall a. a -> [a] -> [a]
: ((TypeRep, TypeRep) -> (TypeRep, TypeRep))
-> Substitution -> Substitution
forall a b. (a -> b) -> [a] -> [b]
map ((TypeRep -> TypeRep) -> (TypeRep, TypeRep) -> (TypeRep, TypeRep)
forall b c d. (b -> c) -> (d, b) -> (d, c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second ((TypeRep -> TypeRep) -> (TypeRep, TypeRep) -> (TypeRep, TypeRep))
-> (TypeRep -> TypeRep) -> (TypeRep, TypeRep) -> (TypeRep, TypeRep)
forall a b. (a -> b) -> a -> b
$ Substitution -> TypeRep -> TypeRep
subst [(TypeRep
x, TypeRep
t)]) Substitution
acc)
                (((TypeRep, TypeRep) -> (TypeRep, TypeRep))
-> Substitution -> Substitution
forall a b. (a -> b) -> [a] -> [b]
map (Substitution -> TypeRep -> TypeRep
subst [(TypeRep
x, TypeRep
t)] (TypeRep -> TypeRep)
-> (TypeRep -> TypeRep) -> (TypeRep, TypeRep) -> (TypeRep, TypeRep)
forall b c b' c'. (b -> c) -> (b' -> c') -> (b, b') -> (c, c')
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** Substitution -> TypeRep -> TypeRep
subst [(TypeRep
x, TypeRep
t)]) Substitution
eqs)
    go Substitution
acc ((TypeRep
t, TypeRep -> Maybe TypeRep
isTypVar -> Just TypeRep
x) : Substitution
eqs) =
      Substitution -> Substitution -> Either TypeError Substitution
go Substitution
acc ((TypeRep -> TypeRep
mkTypVar TypeRep
x, TypeRep
t) (TypeRep, TypeRep) -> Substitution -> Substitution
forall a. a -> [a] -> [a]
: Substitution
eqs)
    go Substitution
acc ((TypeRep -> (TyCon, [TypeRep])
splitTyConApp -> (TyCon
c1, [TypeRep]
ts1), TypeRep -> (TyCon, [TypeRep])
splitTyConApp -> (TyCon
c2, [TypeRep]
ts2)) : Substitution
eqs) =
      if TyCon
c1 TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
/= TyCon
c2
        then TypeError -> Either TypeError Substitution
forall a b. a -> Either a b
Left (TypeError -> Either TypeError Substitution)
-> TypeError -> Either TypeError Substitution
forall a b. (a -> b) -> a -> b
$ TypeError
"Cannot unify " TypeError -> TypeError -> TypeError
forall a. [a] -> [a] -> [a]
++ TyCon -> TypeError
forall a. Show a => a -> TypeError
show TyCon
c1 TypeError -> TypeError -> TypeError
forall a. [a] -> [a] -> [a]
++ TypeError
" and " TypeError -> TypeError -> TypeError
forall a. [a] -> [a] -> [a]
++ TyCon -> TypeError
forall a. Show a => a -> TypeError
show TyCon
c2
        else Substitution -> Substitution -> Either TypeError Substitution
go Substitution
acc ([TypeRep] -> [TypeRep] -> Substitution
forall a b. [a] -> [b] -> [(a, b)]
zip [TypeRep]
ts1 [TypeRep]
ts2 Substitution -> Substitution -> Substitution
forall a. [a] -> [a] -> [a]
++ Substitution
eqs)

--------------------------------------------------------------------------------
-- Pretty-printing                                                            --
--------------------------------------------------------------------------------

instance Show TyCon where
  showsPrec :: Int -> TyCon -> TypeError -> TypeError
showsPrec Int
_ TyCon
c = TypeError -> TypeError -> TypeError
showString (TyCon -> TypeError
tyConName TyCon
c)

instance Show TypeRep where
  showsPrec :: Int -> TypeRep -> TypeError -> TypeError
showsPrec Int
p (TypeRep -> (TyCon, [TypeRep])
splitTyConApp -> (TyCon
tycon, [TypeRep]
tys)) =
      case [TypeRep]
tys of
        [] -> Int -> TyCon -> TypeError -> TypeError
forall a. Show a => Int -> a -> TypeError -> TypeError
showsPrec Int
p TyCon
tycon
        [TypeRep -> Maybe Int
anyIdx -> Just Int
i] | TyCon
tycon TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
typVar -> TypeError -> TypeError -> TypeError
showString TypeError
"ANY" (TypeError -> TypeError)
-> (TypeError -> TypeError) -> TypeError -> TypeError
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> TypeError -> TypeError
forall {a}. (Eq a, Num a, Show a) => a -> TypeError -> TypeError
showIdx Int
i
        [TypeRep
x] | TyCon
tycon TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tcList ->
          Char -> TypeError -> TypeError
showChar Char
'[' (TypeError -> TypeError)
-> (TypeError -> TypeError) -> TypeError -> TypeError
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeRep -> TypeError -> TypeError
forall a. Show a => a -> TypeError -> TypeError
shows TypeRep
x (TypeError -> TypeError)
-> (TypeError -> TypeError) -> TypeError -> TypeError
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> TypeError -> TypeError
showChar Char
']'
        [TypeRep
a,TypeRep
r] | TyCon
tycon TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tcFun ->
          Bool -> (TypeError -> TypeError) -> TypeError -> TypeError
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
8) ((TypeError -> TypeError) -> TypeError -> TypeError)
-> (TypeError -> TypeError) -> TypeError -> TypeError
forall a b. (a -> b) -> a -> b
$ Int -> TypeRep -> TypeError -> TypeError
forall a. Show a => Int -> a -> TypeError -> TypeError
showsPrec Int
9 TypeRep
a
                            (TypeError -> TypeError)
-> (TypeError -> TypeError) -> TypeError -> TypeError
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeError -> TypeError -> TypeError
showString TypeError
" -> "
                            (TypeError -> TypeError)
-> (TypeError -> TypeError) -> TypeError -> TypeError
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> TypeRep -> TypeError -> TypeError
forall a. Show a => Int -> a -> TypeError -> TypeError
showsPrec Int
8 TypeRep
r
        [TypeRep]
xs | TyCon -> Bool
isTupleTyCon TyCon
tycon ->
          [TypeRep] -> TypeError -> TypeError
showTuple [TypeRep]
xs
        [TypeRep]
_ ->
          Bool -> (TypeError -> TypeError) -> TypeError -> TypeError
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9) ((TypeError -> TypeError) -> TypeError -> TypeError)
-> (TypeError -> TypeError) -> TypeError -> TypeError
forall a b. (a -> b) -> a -> b
$ Int -> TyCon -> TypeError -> TypeError
forall a. Show a => Int -> a -> TypeError -> TypeError
showsPrec Int
p TyCon
tycon
                            (TypeError -> TypeError)
-> (TypeError -> TypeError) -> TypeError -> TypeError
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> TypeError -> TypeError
showChar Char
' '
                            (TypeError -> TypeError)
-> (TypeError -> TypeError) -> TypeError -> TypeError
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [TypeRep] -> TypeError -> TypeError
forall a. Show a => [a] -> TypeError -> TypeError
showArgs [TypeRep]
tys
    where
      showIdx :: a -> TypeError -> TypeError
showIdx a
0 = TypeError -> TypeError -> TypeError
showString TypeError
""
      showIdx a
i = a -> TypeError -> TypeError
forall a. Show a => a -> TypeError -> TypeError
shows a
i

showArgs :: Show a => [a] -> ShowS
showArgs :: forall a. Show a => [a] -> TypeError -> TypeError
showArgs [] = TypeError -> TypeError
forall a. a -> a
id
showArgs [a
a] = Int -> a -> TypeError -> TypeError
forall a. Show a => Int -> a -> TypeError -> TypeError
showsPrec Int
10 a
a
showArgs (a
a:[a]
as) = Int -> a -> TypeError -> TypeError
forall a. Show a => Int -> a -> TypeError -> TypeError
showsPrec Int
10 a
a (TypeError -> TypeError)
-> (TypeError -> TypeError) -> TypeError -> TypeError
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeError -> TypeError -> TypeError
showString TypeError
" " (TypeError -> TypeError)
-> (TypeError -> TypeError) -> TypeError -> TypeError
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> TypeError -> TypeError
forall a. Show a => [a] -> TypeError -> TypeError
showArgs [a]
as

anyIdx :: TypeRep -> Maybe Int
anyIdx :: TypeRep -> Maybe Int
anyIdx (TypeRep -> (TyCon, [TypeRep])
splitTyConApp -> (TyCon
c, []))  | TyCon
c TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
zeroTyCon = Int -> Maybe Int
forall a. a -> Maybe a
Just Int
0
anyIdx (TypeRep -> (TyCon, [TypeRep])
splitTyConApp -> (TyCon
c, [TypeRep
t])) | TyCon
c TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
succTyCon = (Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) (Int -> Int) -> Maybe Int -> Maybe Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeRep -> Maybe Int
anyIdx TypeRep
t
anyIdx TypeRep
_ = Maybe Int
forall a. Maybe a
Nothing

showTuple :: [TypeRep] -> ShowS
showTuple :: [TypeRep] -> TypeError -> TypeError
showTuple [TypeRep]
args = Char -> TypeError -> TypeError
showChar Char
'('
               (TypeError -> TypeError)
-> (TypeError -> TypeError) -> TypeError -> TypeError
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((TypeError -> TypeError)
 -> (TypeError -> TypeError) -> TypeError -> TypeError)
-> (TypeError -> TypeError)
-> [TypeError -> TypeError]
-> TypeError
-> TypeError
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (TypeError -> TypeError)
-> (TypeError -> TypeError) -> TypeError -> TypeError
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) TypeError -> TypeError
forall a. a -> a
id ( (TypeError -> TypeError)
-> [TypeError -> TypeError] -> [TypeError -> TypeError]
forall a. a -> [a] -> [a]
intersperse (Char -> TypeError -> TypeError
showChar Char
',')
                              ([TypeError -> TypeError] -> [TypeError -> TypeError])
-> [TypeError -> TypeError] -> [TypeError -> TypeError]
forall a b. (a -> b) -> a -> b
$ (TypeRep -> TypeError -> TypeError)
-> [TypeRep] -> [TypeError -> TypeError]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> TypeRep -> TypeError -> TypeError
forall a. Show a => Int -> a -> TypeError -> TypeError
showsPrec Int
10) [TypeRep]
args
                              )
               (TypeError -> TypeError)
-> (TypeError -> TypeError) -> TypeError -> TypeError
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> TypeError -> TypeError
showChar Char
')'

isTupleTyCon :: TyCon -> Bool
isTupleTyCon :: TyCon -> Bool
isTupleTyCon = TypeError -> TypeError -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf TypeError
"(," (TypeError -> Bool) -> (TyCon -> TypeError) -> TyCon -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyCon -> TypeError
tyConName