1a38107941725211e7c3f051f7a8f5e12199f03acmaederclass Functor < Type -> Type

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder {vars f : Functor; a, b, c : Type

e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens Elkner op map : (a -> b) -> f a -> f b

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder vars x : f a; f : a -> b; g : b -> c

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder . (map \ y : a .! y) x = x

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu Prodescu . (map \ y : a .! g (f y)) x = map g (map f x);

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder }

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksaclass Monad < Type -> Type

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder {vars m : Monad; a, b, c : Type

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder ops __>>=__ : m a * (a ->? m b) ->? m b;

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder __>>=__ : m a * (a -> m b) -> m b;

75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc ret : a -> m a

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder vars x, y : a; p : m a; q : a ->? m b; r : b ->? m c; f : a ->? b

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder . def q x => ret x >>= q = q x

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder . (p >>= \ x : a . ret (f x) >>= r) = p >>= \ x : a . r (f x)

75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc . p >>= ret = p

7b1111ca3b126f71cce47e60ce4b56e6f92422e9Karl Luc . (p >>= q) >>= r = p >>= \ x : a . q x >>= r

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder . (ret x : m a) = ret y => x = y;

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder }

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederclass instance Monad < Functor

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maedervars m : Monad; a, b : Type; f : a -> b; x : m a

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder. map f x = x >>= \ y : a . ret (f y);

e036e115761fe7c09c210c337440a1864d794093Martha Rohteclass MonadT < Monad -> Monad

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder {vars t : MonadT; m : Monad; a : Type

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder op lift : m a -> t m a

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder vars x : a; p : m a; b : Type; q : a -> m b

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder . lift (ret x) = (ret x : t m a)

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder . lift (p >>= q) = lift p >>= \ y : a .! lift (q y) : t m b;

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder }

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maedervar state : Type

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maedertype instance ST state : Monad

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maedervars a, b : Type

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maedertype ST state a := state ->? a * state

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maedervars x : a; p : ST state a; q : a ->? ST state b

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederclasses

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaederFunctor < Type -> Type;

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaederMonad < Type -> Type;

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen KuksaMonadT < (Type -> Type) -> Type -> Type

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederclasses

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaederMonad < Functor;

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederMonadT < Monad -> Monad

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroedertype

1a38107941725211e7c3f051f7a8f5e12199f03acmaederST : Type -> Monad

1a38107941725211e7c3f051f7a8f5e12199f03acmaedertype

7b1111ca3b126f71cce47e60ce4b56e6f92422e9Karl LucST := \ state : Type . \ a : Type . state ->? a * state

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maedervars

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maedera : Type %(var_899)%;

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederb : Type %(var_900)%;

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederc : Type %(var_106)%;

1a38107941725211e7c3f051f7a8f5e12199f03acmaederf : Functor %(var_1)%;

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederm : Monad %(var_651)%;

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederstate : Type %(var_897)%;

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maedert : MonadT %(var_650)%

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederop __>>=__ : forall m : Monad; a : Type; b : Type

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder . m a * (a -> m b) -> m b

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder %(op)%

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederop __>>=__ : forall m : Monad; a : Type; b : Type

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder . m a * (a ->? m b) ->? m b

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder %(op)%

656f17ae9b7610ff2de1b6eedeeadea0c3bcdc8dChristian Maederop lift : forall t : MonadT; m : Monad; a : Type . m a -> t m a

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder %(op)%

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksaop map : forall f : Functor; a : Type; b : Type

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa . (a -> b) -> f a -> f b

7b1111ca3b126f71cce47e60ce4b56e6f92422e9Karl Luc %(op)%

