Safe Haskell	Safe-Inferred
Language	Haskell2010

TypeChecker.HindleyMilner

Contents

Type
UType
Polytype
Converters
Infer
FreeVars
Errors
Orphan instances

Synopsis

data TypeF a
- = TVarF Identifier
- | TUnitF
- | TBoolF
- | TIntF
- | TFunF a a
type UType = UTerm TypeF IntVar
data UTerm (t :: Type -> Type) v where
- pattern UTVar :: Identifier -> UType
- pattern UTUnit :: UType
- pattern UTBool :: UType
- pattern UTInt :: UType
- pattern UTFun :: UType -> UType -> UType
data UTerm (t :: Type -> Type) v where
- pattern UTVar :: Identifier -> UType
- pattern UTUnit :: UType
- pattern UTBool :: UType
- pattern UTInt :: UType
- pattern UTFun :: UType -> UType -> UType
data UTerm (t :: Type -> Type) v where
- pattern UTVar :: Identifier -> UType
- pattern UTUnit :: UType
- pattern UTBool :: UType
- pattern UTInt :: UType
- pattern UTFun :: UType -> UType -> UType
data UTerm (t :: Type -> Type) v where
- pattern UTVar :: Identifier -> UType
- pattern UTUnit :: UType
- pattern UTBool :: UType
- pattern UTInt :: UType
- pattern UTFun :: UType -> UType -> UType
data UTerm (t :: Type -> Type) v where
- pattern UTVar :: Identifier -> UType
- pattern UTUnit :: UType
- pattern UTBool :: UType
- pattern UTInt :: UType
- pattern UTFun :: UType -> UType -> UType
data Poly t = Forall [Identifier] t
type Polytype = Poly Type
toUType :: Type -> UType
toPolytype :: UPolytype -> Polytype
type Infer = ReaderT Ctx (ExceptT TypeError (IntBindingT TypeF Identity))
lookup :: Identifier -> Infer UType
withBinding :: MonadReader Ctx m => Identifier -> UPolytype -> m a -> m a
fresh :: Infer UType
data TypeError where
- Unreachable :: TypeError
- UnboundVar :: Identifier -> TypeError
- Infinite :: IntVar -> UType -> TypeError
- ImpossibleBinOpApplication :: UType -> UType -> TypeError
- ImpossibleUnOpApplication :: UType -> TypeError
- Mismatch :: TypeF UType -> TypeF UType -> TypeError
(=:=) :: UType -> UType -> Infer UType
applyBindings :: UType -> Infer UType
mkVarName :: String -> IntVar -> Identifier
generalize :: UType -> Infer UPolytype

Type

data TypeF a Source #

Constructors

TVarF Identifier
TUnitF
TBoolF
TIntF
TFunF a a

Instances

Instances details

