diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2009-12-26 11:56:40 -0500 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2009-12-26 11:56:40 -0500 |
| commit | 2ace64baba707b2e76778c74789735263eb50823 (patch) | |
| tree | b4c6e798738335ded8d209afc369885664396d08 /lib/ur/monad.urs | |
| parent | 7aa1234891f8831449a573ec067348c89c22692f (diff) | |
Make summary unification more conservative; infer implicit arguments after applications
Diffstat (limited to 'lib/ur/monad.urs')
| -rw-r--r-- | lib/ur/monad.urs | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/lib/ur/monad.urs b/lib/ur/monad.urs index 9ad9262d..698a4b5b 100644 --- a/lib/ur/monad.urs +++ b/lib/ur/monad.urs @@ -14,7 +14,7 @@ val foldR : K --> m ::: (Type -> Type) -> monad m -> [[nm] ~ rest] => tf t -> tr rest -> m (tr ([nm = t] ++ rest))) -> tr [] - -> r :: {K} -> folder r -> $(map tf r) -> m (tr r) + -> r ::: {K} -> folder r -> $(map tf r) -> m (tr r) val foldR2 : K --> m ::: (Type -> Type) -> monad m -> tf1 :: (K -> Type) -> tf2 :: (K -> Type) @@ -23,7 +23,7 @@ val foldR2 : K --> m ::: (Type -> Type) -> monad m -> [[nm] ~ rest] => tf1 t -> tf2 t -> tr rest -> m (tr ([nm = t] ++ rest))) -> tr [] - -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> m (tr r) + -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> m (tr r) val foldR3 : K --> m ::: (Type -> Type) -> monad m -> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type) @@ -32,16 +32,16 @@ val foldR3 : K --> m ::: (Type -> Type) -> monad m -> [[nm] ~ rest] => tf1 t -> tf2 t -> tf3 t -> tr rest -> m (tr ([nm = t] ++ rest))) -> tr [] - -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> m (tr r) + -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> m (tr r) val mapR : K --> m ::: (Type -> Type) -> monad m -> tf :: (K -> Type) -> tr :: (K -> Type) -> (nm :: Name -> t :: K -> tf t -> m (tr t)) - -> r :: {K} -> folder r -> $(map tf r) -> m ($(map tr r)) + -> r ::: {K} -> folder r -> $(map tf r) -> m ($(map tr r)) val mapR2 : K --> m ::: (Type -> Type) -> monad m -> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tr :: (K -> Type) -> (nm :: Name -> t :: K -> tf1 t -> tf2 t -> m (tr t)) - -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> m ($(map tr r)) + -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> m ($(map tr r)) |