7b1111ca3b126f71cce47e60ce4b56e6f92422e9Karl Lucop ret : forall m : Monad; a : Type . a -> m a %(op)%

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroedervars

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederf : a -> b;

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederg : b -> c;

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederp : ST state a;

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederq : a ->? ST state b;

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederr : b ->? m c;

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederx : a;

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maedery : a

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederforall a : Type; f : Functor; x : f a . (map \ y : a .! y) x = x

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederforall

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maedera : Type; b : Type; c : Type; f : Functor; f : a -> b; g : b -> c;

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederx : f a

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder. (map \ y : a .! g (f y)) x = map g (map f x)

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederforall a : Type; b : Type; m : Monad; q : a ->? m b; x : a

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder. def q x => ret x >>= q = q x

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederforall

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroedera : Type; b : Type; c : Type; m : Monad; f : a ->? b; p : m a;

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederr : b ->? m c

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder. (p >>= \ x : a . ret (f x) >>= r) = p >>= \ x : a . r (f x)

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederforall a : Type; m : Monad; p : m a . p >>= ret = p

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederforall

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maedera : Type; b : Type; c : Type; m : Monad; p : m a; q : a ->? m b;

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederr : b ->? m c

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder. (p >>= q) >>= r = p >>= \ x : a . q x >>= r

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksaforall a : Type; m : Monad; x : a; y : a

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder. (ret x : m a) = ret y => x = y

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederforall a : Type; b : Type; m : Monad; f : a -> b; x : m a

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder. map f x = x >>= \ y : a . ret (f y)

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederforall a : Type; m : Monad; t : MonadT; x : a

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder. lift (ret x) = (ret x : t m a)

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederforall

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maedera : Type; b : Type; m : Monad; t : MonadT; p : m a; q : a -> m b

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder. lift (p >>= q) = lift p >>= \ y : a .! lift (q y) : t m b

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder### Hint 2.7, is type variable 'f'

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder### Hint 2.19, is type variable 'a'

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder### Hint 2.22, is type variable 'b'

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder### Hint 2.25, is type variable 'c'

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder### Hint 4.8, not a kind 'f a'

e9e5281899ddaec4778ad14c64800975377630ecChristian Maeder### Hint 4.16, not a class 'a'

e9e5281899ddaec4778ad14c64800975377630ecChristian Maeder### Hint 4.16, not a class 'b'

e036e115761fe7c09c210c337440a1864d794093Martha Rohte### Warning 4.15, variable also known as type variable 'f'

e9e5281899ddaec4778ad14c64800975377630ecChristian Maeder### Hint 4.27, not a class 'b'

e9e5281899ddaec4778ad14c64800975377630ecChristian Maeder### Hint 4.27, not a class 'c'

e9e5281899ddaec4778ad14c64800975377630ecChristian Maeder### Hint 9.7, is type variable 'm'

e9e5281899ddaec4778ad14c64800975377630ecChristian Maeder### Hint 9.17, is type variable 'a'

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder### Hint 9.17, rebound type variable 'a'

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder### Hint 9.20, is type variable 'b'

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder### Hint 9.20, rebound type variable 'b'

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa### Hint 9.23, is type variable 'c'

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa### Hint 9.23, rebound type variable 'c'

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa### Hint 10.17-10.19,

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederno kind found for 'm a'

2c10bceb28a74fc291959697e023f22a66753655Eugen Kuksa expected: {Cpo}

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa found: {Type}

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa### Hint 10.17-10.19,

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksano kind found for 'm a'

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa expected: {Cppo}

2c10bceb28a74fc291959697e023f22a66753655Eugen Kuksa found: {Type}

2c10bceb28a74fc291959697e023f22a66753655Eugen Kuksa### Hint 11.17-11.19,

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksano kind found for 'm a'

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa expected: {Cpo}

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa found: {Type}

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa### Hint 11.17-11.19,

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksano kind found for 'm a'

2c10bceb28a74fc291959697e023f22a66753655Eugen Kuksa expected: {Cppo}

2c10bceb28a74fc291959697e023f22a66753655Eugen Kuksa found: {Type}

2c10bceb28a74fc291959697e023f22a66753655Eugen Kuksa### Hint 13.8, not a class 'a'

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa### Hint 13.7, rebound variable 'x'

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa### Hint 13.11, not a class 'a'

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa### Hint 13.17, not a kind 'm a'

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa### Hint 13.25, not a kind 'a ->? m b'

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa### Hint 13.39, not a kind 'b ->? m c'

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa### Hint 13.53, not a kind 'a ->? b'

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa### Hint 13.52, rebound variable 'f'

ea570f40967ef8bc16b76c54f9b867a8036cc750Soeren D. Schulze### Warning 13.52, variable also known as type variable 'f'

ea570f40967ef8bc16b76c54f9b867a8036cc750Soeren D. Schulze### Hint 14.14-14.24,

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksarejected '__->?__ < __->__' of '((op ret : forall m : Monad; a : Type . a -> m a) (var x : a),

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (var q : a ->? m b))'

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa### Hint 14.14-14.24,

d2d5606ab65ddf48599bd044416de07a205095f2Soeren D. Schulzeuntypeable term (with type: _v142_v129_m _v130_a * (_v130_a -> _v142_v129_m _v131_b))

d2d5606ab65ddf48599bd044416de07a205095f2Soeren D. Schulze'(ret x, q)'

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa### Hint 15.12, rebound variable 'x'

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa### Hint 15.19-15.33,

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksarejected '__->?__ < __->__' of '((op ret : forall m : Monad; a : Type . a -> m a)

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa ((var f : a ->? b) (var x : a)),

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa (var r : b ->? m c))'

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa### Hint 15.19-15.33,

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksauntypeable term (with type: _v218_v205_m _v206_a * (_v206_a -> _v218_v205_m _v207_b))

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa'(ret (f x), r)'

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa### Hint 15.3-15.33,

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksarejected '__->?__ < __->__' of '((var p : m a),

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa \ x : a

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa . (op __>>=__ :

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa forall m : Monad; a : Type; b : Type . m a * (a ->? m b) ->? m b)

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa ((op ret : forall m : Monad; a : Type . a -> m a)

f03aa0b723e5545fddf7019e287368b9e208ca69Soeren D. Schulze ((var f : a ->? b) (var x : a)),

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa (var r : b ->? m c)))'

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa### Hint 15.3-15.26,

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksauntypeable term (with type: _v192_v179_m _v180_a * (_v180_a -> _v192_v179_m _v181_b))

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa'(p, \ x : a . ret (f x) >>= r)'

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa### Hint 15.12, rebound variable 'x'

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa### Hint 15.19-15.33,

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksarejected '__->?__ < __->__' of '((op ret : forall m : Monad; a : Type . a -> m a)

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa ((var f : a ->? b) (var x : a)),

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa (var r : b ->? m c))'

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa### Hint 15.19-15.33,

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksauntypeable term (with type: _v260_v247_m _v248_a * (_v248_a -> _v260_v247_m _v249_b))

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa'(ret (f x), r)'

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa### Hint 16.13, rebound variable 'x'

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder### Hint 16.5-16.25,

0fe5514fdf12b7559c1a470cf22d89737d55b0a0Eugen Kuksarejected '__->?__ < __->__' of '((var p : m a),

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder \ x : a . (var r : b ->? m c) ((var f : a ->? b) (var x : a)))'

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder### Hint 16.5-16.25,

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederuntypeable term (with type: _v302_v289_m _v290_a * (_v290_a -> _v302_v289_m _v291_b))

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder'(p, \ x : a . r (f x))'

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder### Hint 16.13, rebound variable 'x'

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder### Hint 18.4-18.10,

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksarejected '__->?__ < __->__' of '((var p : m a), (var q : a ->? m b))'

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa### Hint 18.4-18.10,

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederuntypeable term (with type: _v414_v401_m _v402_a * (_v402_a -> _v414_v401_m _v403_b))

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder'(p, q)'

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder### Hint 18.3-18.17,

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederrejected '__->?__ < __->__' of '((op __>>=__ :

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder forall m : Monad; a : Type; b : Type . m a * (a ->? m b) ->? m b)

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder ((var p : m a), (var q : a ->? m b)),

0fe5514fdf12b7559c1a470cf22d89737d55b0a0Eugen Kuksa (var r : b ->? m c))'

0fe5514fdf12b7559c1a470cf22d89737d55b0a0Eugen Kuksa### Hint 18.3-18.17,

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederuntypeable term (with type: _v388_v375_m _v376_a * (_v376_a -> _v388_v375_m _v377_b))

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder'(p >>= q, r)'

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder### Hint 18.4-18.10,

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederrejected '__->?__ < __->__' of '((var p : m a), (var q : a ->? m b))'

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder### Hint 18.4-18.10,

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederuntypeable term (with type: _v440_v427_m _v428_a * (_v428_a -> _v440_v427_m _v429_b))

'(p, q)'

### Hint 18.29, rebound variable 'x'

### Hint 18.36-18.44,

rejected '__->?__ < __->__' of '((var q : a ->? m b) (var x : a), (var r : b ->? m c))'

### Hint 18.36-18.44,

untypeable term (with type: _v492_v479_m _v480_a * (_v480_a -> _v492_v479_m _v481_b))

'(q x, r)'

### Hint 18.21-18.44,

rejected '__->?__ < __->__' of '((var p : m a),

\ x : a

. (op __>>=__ :

forall m : Monad; a : Type; b : Type . m a * (a ->? m b) ->? m b)

((var q : a ->? m b) (var x : a), (var r : b ->? m c)))'

### Hint 18.21-18.36,

untypeable term (with type: _v466_v453_m _v454_a * (_v454_a -> _v466_v453_m _v455_b))

'(p, \ x : a . q x >>= r)'

### Hint 18.29, rebound variable 'x'