Foldable TypeF Source #
Instance details Defined in TypeChecker.HindleyMilner Methods fold :: Monoid m => TypeF m -> m # foldMap :: Monoid m => (a -> m) -> TypeF a -> m # foldMap' :: Monoid m => (a -> m) -> TypeF a -> m # foldr :: (a -> b -> b) -> b -> TypeF a -> b # foldr' :: (a -> b -> b) -> b -> TypeF a -> b # foldl :: (b -> a -> b) -> b -> TypeF a -> b # foldl' :: (b -> a -> b) -> b -> TypeF a -> b # foldr1 :: (a -> a -> a) -> TypeF a -> a # foldl1 :: (a -> a -> a) -> TypeF a -> a # toList :: TypeF a -> [a] # null :: TypeF a -> Bool # length :: TypeF a -> Int # elem :: Eq a => a -> TypeF a -> Bool # maximum :: Ord a => TypeF a -> a # minimum :: Ord a => TypeF a -> a # sum :: Num a => TypeF a -> a # product :: Num a => TypeF a -> a #
Traversable TypeF Source #
Instance details Defined in TypeChecker.HindleyMilner Methods traverse :: Applicative f => (a -> f b) -> TypeF a -> f (TypeF b) # sequenceA :: Applicative f => TypeF (f a) -> f (TypeF a) # mapM :: Monad m => (a -> m b) -> TypeF a -> m (TypeF b) # sequence :: Monad m => TypeF (m a) -> m (TypeF a) #
Functor TypeF Source #
Instance details Defined in TypeChecker.HindleyMilner Methods fmap :: (a -> b) -> TypeF a -> TypeF b # (<$) :: a -> TypeF b -> TypeF a #
Unifiable TypeF Source #
Instance details Defined in TypeChecker.HindleyMilner Methods zipMatch :: TypeF a -> TypeF a -> Maybe (TypeF (Either a (a, a))) #
Generic1 TypeF Source #
Instance details Defined in TypeChecker.HindleyMilner Associated Types type Rep1 TypeF :: k -> Type # Methods from1 :: forall (a :: k). TypeF a -> Rep1 TypeF a # to1 :: forall (a :: k). Rep1 TypeF a -> TypeF a #
Fallible TypeF IntVar TypeError Source #
Instance details Defined in TypeChecker.HindleyMilner Methods occursFailure :: IntVar -> UTerm TypeF IntVar -> TypeError # mismatchFailure :: TypeF (UTerm TypeF IntVar) -> TypeF (UTerm TypeF IntVar) -> TypeError #
Show a => Show (TypeF a) Source #
Instance details Defined in TypeChecker.HindleyMilner Methods showsPrec :: Int -> TypeF a -> ShowS # show :: TypeF a -> String # showList :: [TypeF a] -> ShowS #
Eq a => Eq (TypeF a) Source #
Instance details Defined in TypeChecker.HindleyMilner Methods (==) :: TypeF a -> TypeF a -> Bool # (/=) :: TypeF a -> TypeF a -> Bool #
type Rep1 TypeF Source #
Instance details Defined in TypeChecker.HindleyMilner type Rep1 TypeF = D1 ('MetaData "TypeF" "TypeChecker.HindleyMilner" "mini-ml-0.1.0.0-inplace" 'False) ((C1 ('MetaCons "TVarF" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Identifier)) :+: C1 ('MetaCons "TUnitF" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "TBoolF" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "TIntF" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TFunF" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) Par1 :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) Par1))))

UType

type UType = UTerm TypeF IntVar Source #

data UTerm (t :: Type -> Type) v where #

The type of terms generated by structures t over variables v. The structure type should implement Unifiable and the variable type should implement Variable.

The Show instance doesn't show the constructors, in order to improve legibility for large terms.

All the category theoretic instances (Functor, Foldable, Traversable,...) are provided because they are often useful; however, beware that since the implementations must be pure, they cannot read variables bound in the current context and therefore can create incoherent results. Therefore, you should apply the current bindings before using any of the functions provided by those classes.

Bundled Patterns

pattern UTVar :: Identifier -> UType
pattern UTUnit :: UType
pattern UTBool :: UType
pattern UTInt :: UType
pattern UTFun :: UType -> UType -> UType

Instances

Instances details

Foldable t => Foldable (UTerm t)
Instance details Defined in Control.Unification.Types Methods fold :: Monoid m => UTerm t m -> m # foldMap :: Monoid m => (a -> m) -> UTerm t a -> m # foldMap' :: Monoid m => (a -> m) -> UTerm t a -> m # foldr :: (a -> b -> b) -> b -> UTerm t a -> b # foldr' :: (a -> b -> b) -> b -> UTerm t a -> b # foldl :: (b -> a -> b) -> b -> UTerm t a -> b # foldl' :: (b -> a -> b) -> b -> UTerm t a -> b # foldr1 :: (a -> a -> a) -> UTerm t a -> a # foldl1 :: (a -> a -> a) -> UTerm t a -> a # toList :: UTerm t a -> [a] # null :: UTerm t a -> Bool # length :: UTerm t a -> Int # elem :: Eq a => a -> UTerm t a -> Bool # maximum :: Ord a => UTerm t a -> a # minimum :: Ord a => UTerm t a -> a # sum :: Num a => UTerm t a -> a # product :: Num a => UTerm t a -> a #
Traversable t => Traversable (UTerm t)
Instance details Defined in Control.Unification.Types Methods traverse :: Applicative f => (a -> f b) -> UTerm t a -> f (UTerm t b) # sequenceA :: Applicative f => UTerm t (f a) -> f (UTerm t a) # mapM :: Monad m => (a -> m b) -> UTerm t a -> m (UTerm t b) # sequence :: Monad m => UTerm t (m a) -> m (UTerm t a) #
Functor t => Applicative (UTerm t)
Instance details Defined in Control.Unification.Types Methods pure :: a -> UTerm t a # (<>) :: UTerm t (a -> b) -> UTerm t a -> UTerm t b # liftA2 :: (a -> b -> c) -> UTerm t a -> UTerm t b -> UTerm t c # (>) :: UTerm t a -> UTerm t b -> UTerm t b # (<*) :: UTerm t a -> UTerm t b -> UTerm t a #
Functor t => Functor (UTerm t)
Instance details Defined in Control.Unification.Types Methods fmap :: (a -> b) -> UTerm t a -> UTerm t b # (<$) :: a -> UTerm t b -> UTerm t a #
Functor t => Monad (UTerm t)
Instance details Defined in Control.Unification.Types Methods (>>=) :: UTerm t a -> (a -> UTerm t b) -> UTerm t b # (>>) :: UTerm t a -> UTerm t b -> UTerm t b # return :: a -> UTerm t a #
(Show v, Show (t (UTerm t v))) => Show (UTerm t v)
Instance details Defined in Control.Unification.Types Methods showsPrec :: Int -> UTerm t v -> ShowS # show :: UTerm t v -> String # showList :: [UTerm t v] -> ShowS #

data UTerm (t :: Type -> Type) v where #

The type of terms generated by structures t over variables v. The structure type should implement Unifiable and the variable type should implement Variable.

The Show instance doesn't show the constructors, in order to improve legibility for large terms.

All the category theoretic instances (Functor, Foldable, Traversable,...) are provided because they are often useful; however, beware that since the implementations must be pure, they cannot read variables bound in the current context and therefore can create incoherent results. Therefore, you should apply the current bindings before using any of the functions provided by those classes.

Bundled Patterns

pattern UTVar :: Identifier -> UType
pattern UTUnit :: UType
pattern UTBool :: UType
pattern UTInt :: UType
pattern UTFun :: UType -> UType -> UType

Instances

Instances details

Foldable t => Foldable (UTerm t)
Instance details Defined in Control.Unification.Types Methods fold :: Monoid m => UTerm t m -> m # foldMap :: Monoid m => (a -> m) -> UTerm t a -> m # foldMap' :: Monoid m => (a -> m) -> UTerm t a -> m # foldr :: (a -> b -> b) -> b -> UTerm t a -> b # foldr' :: (a -> b -> b) -> b -> UTerm t a -> b # foldl :: (b -> a -> b) -> b -> UTerm t a -> b # foldl' :: (b -> a -> b) -> b -> UTerm t a -> b # foldr1 :: (a -> a -> a) -> UTerm t a -> a # foldl1 :: (a -> a -> a) -> UTerm t a -> a # toList :: UTerm t a -> [a] # null :: UTerm t a -> Bool # length :: UTerm t a -> Int # elem :: Eq a => a -> UTerm t a -> Bool # maximum :: Ord a => UTerm t a -> a # minimum :: Ord a => UTerm t a -> a # sum :: Num a => UTerm t a -> a # product :: Num a => UTerm t a -> a #
Traversable t => Traversable (UTerm t)
Instance details Defined in Control.Unification.Types Methods traverse :: Applicative f => (a -> f b) -> UTerm t a -> f (UTerm t b) # sequenceA :: Applicative f => UTerm t (f a) -> f (UTerm t a) # mapM :: Monad m => (a -> m b) -> UTerm t a -> m (UTerm t b) # sequence :: Monad m => UTerm t (m a) -> m (UTerm t a) #
Functor t => Applicative (UTerm t)
Instance details Defined in Control.Unification.Types Methods pure :: a -> UTerm t a # (<>) :: UTerm t (a -> b) -> UTerm t a -> UTerm t b # liftA2 :: (a -> b -> c) -> UTerm t a -> UTerm t b -> UTerm t c # (>) :: UTerm t a -> UTerm t b -> UTerm t b # (<*) :: UTerm t a -> UTerm t b -> UTerm t a #
Functor t => Functor (UTerm t)
Instance details Defined in Control.Unification.Types Methods fmap :: (a -> b) -> UTerm t a -> UTerm t b # (<$) :: a -> UTerm t b -> UTerm t a #
Functor t => Monad (UTerm t)
Instance details Defined in Control.Unification.Types Methods (>>=) :: UTerm t a -> (a -> UTerm t b) -> UTerm t b # (>>) :: UTerm t a -> UTerm t b -> UTerm t b # return :: a -> UTerm t a #
(Show v, Show (t (UTerm t v))) => Show (UTerm t v)
Instance details Defined in Control.Unification.Types Methods showsPrec :: Int -> UTerm t v -> ShowS # show :: UTerm t v -> String # showList :: [UTerm t v] -> ShowS #

data UTerm (t :: Type -> Type) v where #

The type of terms generated by structures t over variables v. The structure type should implement Unifiable and the variable type should implement Variable.

The Show instance doesn't show the constructors, in order to improve legibility for large terms.

All the category theoretic instances (Functor, Foldable, Traversable,...) are provided because they are often useful; however, beware that since the implementations must be pure, they cannot read variables bound in the current context and therefore can create incoherent results. Therefore, you should apply the current bindings before using any of the functions provided by those classes.

Bundled Patterns

pattern UTVar :: Identifier -> UType
pattern UTUnit :: UType
pattern UTBool :: UType
pattern UTInt :: UType
pattern UTFun :: UType -> UType -> UType

Instances

Instances details

Foldable t => Foldable (UTerm t)
Instance details Defined in Control.Unification.Types Methods fold :: Monoid m => UTerm t m -> m # foldMap :: Monoid m => (a -> m) -> UTerm t a -> m # foldMap' :: Monoid m => (a -> m) -> UTerm t a -> m # foldr :: (a -> b -> b) -> b -> UTerm t a -> b # foldr' :: (a -> b -> b) -> b -> UTerm t a -> b # foldl :: (b -> a -> b) -> b -> UTerm t a -> b # foldl' :: (b -> a -> b) -> b -> UTerm t a -> b # foldr1 :: (a -> a -> a) -> UTerm t a -> a # foldl1 :: (a -> a -> a) -> UTerm t a -> a # toList :: UTerm t a -> [a] # null :: UTerm t a -> Bool # length :: UTerm t a -> Int # elem :: Eq a => a -> UTerm t a -> Bool # maximum :: Ord a => UTerm t a -> a # minimum :: Ord a => UTerm t a -> a # sum :: Num a => UTerm t a -> a # product :: Num a => UTerm t a -> a #
Traversable t => Traversable (UTerm t)
Instance details Defined in Control.Unification.Types Methods traverse :: Applicative f => (a -> f b) -> UTerm t a -> f (UTerm t b) # sequenceA :: Applicative f => UTerm t (f a) -> f (UTerm t a) # mapM :: Monad m => (a -> m b) -> UTerm t a -> m (UTerm t b) # sequence :: Monad m => UTerm t (m a) -> m (UTerm t a) #
Functor t => Applicative (UTerm t)
Instance details Defined in Control.Unification.Types Methods pure :: a -> UTerm t a # (<>) :: UTerm t (a -> b) -> UTerm t a -> UTerm t b # liftA2 :: (a -> b -> c) -> UTerm t a -> UTerm t b -> UTerm t c # (>) :: UTerm t a -> UTerm t b -> UTerm t b # (<*) :: UTerm t a -> UTerm t b -> UTerm t a #
Functor t => Functor (UTerm t)
Instance details Defined in Control.Unification.Types Methods fmap :: (a -> b) -> UTerm t a -> UTerm t b # (<$) :: a -> UTerm t b -> UTerm t a #
Functor t => Monad (UTerm t)
Instance details Defined in Control.Unification.Types Methods (>>=) :: UTerm t a -> (a -> UTerm t b) -> UTerm t b # (>>) :: UTerm t a -> UTerm t b -> UTerm t b # return :: a -> UTerm t a #
(Show v, Show (t (UTerm t v))) => Show (UTerm t v)
Instance details Defined in Control.Unification.Types Methods showsPrec :: Int -> UTerm t v -> ShowS # show :: UTerm t v -> String # showList :: [UTerm t v] -> ShowS #

data UTerm (t :: Type -> Type) v where #

The type of terms generated by structures t over variables v. The structure type should implement Unifiable and the variable type should implement Variable.

The Show instance doesn't show the constructors, in order to improve legibility for large terms.

All the category theoretic instances (Functor, Foldable, Traversable,...) are provided because they are often useful; however, beware that since the implementations must be pure, they cannot read variables bound in the current context and therefore can create incoherent results. Therefore, you should apply the current bindings before using any of the functions provided by those classes.

Bundled Patterns

pattern UTVar :: Identifier -> UType
pattern UTUnit :: UType
pattern UTBool :: UType
pattern UTInt :: UType
pattern UTFun :: UType -> UType -> UType

Instances

Instances details

Foldable t => Foldable (UTerm t)
Instance details Defined in Control.Unification.Types Methods fold :: Monoid m => UTerm t m -> m # foldMap :: Monoid m => (a -> m) -> UTerm t a -> m # foldMap' :: Monoid m => (a -> m) -> UTerm t a -> m # foldr :: (a -> b -> b) -> b -> UTerm t a -> b # foldr' :: (a -> b -> b) -> b -> UTerm t a -> b # foldl :: (b -> a -> b) -> b -> UTerm t a -> b # foldl' :: (b -> a -> b) -> b -> UTerm t a -> b # foldr1 :: (a -> a -> a) -> UTerm t a -> a # foldl1 :: (a -> a -> a) -> UTerm t a -> a # toList :: UTerm t a -> [a] # null :: UTerm t a -> Bool # length :: UTerm t a -> Int # elem :: Eq a => a -> UTerm t a -> Bool # maximum :: Ord a => UTerm t a -> a # minimum :: Ord a => UTerm t a -> a # sum :: Num a => UTerm t a -> a # product :: Num a => UTerm t a -> a #
Traversable t => Traversable (UTerm t)
Instance details Defined in Control.Unification.Types Methods traverse :: Applicative f => (a -> f b) -> UTerm t a -> f (UTerm t b) # sequenceA :: Applicative f => UTerm t (f a) -> f (UTerm t a) # mapM :: Monad m => (a -> m b) -> UTerm t a -> m (UTerm t b) # sequence :: Monad m => UTerm t (m a) -> m (UTerm t a) #
Functor t => Applicative (UTerm t)
Instance details Defined in Control.Unification.Types Methods pure :: a -> UTerm t a # (<>) :: UTerm t (a -> b) -> UTerm t a -> UTerm t b # liftA2 :: (a -> b -> c) -> UTerm t a -> UTerm t b -> UTerm t c # (>) :: UTerm t a -> UTerm t b -> UTerm t b # (<*) :: UTerm t a -> UTerm t b -> UTerm t a #
Functor t => Functor (UTerm t)
Instance details Defined in Control.Unification.Types Methods fmap :: (a -> b) -> UTerm t a -> UTerm t b # (<$) :: a -> UTerm t b -> UTerm t a #
Functor t => Monad (UTerm t)
Instance details Defined in Control.Unification.Types Methods (>>=) :: UTerm t a -> (a -> UTerm t b) -> UTerm t b # (>>) :: UTerm t a -> UTerm t b -> UTerm t b # return :: a -> UTerm t a #
(Show v, Show (t (UTerm t v))) => Show (UTerm t v)
Instance details Defined in Control.Unification.Types Methods showsPrec :: Int -> UTerm t v -> ShowS # show :: UTerm t v -> String # showList :: [UTerm t v] -> ShowS #

data UTerm (t :: Type -> Type) v where #

The type of terms generated by structures t over variables v. The structure type should implement Unifiable and the variable type should implement Variable.

The Show instance doesn't show the constructors, in order to improve legibility for large terms.

All the category theoretic instances (Functor, Foldable, Traversable,...) are provided because they are often useful; however, beware that since the implementations must be pure, they cannot read variables bound in the current context and therefore can create incoherent results. Therefore, you should apply the current bindings before using any of the functions provided by those classes.

Bundled Patterns

pattern UTVar :: Identifier -> UType
pattern UTUnit :: UType
pattern UTBool :: UType
pattern UTInt :: UType
pattern UTFun :: UType -> UType -> UType

Instances

Instances details

Foldable t => Foldable (UTerm t)
Instance details Defined in Control.Unification.Types Methods fold :: Monoid m => UTerm t m -> m # foldMap :: Monoid m => (a -> m) -> UTerm t a -> m # foldMap' :: Monoid m => (a -> m) -> UTerm t a -> m # foldr :: (a -> b -> b) -> b -> UTerm t a -> b # foldr' :: (a -> b -> b) -> b -> UTerm t a -> b # foldl :: (b -> a -> b) -> b -> UTerm t a -> b # foldl' :: (b -> a -> b) -> b -> UTerm t a -> b # foldr1 :: (a -> a -> a) -> UTerm t a -> a # foldl1 :: (a -> a -> a) -> UTerm t a -> a # toList :: UTerm t a -> [a] # null :: UTerm t a -> Bool # length :: UTerm t a -> Int # elem :: Eq a => a -> UTerm t a -> Bool # maximum :: Ord a => UTerm t a -> a # minimum :: Ord a => UTerm t a -> a # sum :: Num a => UTerm t a -> a # product :: Num a => UTerm t a -> a #
Traversable t => Traversable (UTerm t)
Instance details Defined in Control.Unification.Types Methods traverse :: Applicative f => (a -> f b) -> UTerm t a -> f (UTerm t b) # sequenceA :: Applicative f => UTerm t (f a) -> f (UTerm t a) # mapM :: Monad m => (a -> m b) -> UTerm t a -> m (UTerm t b) # sequence :: Monad m => UTerm t (m a) -> m (UTerm t a) #
Functor t => Applicative (UTerm t)
Instance details Defined in Control.Unification.Types Methods pure :: a -> UTerm t a # (<>) :: UTerm t (a -> b) -> UTerm t a -> UTerm t b # liftA2 :: (a -> b -> c) -> UTerm t a -> UTerm t b -> UTerm t c # (>) :: UTerm t a -> UTerm t b -> UTerm t b # (<*) :: UTerm t a -> UTerm t b -> UTerm t a #
Functor t => Functor (UTerm t)
Instance details Defined in Control.Unification.Types Methods fmap :: (a -> b) -> UTerm t a -> UTerm t b # (<$) :: a -> UTerm t b -> UTerm t a #
Functor t => Monad (UTerm t)
Instance details Defined in Control.Unification.Types Methods (>>=) :: UTerm t a -> (a -> UTerm t b) -> UTerm t b # (>>) :: UTerm t a -> UTerm t b -> UTerm t b # return :: a -> UTerm t a #
(Show v, Show (t (UTerm t v))) => Show (UTerm t v)
Instance details Defined in Control.Unification.Types Methods showsPrec :: Int -> UTerm t v -> ShowS # show :: UTerm t v -> String # showList :: [UTerm t v] -> ShowS #

Polytype

data Poly t Source #

Constructors

Forall [Identifier] t

Instances

Instances details

Functor Poly Source #
Instance details Defined in TypeChecker.HindleyMilner Methods fmap :: (a -> b) -> Poly a -> Poly b # (<$) :: a -> Poly b -> Poly a #
Show t => Show (Poly t) Source #
Instance details Defined in TypeChecker.HindleyMilner Methods showsPrec :: Int -> Poly t -> ShowS # show :: Poly t -> String # showList :: [Poly t] -> ShowS #
Eq t => Eq (Poly t) Source #
Instance details Defined in TypeChecker.HindleyMilner Methods (==) :: Poly t -> Poly t -> Bool # (/=) :: Poly t -> Poly t -> Bool #

type Polytype = Poly Type Source #

Converters

toUType :: Type -> UType Source #

toPolytype :: UPolytype -> Polytype Source #

Infer

type Infer = ReaderT Ctx (ExceptT TypeError (IntBindingT TypeF Identity)) Source #

lookup :: Identifier -> Infer UType Source #

withBinding :: MonadReader Ctx m => Identifier -> UPolytype -> m a -> m a Source #

FreeVars

fresh :: Infer UType Source #

Errors

data TypeError where Source #

Constructors

Unreachable :: TypeError
UnboundVar :: Identifier -> TypeError
Infinite :: IntVar -> UType -> TypeError
ImpossibleBinOpApplication :: UType -> UType -> TypeError
ImpossibleUnOpApplication :: UType -> TypeError
Mismatch :: TypeF UType -> TypeF UType -> TypeError

Instances

Instances details

Show TypeError Source #
Instance details Defined in TypeChecker.HindleyMilner Methods showsPrec :: Int -> TypeError -> ShowS # show :: TypeError -> String # showList :: [TypeError] -> ShowS #
Fallible TypeF IntVar TypeError Source #
Instance details Defined in TypeChecker.HindleyMilner Methods occursFailure :: IntVar -> UTerm TypeF IntVar -> TypeError # mismatchFailure :: TypeF (UTerm TypeF IntVar) -> TypeF (UTerm TypeF IntVar) -> TypeError #

(=:=) :: UType -> UType -> Infer UType Source #

applyBindings :: UType -> Infer UType Source #

mkVarName :: String -> IntVar -> Identifier Source #

generalize :: UType -> Infer UPolytype Source #

Orphan instances

Ord IntVar Source #
Instance details Methods compare :: IntVar -> IntVar -> Ordering # (<) :: IntVar -> IntVar -> Bool # (<=) :: IntVar -> IntVar -> Bool # (>) :: IntVar -> IntVar -> Bool # (>=) :: IntVar -> IntVar -> Bool # max :: IntVar -> IntVar -> IntVar # min :: IntVar -> IntVar -> IntVar #