This page how the various expression constructs in monad-embed behave during type inference. The first column shows an example of an expression. The second and third columns show the free variables and type-equalities that are created for the type inference system to solve.

Expression | Free type vars | Type constraints |
---|---|---|

x = \ arg -> body |
m :: * -> * a :: * b :: * |
x :: {m} (a -> {m} b); arg :: (n :: * -> *) => {n} a; body :: {m} b; |

x = fun arg |
m :: * -> * a :: * b :: * |
fun :: {m} (a -> {m} b); arg :: {m} a; x :: {m} b; |

x = \ [arg] -> body |
m :: * -> * n :: * -> * a :: * b :: * |
x :: {m} [{n} a] -> {m} b; arg :: {n} a; body :: {m} b; |

x = fun [arg] |
m :: * -> * n :: * -> * a :: * b :: * |
fun :: {m} [{n} a] -> {m} b; arg :: {n} a; x :: {m} b; |

1234567 |
m :: * -> * |
1234567 :: {m} Number; |

x = case subj of { Con field -> value; }where data T = { Con U; }; |
m :: * -> * b :: * |
subj :: {m} T; field :: (n :: * -> *) => {n} U; value :: {m} b; x :: {m} b; |

x = case subj of { Con [field] -> value; }where data T = { Con [{M} U]; }; |
n :: * -> * b :: * |
subj :: {n} T; field :: {M} U; value :: {n} b; x :: {n} b; |

x = do { var = value; } then rest |
m :: * -> * a :: * b :: * |
value :: {m} a; var :: (n :: * -> *) => {n} a; rest :: {m} b; x :: {m} b; |

x = do { var =[] value; } then rest |
m :: * -> * n :: * -> * a :: * b :: * |
value :: {n} a; var :: {n} a; rest :: {m} b; x :: {m} b |

x = do { thing; } then rest |
m :: * -> * a :: * b :: * |
thing :: {m} a; x :: {m} b; |