### Hint 18.36-18.44,

rejected '__->?__ < __->__' of '((var q : a ->? m b) (var x : a), (var r : b ->? m c))'

### Hint 18.36-18.44,

untypeable term (with type: _v526_v513_m _v514_a * (_v514_a -> _v526_v513_m _v515_b))

'(q x, r)'

### Warning 20.16, refined class 'Monad'

### Hint 21.7, is type variable 'm'

### Hint 21.7, rebound type variable 'm'

### Hint 21.17, is type variable 'a'

### Hint 21.17, rebound type variable 'a'

### Hint 21.20, is type variable 'b'

### Hint 21.20, rebound type variable 'b'

### Hint 21.30, not a class 'a'

### Hint 21.30, not a class 'b'

### Hint 21.29, rebound variable 'f'

### Warning 21.29, variable also known as type variable 'f'

### Hint 21.41, not a kind 'm a'

### Hint 21.40, rebound variable 'x'

### Hint 22.21, rebound variable 'y'

### Hint 22.13-22.35,

rejected '__->?__ < __->__' of '((var x : m a),

\ y : a

. (op ret : forall m : Monad; a : Type . a -> m a)

((var f : a -> b) (var y : a)))'

### Hint 22.13-22.35,

untypeable term (with type: _v621_v608_m _v609_a * (_v609_a -> _v621_v608_m _v610_b))

'(x, \ y : a . ret (f y))'

### Hint 22.21, rebound variable 'y'

### Hint 25.7, is type variable 't'

### Hint 25.18, is type variable 'm'

### Hint 25.18, rebound type variable 'm'

### Hint 25.28, is type variable 'a'

### Hint 25.28, rebound type variable 'a'

### Hint 27.8, not a class 'a'

### Hint 27.7, rebound variable 'x'

### Hint 27.14, not a kind 'm a'

### Hint 27.13, rebound variable 'p'

### Hint 27.21, is type variable 'b'

### Hint 27.21, rebound type variable 'b'

### Hint 27.31, not a kind 'a -> m b'

### Hint 27.30, rebound variable 'q'

### Hint 29.33, rebound variable 'y'

### Hint 29.33, rebound variable 'y'

### Hint 29.33, rebound variable 'y'

### Hint 29.33, rebound variable 'y'

### Hint 31.7, is type variable 'state'

### Hint 33.7, is type variable 'a'

### Hint 33.7, rebound type variable 'a'

### Hint 33.10, is type variable 'b'

### Hint 33.10, rebound type variable 'b'

### Hint 34.30,

no kind found for 'a'

expected: {Cpo}

found: {Type}

### Hint 34.30,

no kind found for 'a'

expected: {Cppo}

found: {Type}

### Hint 34.6, redeclared type 'ST'

### Hint 35.8, not a class 'a'

### Hint 35.7, rebound variable 'x'

### Hint 35.14, not a kind 'ST state a'

### Hint 35.13, rebound variable 'p'

### Hint 35.29, not a kind 'a ->? ST state b'

### Hint 35.28, rebound variable 'q'

### Hint 36.3-36.9,

in type of '(op ret : forall m : Monad; a : Type . a -> m a) (var x : a) :

ST state a'

typename 'a' (35.10)

is not unifiable with type 'a * state' (36.20)

### Hint 36.3-36.42,

untypeable term (with type: ? _v906_a * ? _v906_a)

'(ret x : ST state a, \ s : state . (x, s))'

*** Error 36.3,

no typing for '(ret x : ST state a) = \ s : state . (x, s)'

### Hint 37.3-37.9,

in type of '((var p : ST state a), (var q : a ->? ST state b))'

typename 'a' (35.31)

is not unifiable with type 'a * state' (35.25)

### Hint 37.3-37.9,

untypeable term (with type: _v940_v927_m _v928_a * (_v928_a -> _v940_v927_m _v929_b))

'(p, q)'

### Hint 37.3-37.9,

in type of '((var p : ST state a), (var q : a ->? ST state b))'

typename 'a' (35.31)

is not unifiable with type 'a * state' (35.25)

### Hint 37.3-37.9,

untypeable term (with type: _v949_v930_m _v931_a * (_v931_a ->? _v949_v930_m _v932_b))

'(p, q)'

### Hint 37.5-37.54,

untypeable term (with type: ? _v921_a * ? _v921_a)

'(p >>= q, \ s1 : state . let (z, s2) = p s1 in q z s2)'

*** Error 37.5,

no typing for

'p >>= q = \ s1 : state . let (z, s2) = p s1 in q z s2'