Skip to content

Instantly share code, notes, and snippets.

@soupi
Last active July 17, 2024 14:04
Show Gist options
  • Save soupi/ee78682851f396dc9b1953e9a72b9085 to your computer and use it in GitHub Desktop.
Save soupi/ee78682851f396dc9b1953e9a72b9085 to your computer and use it in GitHub Desktop.
Kind inference using unification-base constraint solving.
#!/usr/bin/env cabal
{- cabal:
build-depends: base, mtl, containers, uniplate
ghc-options: -Wall
-}
-- | An example of a kind inference for data types using
-- unification-based constraint solving.
--
-- See the blog post:
-- <https://gilmi.me/blog/post/2023/09/30/kind-inference>
{-# Language GHC2021 #-}
{-# Language LambdaCase #-}
import Data.Data (Data)
import GHC.Generics (Generic)
import Data.Tuple (swap)
import Data.Maybe (listToMaybe)
import Data.Foldable (for_)
import Data.Traversable (for)
import Control.Monad (foldM)
import Control.Monad.State qualified as Mtl
import Control.Monad.Except qualified as Mtl
import Data.Generics.Uniplate.Data qualified as Uniplate (universe, transformBi)
import Data.Map qualified as Map
-- * Tests
main :: IO ()
main = do
putStrLn "========================"
putStrLn "-- Expected successes --"
for_ expectedSuccesses inferAndPrint
putStrLn "========================"
putStrLn "-- Expected failures --"
for_ expectedFailures inferAndPrint
putStrLn "========================"
expectedSuccesses :: [[Datatype ()]]
expectedSuccesses =
[ -- We start with a simple data type of kind 'Type'.
[ Datatype () (MkTypeName "Person")
[]
[ Variant "Person"
[ TypeName () $ MkTypeName "String"
, TypeName () $ MkTypeName "Int"
]
]
]
, -- A data type with a type variable.
[ Datatype () (MkTypeName "Option")
[MkTypeVar "a"]
[ Variant "Some" [TypeVar () $ MkTypeVar "a"]
, Variant "None" []
]
]
, -- A data type with two type variables.
[ Datatype () (MkTypeName "Result")
[MkTypeVar "a", MkTypeVar "b"]
[ Variant "Ok" [TypeVar () $ MkTypeVar "a"]
, Variant "Err" [TypeVar () $ MkTypeVar "b"]
]
]
, -- A more complex, recursive data type with higher-kinded type variables.
[ Datatype () (MkTypeName "Cofree")
[MkTypeVar "f", MkTypeVar "a"]
[ Variant "Cofree"
[ TypeVar () $ MkTypeVar "a"
, TypeApp ()
(TypeVar () $ MkTypeVar "f")
( TypeApp ()
( TypeApp ()
(TypeName () $ MkTypeName "Cofree")
(TypeVar () $ MkTypeVar "f")
)
(TypeVar () $ MkTypeVar "a")
)
]
]
]
, -- A data type where the type variable does not appear in the variants.
[ Datatype () (MkTypeName "Phantom")
[MkTypeVar "a"]
[ Variant "A" [TypeName () $ MkTypeName "Int"]
, Variant "B" [TypeApp () (TypeName () $ MkTypeName "List") (TypeName () $ MkTypeName "Bool")]
]
]
, -- Mutually recursive data types.
[ Datatype () (MkTypeName "Select")
[MkTypeVar "ann", MkTypeVar "lit"]
[ Variant "Select"
[ TypeVar () $ MkTypeVar "ann"
, TypeApp ()
( TypeApp ()
(TypeName () $ MkTypeName "Expr")
(TypeVar () $ MkTypeVar "ann")
)
(TypeVar () $ MkTypeVar "lit")
]
]
, Datatype () (MkTypeName "Expr")
[MkTypeVar "ann", MkTypeVar "lit"]
[ Variant "Subselect"
[ TypeApp ()
( TypeApp ()
(TypeName () $ MkTypeName "Select")
(TypeVar () $ MkTypeVar "ann")
)
(TypeVar () $ MkTypeVar "lit")
]
, Variant "Lit" [TypeApp () (TypeVar () $ MkTypeVar "lit") (TypeVar () $ MkTypeVar "ann")]
]
]
, -- Empty data types with proxy types used more than once.
[ Datatype () (MkTypeName "Person") [] []
, Datatype () (MkTypeName "Company") [MkTypeVar "taxId"] [Variant "TaxId" [TypeVar () $ MkTypeVar "taxId"]]
, Datatype () (MkTypeName "ObjectId")
[]
[ Variant "Person"
[ TypeApp ()
(TypeName () $ MkTypeName "Id")
(TypeName () $ MkTypeName "Person")
]
, Variant "Company"
[ TypeApp ()
(TypeName () $ MkTypeName "Id")
(TypeName () $ MkTypeName "Company")
]
]
]
]
expectedFailures :: [[Datatype ()]]
expectedFailures =
[ -- Type variable 'a' is used as a 'Type' and a higher-kinded type.
[ Datatype () (MkTypeName "Fail1")
[MkTypeVar "a"]
[ Variant "A" [TypeVar () $ MkTypeVar "a"]
, Variant "B" [TypeApp () (TypeVar () $ MkTypeVar "a") (TypeName () $ MkTypeName "Bool")]
]
]
, -- Data type 'Fail2' is higher-kinded but does not take type parameters
-- in the variant 'A'.
[ Datatype () (MkTypeName "Fail2")
[MkTypeVar "a"]
[ Variant "A" [TypeName () $ MkTypeName "Fail2"]
]
]
, -- contains a type variable with two different kinds.
[ Datatype () (MkTypeName "Fail3")
[MkTypeVar "f", MkTypeVar "a"]
[ Variant "A"
[ TypeApp ()
(TypeVar () $ MkTypeVar "f")
( TypeApp ()
(TypeVar () $ MkTypeVar "a")
(TypeVar () $ MkTypeVar "a")
)
]
]
]
, -- Data type usage is not fully saturated.
[ Datatype () (MkTypeName "Tree")
[MkTypeVar "a"]
[ Variant "Node"
[ TypeVar () $ MkTypeVar "a"
, TypeName () $ MkTypeName "Tree"
, TypeName () $ MkTypeName "Tree"
]
]
]
]
-- | Infer a group of data types and print the result.
inferAndPrint :: [Datatype ()] -> IO ()
inferAndPrint datatypes = do
putStrLn "========================"
putStrLn ""
for_ datatypes $ putStrLn . ppDatatype
putStrLn "------------------------"
putStrLn ""
let result = infer builtinKindEnv datatypes
case result of
Left err -> do
putStrLn (ppError err)
Right datatypes' ->
for_ datatypes' $ putStrLn . ppDatatype'
-- | A environment of kinds for built-in types.
builtinKindEnv :: Map.Map TypeName Kind
builtinKindEnv = Map.fromList
[ (MkTypeName "Int", Type)
, (MkTypeName "Bool", Type)
, (MkTypeName "String", Type)
, (MkTypeName "List", KindFun Type Type)
, ( MkTypeName "Id" -- Something like: `Id object = Id Int`.
, KindScheme [MkKindVar "k1"] $ KindFun (KindVar (MkKindVar "k1")) Type
)
]
-- * Data types
-- | The representation of a data type definition.
data Datatype a
= Datatype
{ -- | A place to put kind annotation in.
dtAnn :: a
, -- | The name of the data type.
dtName :: TypeName
, -- | Type parameters.
dtParameters :: [TypeVar]
, -- | Alternative variants.
dtVariants :: [Variant a]
}
deriving (Show, Eq, Data, Generic, Functor, Foldable, Traversable)
-- | A Variant of a data type definition.
data Variant a
= Variant
{ -- | A type constructor.
vTypeConstructor :: String
, -- | A list of types.
vTypes :: [Type a]
}
deriving (Show, Eq, Data, Generic, Functor, Foldable, Traversable)
-- | A name of known types.
newtype TypeName = MkTypeName { getTypeName :: String }
deriving (Show, Eq, Ord, Data, Generic)
-- | A type variable.
newtype TypeVar = MkTypeVar { getTypeVar :: String }
deriving (Show, Eq, Ord, Data, Generic)
-- | A representation of a type with a place for kind annotation.
data Type a
= -- | A type variable.
TypeVar a TypeVar
| -- | A named type.
TypeName a TypeName
| -- | An application of two types, of the form `t1 t2`.
TypeApp a (Type a) (Type a)
deriving (Show, Eq, Data, Generic, Functor, Foldable, Traversable)
-- | A representation of a kind.
data Kind
= -- | For types like `Int`.
Type
| -- | For types like `Option`.
KindFun Kind Kind
| -- | For polymorphic kinds.
KindVar KindVar
| -- | For closing over polymorphic kinds.
KindScheme [KindVar] Kind
deriving (Show, Eq, Data, Generic)
-- | A kind variable.
newtype KindVar = MkKindVar { getKindVar :: String }
deriving (Show, Eq, Ord, Data, Generic)
-- * Algorithm
-- ** Inference
-- | Infer the kind of a group of data types that should be solved together
-- (because they are mutually recursive).
infer :: Map.Map TypeName Kind -> [Datatype ()] -> Either Error [Datatype Kind]
infer kindEnv datatypes =
-- initialize our `InferenceM` which is State + Except
flip Mtl.evalState (initialState kindEnv) $ Mtl.runExceptT $ do
-- Invent a kind variable for each data type
for_ datatypes $ \(Datatype _ name _ _) -> do
kindvar <- freshKindVar
declareNamedType name kindvar
-- Elaborate all of the data types
datatypes' <- traverse elaborate datatypes
-- Solve the constraints
solveConstraints
for datatypes' $ \(Datatype kindvar name vars variants) -> do
-- Substitute the kind variable for a kind
-- for the data type
kind <- lookupKindVarInSubstitution kindvar
-- ... and for all types
variants' <- for variants $ traverse lookupKindVarInSubstitution
-- generalize the data type's kind, and return.
pure (Datatype (generalize kind) name vars variants')
-- ** Elaboration
-- | Invent kind variables for types we don't know and add constraints
-- on them according to their usage.
elaborate :: Datatype () -> InferenceM (Datatype KindVar)
elaborate (Datatype _ datatypeName vars variants) = do
-- We go over each of the data type parameters and
-- generate a fresh kind variable for them.
varKinds <- for vars $ \var -> do
kindvar <- freshKindVar
declareTypeVar var kindvar
pure kindvar
-- We go over the variants, elaborate each field,
-- and return the elaborated variants.
variants' <- for variants $ \(Variant name fields) -> do
Variant name <$>
for fields
( \field -> do
field' <- elaborateType field
-- a constraint on fields: their kind must be `Type`.
newEqualityConstraint (KindVar $ getAnn field') Type
pure field'
)
-- We grab the kind variable of the data type
-- so we can add a constraint on it.
datatypeKindvar <- lookupNameKindVar datatypeName
-- A type of the form `T a b c ... =` has the kind:
-- `aKind -> bKind -> cKind -> ... -> Type`.
-- We add that as a constraint.
let kind = foldr KindFun Type $ map KindVar varKinds
newEqualityConstraint (KindVar datatypeKindvar) kind
-- We return the elaborated data type after annotating
-- all types with kind variables and generating constraints.
pure (Datatype datatypeKindvar datatypeName vars variants')
-- | Elaborate a type with a kind variable and add constraints
-- according to usage.
elaborateType :: Type () -> InferenceM (Type KindVar)
elaborateType = \case
-- for type variables and type names,
-- we lookup the kind variables we generated when we ran into
-- the declaration of them.
TypeVar () var ->
fmap (\kindvar -> TypeVar kindvar var) (lookupVarKindVar var)
TypeName () name ->
fmap (\kindvar -> TypeName kindvar name) (lookupNameKindVar name)
-- for type application
TypeApp () t1 t2 -> do
-- we elaborate both types
t1Kindvar <- elaborateType t1
t2Kindvar <- elaborateType t2
-- then we generate a kind variable for the type application
typeAppKindvar <- freshKindVar
-- then we constrain the type application kind variable
-- it should unify with `t2Kind -> typeAppKind`.
newEqualityConstraint
(KindVar $ getAnn t1Kindvar)
(KindFun (KindVar $ getAnn t2Kindvar) (KindVar typeAppKindvar))
pure (TypeApp typeAppKindvar t1Kindvar t2Kindvar)
-- ** Constraint solving and generating a substitution.
-- | Solve constraints according to logic.
-- this process is iterative. We continue fetching
-- the next constraint and try to solve it.
--
-- Each step can either reduce or increase the number of constraints,
-- and we are done when there are no more constraints to solve,
-- or if we ran into a constraint that cannot be solved.
solveConstraints :: InferenceM ()
solveConstraints = do
-- Pop the next constraint we should solve.
constraint <- do
c <- listToMaybe . constraints <$> Mtl.get
Mtl.modify $ \s -> s { constraints = drop 1 $ constraints s }
pure c
case constraint of
-- If we have two 'Type's, the unify. We can skip to the next constraint.
Just (Equality Type Type) -> solveConstraints
-- We have an equality between two kind functions.
-- We add two new equality constraints matching the two firsts
-- with the two seconds.
Just (Equality (KindFun k1 k2) (KindFun k3 k4)) -> do
Mtl.modify $ \s ->
s { constraints = Equality k1 k3 : Equality k2 k4 : constraints s }
solveConstraints
-- When we run into a kind scheme, we instantiate it
-- (we look at the kind and replace all closed kind variables
-- with fresh kind variables), and add an equality constraint
-- between the other kind and the instantiated kind.
Just (Equality (KindScheme vars kind) k) -> do
kind' <- instantiate kind vars
Mtl.modify $ \s ->
s { constraints = Equality k kind' : constraints s }
solveConstraints
-- Same as the previous scenario.
Just (Equality k (KindScheme vars kind)) -> do
kind' <- instantiate kind vars
Mtl.modify $ \s ->
s { constraints = Equality kind' k : constraints s }
solveConstraints
-- If we run into a kind variable on one of the sides,
-- we replace all instances of it with the other kind and continue.
Just (Equality (KindVar var) k) -> do
replaceInState var k
solveConstraints
-- The same as the previous scenario, but the kind var is on the other side.
Just (Equality k (KindVar var)) -> do
replaceInState var k
solveConstraints
-- If we have an equality constraint between a 'Type' and
-- a 'KindFun', we cannot unify the two, and unification fails.
Just (Equality k1@Type k2@KindFun{}) -> Mtl.throwError (UnificationFailed k1 k2)
Just (Equality k1@KindFun{} k2@Type) -> Mtl.throwError (UnificationFailed k1 k2)
-- If there are no more constraints, we are done. Good job!
Nothing -> pure ()
-- | Instantiate a kind.
-- We look at the kind and replace all closed kind variables
-- with fresh kind variables.
instantiate :: Kind -> [KindVar] -> InferenceM Kind
instantiate = foldM replaceKindVarWithFreshKindVar
-- | Replace a kind variable with a fresh variable in the kind.
replaceKindVarWithFreshKindVar :: Kind -> KindVar -> InferenceM Kind
replaceKindVarWithFreshKindVar kind var = do
kindvar <- freshKindVar
-- Uniplate.transformBi lets us perform reflection and
-- apply a function to all instances of a certain type
-- in a value. Think of it like `fmap`, but for any type.
--
-- It is a bit slow though, so it's worth replacing it with
-- hand rolled recursion or a functor, but its convenient.
pure $ flip Uniplate.transformBi kind $ \case
kv | kv == var -> kindvar
x -> x
-- | Replace every instance of 'KindVar var' in our state with 'kind'.
-- And add it to the substitution.
replaceInState :: KindVar -> Kind -> InferenceM ()
replaceInState var kind = do
occursCheck var kind
s <- Mtl.get
let
-- Uniplate.transformBi lets us perform reflection and
-- apply a function to all instances of a certain type
-- in a value. Think of it like `fmap`, but for any type.
--
-- Note that we are changing all instances of `Kind` of the form
-- `KindVar v | v == var` in all of `State`! This includes both the
-- `substitution` and the remaining `constraints`,
--
-- It is a bit slow though, so it's worth replacing it with
-- hand rolled recursion or a functor, but its convenient.
s' =
flip Uniplate.transformBi s $ \case
KindVar v | v == var -> kind
x -> x
Mtl.put $ s' { substitution = Map.insert var kind (substitution s') }
-- | We check that the kind variable does not appear in the kind
-- and throw an error if it does.
occursCheck :: KindVar -> Kind -> InferenceM ()
occursCheck var kind =
if KindVar var == kind || null [ () | KindVar v <- Uniplate.universe kind, var == v ]
then pure ()
else do
-- We try to find the type of the kind variable by doing reverse lookup,
-- but this might not succeed before the kind variable might be generated
-- during constraint solving.
-- We might be able to find the type if we look at the substitution as well,
-- but for now lets leave it at this "best effort" attempt.
reverseEnv <- map swap . Map.toList . env <$> Mtl.get
let typ = either (TypeName ()) (TypeVar ()) <$> lookup var reverseEnv
Mtl.throwError (OccursCheckFailed typ var kind)
-- ** Generalization
-- | Close over kind variables we did not solve.
generalize :: Kind -> Kind
generalize kind = KindScheme [var | KindVar var <- Uniplate.universe kind] kind
-----------------------------------
-- * Utilities for working State
-- ** Types
-- | We combine the capabilities of Except and State
-- For our kind inference code.
type InferenceM a = Mtl.ExceptT Error (Mtl.State State) a
-- | The errors that can be thrown in the process.
data Error
= UnboundVar TypeVar
| UnboundName TypeName
| UnificationFailed Kind Kind
| OccursCheckFailed (Maybe (Type ())) KindVar Kind
deriving (Show)
-- | The state we keep during an inference cycle
data State = State
{ -- | Mapping from named types or type variables to kind variables.
-- When we declare a new data type or a type variable, we'll add it here.
-- When run into a type variable or a type name during elaboration,
-- we search its matching kind here.
env :: Map.Map (Either TypeName TypeVar) KindVar
, -- | Mapping from existing named types to their kinds.
-- Kinds for types that are supplied before the inference process can be found here.
kindEnv :: Map.Map TypeName Kind
, -- | Used for generating fresh kind variables.
counter :: Int
, -- | When we learn information about kinds during elaboration, we'll add it here.
constraints :: [Constraint]
, -- | The constraint solving process will generate this mapping from
-- the kind variables we collected to the kind they should represent.
-- If we don't find the kind variable in the substitution, that means
-- it is a free variable we should close over.
substitution :: Map.Map KindVar Kind
}
deriving (Show, Eq, Data, Generic)
-- | A constraint on kinds.
data Constraint
= Equality Kind Kind
-- ^ The two kinds should unify.
-- If one of the kinds is a kind scheme, we will instantiate it, and
-- add an equality constraint of the other kind with the instantiated kind.
deriving (Show, Eq, Data, Generic)
-- ** Utilities
-- | The state at the start of the process.
initialState :: Map.Map TypeName Kind -> State
initialState kindEnv =
State mempty kindEnv 0 mempty mempty
-- | Generate a fresh kind variables.
freshKindVar :: InferenceM KindVar
freshKindVar = do
s <- Mtl.get
let kindvar = MkKindVar ("k" <> show (counter s))
Mtl.put s { counter = 1 + counter s }
pure kindvar
-- | Insert declared type names into the environment.
declareNamedType :: TypeName -> KindVar -> InferenceM ()
declareNamedType name kindvar =
Mtl.modify $ \s ->
s { env = Map.insert (Left name) kindvar (env s) }
-- | Insert declared type variables into the environment.
declareTypeVar :: TypeVar -> KindVar -> InferenceM ()
declareTypeVar var kindvar =
Mtl.modify $ \s ->
s { env = Map.insert (Right var) kindvar (env s) }
-- | Add a new equality constraint to the state.
newEqualityConstraint :: Kind -> Kind -> InferenceM ()
newEqualityConstraint k1 k2 =
Mtl.modify $ \s ->
s { constraints = Equality k1 k2 : constraints s }
-- | Find the kind variable of a named type in the environment.
lookupNameKindVar :: TypeName -> InferenceM KindVar
lookupNameKindVar name = do
state <- Mtl.get
-- We first look the named type in the supplied kind env.
case Map.lookup name (kindEnv state) of
-- If we find it, we generate a new kind variable for it
-- and constraint it to be this type, so that each use has it own
-- type variable (later used for instantiation).
Just kind -> do
kindvar <- freshKindVar
newEqualityConstraint (KindVar kindvar) kind
pure kindvar
-- If it's not a supplied type, it means we are actively inferring it,
-- and we need to use the same kind variable for all uses.
-- We'll look it up in our environment of declared types.
Nothing ->
maybe
-- If we still can't find it, we error.
(Mtl.throwError $ UnboundName name)
pure
. Map.lookup (Left name)
$ env state
-- | Find the kind variable of a type variable in the environment.
lookupVarKindVar :: TypeVar -> InferenceM KindVar
lookupVarKindVar var =
maybe
(Mtl.throwError $ UnboundVar var)
pure
. Map.lookup (Right var)
. env =<< Mtl.get
-- | Look up what the kind of a kind variable is in the substitution
-- produced by constraint solving.
-- If there was no constraint on the kind variable, it won't appear
-- in the substitution, which means it can stay a kind variable which
-- we will close over later.
lookupKindVarInSubstitution :: KindVar -> InferenceM Kind
lookupKindVarInSubstitution kindvar =
maybe (KindVar kindvar) id . Map.lookup kindvar . substitution <$> Mtl.get
-- | Get the annotation of a type.
getAnn :: Type a -> a
getAnn = \case
TypeVar a _ -> a
TypeName a _ -> a
TypeApp a _ _ -> a
-- * Prettyprinting
ppDatatype :: Datatype a -> String
ppDatatype (Datatype _ name vars variants) =
let
parameters
| null vars = ""
| otherwise = " " <> unwords (map getTypeVar vars)
in
getTypeName name <> parameters <> " =\n" <> unlines (map ppVariant variants)
ppDatatype' :: Datatype Kind -> String
ppDatatype' (Datatype kind name vars variants) =
getTypeName name <> " : " <> ppKind False kind <> "\n" <>
getTypeName name <> " " <> unwords (map getTypeVar vars) <> " =\n" <> unlines (map ppVariant variants)
ppVariant :: Variant a -> String
ppVariant (Variant con types) =
" | " <> con <> " " <> unwords (map (ppType True) types)
ppType :: Bool -> Type a -> String
ppType parens = \case
TypeVar _ var -> getTypeVar var
TypeName _ name -> getTypeName name
TypeApp _ t1 t2 ->
let result = ppType False t1 <> " " <> ppType True t2
in if parens then "(" <> result <> ")" else result
ppKind :: Bool -> Kind -> String
ppKind parens = \case
Type -> "Type"
KindVar v -> getKindVar v
KindFun k1 k2 ->
let str = ppKind True k1 <> " -> " <> ppKind False k2
in if parens then "(" <> str <> ")" else str
KindScheme vars kind
| null vars -> ppKind parens kind
| otherwise ->
let str = "forall " <> unwords (map getKindVar vars) <> ". " <> ppKind False kind
in if parens then "(" <> str <> ")" else str
ppError :: Error -> String
ppError = \case
UnboundVar var ->
"Unbound type variable: '" <> getTypeVar var <> "'.\n"
UnboundName name ->
"Unbound type variable: '" <> getTypeName name <> "'.\n"
UnificationFailed k1 k2 ->
unlines
[ "Unification failed between the following kinds:"
, " * " <> ppKind False k1
, " * " <> ppKind False k2
]
OccursCheckFailed mtype kindvar kind ->
unlines
[ "Occurs check failed" <>
( case mtype of
Nothing -> ""
Just typ -> " for type '" <> ppType False typ <> "'"
) <> ":"
, " * " <> getKindVar kindvar
, " * " <> ppKind False kind
]

Output:

========================
-- Expected successes --
========================

Person =
  | Person String Int

------------------------

Person : Type
Person  =
  | Person String Int

========================

Option a =
  | Some a
  | None 

------------------------

Option : Type -> Type
Option a =
  | Some a
  | None 

========================

Result a b =
  | Ok a
  | Err b

------------------------

Result : Type -> Type -> Type
Result a b =
  | Ok a
  | Err b

========================

Cofree f a =
  | Cofree a (f (Cofree f a))

------------------------

Cofree : (Type -> Type) -> Type -> Type
Cofree f a =
  | Cofree a (f (Cofree f a))

========================

Phantom a =
  | A Int
  | B (List Bool)

------------------------

Phantom : forall k1. k1 -> Type
Phantom a =
  | A Int
  | B (List Bool)

========================

Select ann lit =
  | Select ann (Expr ann lit)

Expr ann lit =
  | Subselect (Select ann lit)
  | Lit (lit ann)

------------------------

Select : Type -> (Type -> Type) -> Type
Select ann lit =
  | Select ann (Expr ann lit)

Expr : Type -> (Type -> Type) -> Type
Expr ann lit =
  | Subselect (Select ann lit)
  | Lit (lit ann)

========================

Person =

Company taxId =
  | TaxId taxId

ObjectId =
  | Person (Id Person)
  | Company (Id Company)

------------------------

Person : Type
Person  =

Company : Type -> Type
Company taxId =
  | TaxId taxId

ObjectId : Type
ObjectId  =
  | Person (Id Person)
  | Company (Id Company)

========================
-- Expected failures  --
========================

Fail1 a =
  | A a
  | B (a Bool)

------------------------

Unification failed between the following kinds:
  * Type -> Type
  * Type

========================

Fail2 a =
  | A Fail2

------------------------

Unification failed between the following kinds:
  * k1 -> Type
  * Type

========================

Fail3 f a =
  | A (f (a a))

------------------------

Occurs check failed for type 'a':
  * k2
  * k2 -> k3

========================

Tree a =
  | Node a Tree Tree

------------------------

Unification failed between the following kinds:
  * k1 -> Type
  * Type

========================
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment