From 0fb5b085988154e5dc3cacbf55e79d4c403f5f63 Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Tue, 29 Oct 2024 16:35:34 -0700 Subject: [PATCH] Typeclass works for Monad --- TODO.md | 19 ++-------- newt/TypeClass.newt | 61 +---------------------------- src/Lib/CompileExp.idr | 2 +- src/Lib/Elab.idr | 78 ++++++++++++++++++++++++++++++-------- src/Lib/Eval.idr | 32 ++-------------- src/Lib/ProcessDecl.idr | 28 ++++++++------ src/Lib/Types.idr | 13 +++++-- tests/black/Tree.newt | 3 -- tests/black/TypeClass.newt | 37 +++++++++++------- 9 files changed, 120 insertions(+), 153 deletions(-) diff --git a/TODO.md b/TODO.md index 5d81bc2..e6e40ba 100644 --- a/TODO.md +++ b/TODO.md @@ -1,21 +1,13 @@ ## TODO -NOW - two things - -1. I broke Tree.newt by removing some over-aggressive reduction. I need to -make it happen during unification. Not sure if I have all of the bits to vappspine there. - -2. Need to collect constraints and re-run, I think that may get me to -typeclasses - - [x] Remember operators from imports - [ ] Default cases for non-primitives (currently gets expanded to all constructors) - [x] Case for primitives - [ ] aoc2023 translation - [x] day1 - [x] day2 - - some "real world" examples + - some "real world" examples -v - [x] Maybe Eq and stuff would work for typeclass without dealing with unification issues yet - [x] unsolved meta errors repeat (need to freeze or only report at end) - [x] Sanitize JS idents, e.g. `_+_` @@ -46,12 +38,7 @@ typeclasses - Agda doesn't have it, clashes with pair syntax - [ ] autos / typeclass resolution - [x] very primitive version in place, not higher order, search at end - - We need special handling in unification to make this possible for typeclasses on `U -> U`, we could still do `Eq` or `Show` with the current unification - - options - - keep as implicit and do auto if the type constructor is flagged auto - - keep as implicit and mark auto, behavior overlaps a lot with implicit - - have separate type of implict with `{{}}` - - `TypeClass.newt` is the exercise for this + - [x] monad is now working - [ ] do blocks (needs typeclass, overloaded functions, or constrain to IO) - [x] some solution for `+` problem (classes? ambiguity?) - [x] show compiler failure in the editor (exit code != 0) @@ -67,7 +54,7 @@ typeclasses - I think we got this by not switching for single cases - [ ] magic nat (codegen as number with appropriate pattern matching) - [ ] magic tuple? (codegen as array) -- [ ] magic newtype? (drop in codegen) +- [ ] magic newtype? (drop them in codegen) - [ ] records / copatterns - [x] vscode: syntax highlighting for String - [ ] add `pop` or variant of `pfunc` that maps to an operator, giving the js operator and precedence on RHS diff --git a/newt/TypeClass.newt b/newt/TypeClass.newt index 44bbc70..d83daa0 100644 --- a/newt/TypeClass.newt +++ b/newt/TypeClass.newt @@ -1,17 +1,5 @@ module TypeClass --- experiment on one option for typeclass (we don't have record yet) - --- this would be nicer with records and copatterns - --- At this point, for Agda style, I'll probably need to postpone, or collect constraints --- at lesat. Idris style, I might get away without short term. - --- So I can read mcbride paper and maybe agda source. - - - --- we need a bit more than this, but data Monad : (U -> U) -> U where MkMonad : { M : U -> U } -> (bind : {A B : U} -> (M A) -> (A -> M B) -> M B) -> @@ -21,7 +9,6 @@ data Maybe : U -> U where Just : {A : U} -> A -> Maybe A Nothing : {A : U} -> Maybe A - data Either : U -> U -> U where Left : {A B : U} -> A -> Either A B Right : {A B : U} -> B -> Either A B @@ -37,14 +24,9 @@ bindMaybe : {A B : U} -> Maybe A -> (A -> Maybe B) -> Maybe B bindMaybe Nothing amb = Nothing bindMaybe (Just a) amb = amb a --- I think it was picking up the Maybe before I made it less aggressive about eval - MaybeMonad : Monad Maybe MaybeMonad = MkMonad bindMaybe --- So the idea here is to have some implicits that are solved by search - --- Error here is from foo, with a bad FC. I think it might be showing up during search. _>>=_ : {a b : U} -> {m : U -> U} -> {{x : Monad m}} -> (m a) -> (a -> m b) -> m b _>>=_ {a} {b} {m} {{MkMonad bind'}} ma amb = bind' {a} {b} ma amb @@ -52,46 +34,5 @@ infixl 1 _>>=_ ptype Int --- It's bailing on MaybeMonad and picking up Either? - foo : Int -> Maybe Int -foo x = (Just x) >>= (\ x => Just 10) - --- NOW - --- Older notes below, but this is _close_, we're doing something like agda, and we're getting the right solution --- It's over-expanded, and there is an unsolved meta that I think the solution would unlock. (Need to collect and --- retry constraints) - --- *SOLVE meta 6 sp [< (%var 0 [< ]), (%meta 4 [< (%var 0 [< ])])] val (%ref Maybe [< (%meta 9 [< (%var 0 [< ]), (%var 1 [< ])])]) - --- Essentially (m6 v0) (m4 ...) == Maybe Int and (m6 v0) (m2 v0) == Maybe Int - --- Idris gets this by specially treating determining arguments of an auto as "invertible". It then unifies --- the last arg on each side and tries the rest, which is now in the pattern fragment. - --- Agda may do this slightly differently from Idris: --- https://agda.readthedocs.io/en/v2.6.0.1/language/instance-arguments.html#instance-resolution - --- I think it searches, pulls in all possibilities and tries to unify them into place. --- We'll want to extend our example to what I have in Foo2.agda to test that it finds the right --- one. Maybe look at the source to see if there is any invertible trickery going on? - --- I know that here, if I fill in the instance, everything works out, so finding the instance that works --- out might be sufficient. That might mean that a instance constraint is a pile of options that get --- winnowed down? - --- Putting MaybeMonad in there helps the unification --- of Maybe Int =?= ?m6 ?m2 (as Monad Maybe (the type) gives ?m6 is Maybe) --- and MaybeEither would fail after a couple of steps. But it seems expensive/complex --- to have to run the process down for each candidate. - --- Agda seems complicated, minting fresh metas for bits of potential solutions (which --- may be tossed if the solution is ruled out.) - - --- ^ -/- -So, agda style we'd guess ?m8 is MonadMaybe or MonadEither - agda's "maybe" case - --/ +foo x = (Just x) >>= (\ x => Just 10) diff --git a/src/Lib/CompileExp.idr b/src/Lib/CompileExp.idr index c99c359..67a7012 100644 --- a/src/Lib/CompileExp.idr +++ b/src/Lib/CompileExp.idr @@ -93,7 +93,7 @@ compileTerm tm@(App _ _ _) with (funArgs tm) -- apply (CRef "Meta\{show k}") args' [<] 0 arity <- case meta of -- maybe throw - (Unsolved x j ctx _ _) => pure 0 -- FIXME # of Bound in ctx.bds + (Unsolved x j ctx _ _ _) => pure 0 -- FIXME # of Bound in ctx.bds (Solved j tm) => pure $ getArity !(quote 0 tm) apply (CRef "Meta\{show k}") args' [<] arity _ | (t@(Ref fc nm _), args) = do diff --git a/src/Lib/Elab.idr b/src/Lib/Elab.idr index d281091..26118a9 100644 --- a/src/Lib/Elab.idr +++ b/src/Lib/Elab.idr @@ -9,6 +9,7 @@ import Lib.Prettier import Data.List import Data.Vect import Data.String +import Data.IORef import Lib.Types import Lib.Eval import Lib.TopContext @@ -53,7 +54,7 @@ lookupDef ctx name = go 0 ctx.types ctx.env export forceMeta : Val -> M Val forceMeta (VMeta fc ix sp) = case !(lookupMeta ix) of - (Unsolved pos k xs _ _) => pure (VMeta fc ix sp) + (Unsolved pos k xs _ _ _) => pure (VMeta fc ix sp) (Solved k t) => vappSpine t sp >>= forceMeta forceMeta x = pure x @@ -70,7 +71,7 @@ tryEval k sp = -- Force far enough to compare types forceType : Val -> M Val forceType (VMeta fc ix sp) = case !(lookupMeta ix) of - (Unsolved x k xs _ _) => pure (VMeta fc ix sp) + (Unsolved x k xs _ _ _) => pure (VMeta fc ix sp) (Solved k t) => vappSpine t sp >>= forceType forceType x@(VRef fc nm _ sp) = fromMaybe x <$> tryEval nm sp forceType x = pure x @@ -87,6 +88,30 @@ Semigroup UnifyResult where Monoid UnifyResult where neutral = MkResult [] +-- We need to switch to SortedMap here +export +updateMeta : Context -> Nat -> (MetaEntry -> M MetaEntry) -> M () +updateMeta ctx ix f = do + mc <- readIORef ctx.metas + metas <- go mc.metas + writeIORef ctx.metas $ {metas := metas} mc + where + go : List MetaEntry -> M (List MetaEntry) + go [] = error' "Meta \{show ix} not found" + go (x@((Unsolved y k z w v ys)) :: xs) = if k == ix then (::xs) <$> f x else (x ::) <$> go xs + go (x@((Solved k y)) :: xs) = if k == ix then (::xs) <$> f x else (x ::) <$> go xs + +export +addConstraint : Context -> Nat -> SnocList Val -> Val -> M () +addConstraint ctx ix sp tm = do + mc <- readIORef ctx.metas + updateMeta ctx ix $ \case + (Unsolved pos k a b c cons) => do + info (getFC tm) "Add constraint m\{show ix} \{show sp} =?= \{show tm}" + pure (Unsolved pos k a b c (MkMc (getFC tm) ctx sp tm :: cons)) + (Solved k tm) => error' "Meta \{show k} already solved" + pure () + parameters (ctx: Context) -- return renaming, the position is the new VVar invert : Nat -> SnocList Val -> M (List Nat) @@ -140,28 +165,51 @@ parameters (ctx: Context) -- REVIEW can I get better names in here? lams (S k) tm = Lam emptyFC "arg_\{show k}" (lams k tm) + + export + unify : (l : Nat) -> Val -> Val -> M UnifyResult + export solve : (lvl : Nat) -> (k : Nat) -> SnocList Val -> Val -> M () solve l m sp t = do - meta@(Unsolved metaFC ix ctx ty kind) <- lookupMeta m + meta@(Unsolved metaFC ix ctx ty kind cons) <- lookupMeta m | _ => error (getFC t) "Meta \{show m} already solved!" debug "SOLVE \{show m} \{show kind} lvl \{show l} sp \{show sp} is \{show t}" let size = length $ filter (\x => x == Bound) $ toList ctx.bds - debug "\{show m} size is \{show size}" - if (length sp /= size) then do + debug "\{show m} size is \{show size} sps \{show $ length sp}" + let True = length sp == size + | _ => do -- need INFO that works like debug. -- FIXME we probably need to hold onto the constraint and recheck when we solve the meta? info (getFC t) "meta \{show m} (\{show ix}) applied to \{show $ length sp} args instead of \{show size}" + debug "CONSTRAINT m\{show ix} \{show sp} =?= \{show t}" -- error (getFC t) "meta \{show m} applied to \{show $ length sp} args instead of \{show size}" - else do - debug "meta \{show meta}" - ren <- invert l sp - tm <- rename m ren l t - let tm = lams (length sp) tm - top <- get - soln <- eval [] CBN tm - solveMeta top m soln - pure () + +-- add constraint to meta m +-- we can keep a list and run them when it is solved. + addConstraint ctx m sp t + + debug "meta \{show meta}" + ren <- invert l sp + tm <- rename m ren l t + let tm = lams (length sp) tm + top <- get + soln <- eval [] CBN tm + + updateMeta ctx m $ \case + (Unsolved pos k _ _ _ cons) => do + putStrLn "INFO at \{show pos}: solve \{show k} as \{pprint [] !(quote 0 soln)}" + pure $ Solved k soln + (Solved k x) => error' "Meta \{show ix} already solved!" + -- We're not breaking anything, but not quite getting an answer? + for_ cons $ \case + MkMc fc ctx sp rhs => do + val <- vappSpine soln sp + debug "discharge l=\{show ctx.lvl} \{(show val)} =?= \{(show rhs)}" + -- is this the right depth? + unify ctx.lvl val rhs + + pure () trySolve : Nat -> Nat -> SnocList Val -> Val -> M () trySolve l m sp t = do @@ -170,8 +218,6 @@ parameters (ctx: Context) pure ()) - export - unify : (l : Nat) -> Val -> Val -> M UnifyResult unifySpine : Nat -> Bool -> SnocList Val -> SnocList Val -> M UnifyResult unifySpine l False _ _ = error emptyFC "unify failed at head" -- unreachable now diff --git a/src/Lib/Eval.idr b/src/Lib/Eval.idr index 1ab0aac..d836324 100644 --- a/src/Lib/Eval.idr +++ b/src/Lib/Eval.idr @@ -79,7 +79,7 @@ eval env mode (App _ t u) = vapp !(eval env mode t) !(eval env mode u) eval env mode (U fc) = pure (VU fc) eval env mode (Meta fc i) = case !(lookupMeta i) of - (Unsolved _ k xs _ _) => pure $ VMeta fc i [<] + (Unsolved _ k xs _ _ _) => pure $ VMeta fc i [<] (Solved k t) => pure $ t eval env mode (Lam fc x t) = pure $ VLam fc x (MkClosure env t) eval env mode (Pi fc x icit a b) = pure $ VPi fc x icit !(eval env mode a) (MkClosure env b) @@ -112,7 +112,7 @@ quote l (VVar fc k sp) = if k < l else ?borken quote l (VMeta fc i sp) = case !(lookupMeta i) of - (Unsolved _ k xs _ _) => quoteSp l (Meta fc i) sp + (Unsolved _ k xs _ _ _) => quoteSp l (Meta fc i) sp (Solved k t) => quote l !(vappSpine t sp) quote l (VLam fc x t) = pure $ Lam fc x !(quote (S l) !(t $$ VVar emptyFC l [<])) quote l (VPi fc x icit a b) = pure $ Pi fc x icit !(quote l a) !(quote (S l) !(b $$ VVar emptyFC l [<])) @@ -128,35 +128,10 @@ export nf : Env -> Tm -> M Tm nf env t = quote (length env) !(eval env CBN t) -export -prval : Val -> M String -prval v = pure $ pprint [] !(quote 0 v) - export prvalCtx : {auto ctx : Context} -> Val -> M String prvalCtx v = pure $ pprint (toList $ map fst ctx.types) !(quote ctx.lvl v) - -export -solveMeta : TopContext -> Nat -> Val -> M () -solveMeta ctx ix tm = do - mc <- readIORef ctx.metas - metas <- go mc.metas [<] - writeIORef ctx.metas $ {metas := metas} mc - where - go : List MetaEntry -> SnocList MetaEntry -> M (List MetaEntry) - go [] _ = error' "Meta \{show ix} not found" - go (meta@(Unsolved pos k _ _ _) :: xs) lhs = if k == ix - then do - -- empty context should be ok, because this needs to be closed - putStrLn "INFO at \{show pos}: solve \{show k} as \{!(prval tm)}" - pure $ lhs <>> (Solved k tm :: xs) - else go xs (lhs :< meta) - go (meta@(Solved k _) :: xs) lhs = if k == ix - then error' "Meta \{show ix} already solved!" - else go xs (lhs :< meta) - - -- REVIEW - might be easier if we inserted the meta without a bunch of explicit App -- I believe Kovacs is doing that. @@ -183,6 +158,7 @@ appSpine : Tm -> List Tm -> Tm appSpine t [] = t appSpine t (x :: xs) = appSpine (App (getFC t) t x) xs +-- TODO replace this with a variant on nf zonkApp : TopContext -> Nat -> Env -> Tm -> List Tm -> M Tm zonkApp top l env (App fc t u) sp = zonkApp top l env t (!(zonk top l env u) :: sp) zonkApp top l env t@(Meta fc k) sp = case !(lookupMeta k) of @@ -192,7 +168,7 @@ zonkApp top l env t@(Meta fc k) sp = case !(lookupMeta k) of foo <- vappSpine v ([<] <>< sp') debug "-> result is \{show foo}" quote l foo - (Unsolved x j xs _ _) => pure $ appSpine t sp + (Unsolved x j xs _ _ _) => pure $ appSpine t sp zonkApp top l env t sp = pure $ appSpine !(zonk top l env t) sp zonkAlt : TopContext -> Nat -> Env -> CaseAlt -> M CaseAlt diff --git a/src/Lib/ProcessDecl.idr b/src/Lib/ProcessDecl.idr index a9d7059..9d3a4da 100644 --- a/src/Lib/ProcessDecl.idr +++ b/src/Lib/ProcessDecl.idr @@ -25,7 +25,7 @@ isCandidate _ _ = False -- This is a crude first pass -- TODO consider ctx -findMatches : Val -> List TopEntry -> M (List Tm) +findMatches : Val -> List TopEntry -> M (List (Tm, MetaContext)) findMatches ty [] = pure [] findMatches ty ((MkEntry name type def@(Fn t)) :: xs) = do let True = isCandidate ty type | False => findMatches ty xs @@ -38,10 +38,12 @@ findMatches ty ((MkEntry name type def@(Fn t)) :: xs) = do -- TODO sort out the FC here let fc = getFC ty debug "TRY \{name} : \{pprint [] type} for \{show ty}" - tm <- check (mkCtx top.metas fc) (RVar fc name) ty + -- This check is solving metas, so we save mc below in case we want this solution + tm <- check (mkCtx top.metas fc) (RVar fc name) ty debug "Found \{pprint [] tm} for \{show ty}" + mc' <- readIORef top.metas writeIORef top.metas mc - (tm ::) <$> findMatches ty xs) + ((tm, mc') ::) <$> findMatches ty xs) (\ err => do debug "No match \{show ty} \{pprint [] type} \{showError "" err}" writeIORef top.metas mc @@ -127,14 +129,16 @@ processDecl (Def fc nm clauses) = do mc <- readIORef top.metas let mlen = length mc.metas `minus` mstart + -- FIXME every time we hit solve in this loop, we need to start over with mc.metas for_ (take mlen mc.metas) $ \case - (Unsolved fc k ctx ty AutoSolve) => do - debug "auto solving \{show k} : \{show ty}" + (Unsolved fc k ctx ty AutoSolve _) => do + debug "AUTO solving \{show k} : \{show ty}" -- we want the context here too. - [tm] <- findMatches ty top.defs - | res => error fc "Failed to solve \{show ty}, matches: \{show $ map (pprint []) res}" + [(tm,mc)] <- findMatches ty top.defs + | res => error fc "FAILED to solve \{show ty}, matches: \{show $ map (pprint [] . fst) res}" + writeIORef top.metas mc val <- eval ctx.env CBN tm - debug "solution \{pprint [] tm} evaled to \{show val}" + debug "SOLUTION \{pprint [] tm} evaled to \{show val}" let sp = makeSpine ctx.lvl ctx.bds solve ctx ctx.lvl k sp val pure () @@ -146,13 +150,15 @@ processDecl (Def fc nm clauses) = do mc <- readIORef top.metas for_ (take mlen mc.metas) $ \case (Solved k x) => pure () - (Unsolved (l,c) k ctx ty User) => do + (Unsolved (l,c) k ctx ty User cons) => do -- TODO print here instead of during Elab pure () - (Unsolved (l,c) k ctx ty kind) => do + (Unsolved (l,c) k ctx ty kind cons) => do tm <- quote ctx.lvl !(forceMeta ty) -- Now that we're collecting errors, maybe we simply check at the end - addError $ E (l,c) "Unsolved meta \{show k} \{show kind} type \{pprint (names ctx) tm}" + -- TODO - log constraints? + addError $ E (l,c) "Unsolved meta \{show k} \{show kind} type \{pprint (names ctx) tm} \{show $ length cons} constraints" + debug "Add def \{nm} \{pprint [] tm'} : \{pprint [] ty}" modify $ setDef nm ty (Fn tm') diff --git a/src/Lib/Types.idr b/src/Lib/Types.idr index bd29ecc..abf3910 100644 --- a/src/Lib/Types.idr +++ b/src/Lib/Types.idr @@ -325,8 +325,12 @@ Show MetaKind where show User = "User" show AutoSolve = "Auto" +-- constrain meta applied to val to be a val public export -data MetaEntry = Unsolved FC Nat Context Val MetaKind | Solved Nat Val +data MConstraint = MkMc FC Context (SnocList Val) Val + +public export +data MetaEntry = Unsolved FC Nat Context Val MetaKind (List MConstraint) | Solved Nat Val public export @@ -399,6 +403,7 @@ record Context where metas : IORef MetaContext fc : FC +%name Context ctx ||| add a binding to environment export @@ -416,7 +421,7 @@ define ctx name val ty = export covering Show MetaEntry where - show (Unsolved pos k ctx ty kind) = "Unsolved \{show pos} \{show k} \{show kind} : \{show ty} \{show ctx.bds}" + show (Unsolved pos k ctx ty kind constraints) = "Unsolved \{show pos} \{show k} \{show kind} : \{show ty} \{show ctx.bds} cs \{show $ length constraints}" show (Solved k x) = "Solved \{show k} \{show x}" export withPos : Context -> FC -> Context @@ -447,7 +452,7 @@ freshMeta : Context -> FC -> Val -> MetaKind -> M Tm freshMeta ctx fc ty kind = do mc <- readIORef ctx.metas putStrLn "INFO at \{show fc}: fresh meta \{show mc.next} : \{show ty}" - writeIORef ctx.metas $ { next $= S, metas $= (Unsolved fc mc.next ctx ty kind ::) } mc + writeIORef ctx.metas $ { next $= S, metas $= (Unsolved fc mc.next ctx ty kind [] ::) } mc pure $ applyBDs 0 (Meta emptyFC mc.next) ctx.bds where -- hope I got the right order here :) @@ -471,7 +476,7 @@ lookupMeta ix = do where go : List MetaEntry -> M MetaEntry go [] = error' "Meta \{show ix} not found" - go (meta@(Unsolved _ k ys _ _) :: xs) = if k == ix then pure meta else go xs + go (meta@(Unsolved _ k ys _ _ _) :: xs) = if k == ix then pure meta else go xs go (meta@(Solved k x) :: xs) = if k == ix then pure meta else go xs -- we need more of topcontext later - Maybe switch it up so we're not passing diff --git a/tests/black/Tree.newt b/tests/black/Tree.newt index 243d7af..9346e37 100644 --- a/tests/black/Tree.newt +++ b/tests/black/Tree.newt @@ -91,9 +91,6 @@ insert (intv x lx xu) (node2 y tly tyu) = case cmp x y of inr tyu' => inr (node2 y tly tyu') insert (intv x lx xu) (node3 y z tly tyz tzu) = case cmp x y of inl xy => case insert (intv {_} {N y} x lx xy) tly of - -- TODO Here a meta is applied to an extra argument, if we ignore that - -- constraint we get a better one later - _but_ we probably need to check - -- the constraint later. inl (v ** (tlv , tvy)) => inl (y ** (node2 v tlv tvy, node2 z tyz tzu)) inr tly' => inr (node3 y z tly' tyz tzu) inr yx => case cmp x z of diff --git a/tests/black/TypeClass.newt b/tests/black/TypeClass.newt index 0b08c4d..d83daa0 100644 --- a/tests/black/TypeClass.newt +++ b/tests/black/TypeClass.newt @@ -1,8 +1,5 @@ module TypeClass --- experiment on one option for typeclass (we don't have record yet) - --- we need a bit more than this, but data Monad : (U -> U) -> U where MkMonad : { M : U -> U } -> (bind : {A B : U} -> (M A) -> (A -> M B) -> M B) -> @@ -12,18 +9,30 @@ data Maybe : U -> U where Just : {A : U} -> A -> Maybe A Nothing : {A : U} -> Maybe A +data Either : U -> U -> U where + Left : {A B : U} -> A -> Either A B + Right : {A B : U} -> B -> Either A B --- NEXT trying to get this to work. An equivalence is not found in pattern --- matching +bindEither : {A B C : U} -> (Either A B) -> (B -> Either A C) -> Either A C +bindEither (Left a) amb = Left a +bindEither (Right b) amb = amb b + +EitherMonad : {A : U} -> Monad (Either A) +EitherMonad = MkMonad {Either A} bindEither + +bindMaybe : {A B : U} -> Maybe A -> (A -> Maybe B) -> Maybe B +bindMaybe Nothing amb = Nothing +bindMaybe (Just a) amb = amb a --- [instance] MaybeMonad : Monad Maybe --- Agda case lambda might be nice.. --- The {Maybe} isn't solved in type for the case -MaybeMonad = MkMonad {Maybe} (\ {A} ma amb => - case ma of - Nothing => Nothing - -- It doesn't discover pat$5 is A during pattern matching - -- oh, but var 0 value is var5 - Just a => amb a) +MaybeMonad = MkMonad bindMaybe +_>>=_ : {a b : U} -> {m : U -> U} -> {{x : Monad m}} -> (m a) -> (a -> m b) -> m b +_>>=_ {a} {b} {m} {{MkMonad bind'}} ma amb = bind' {a} {b} ma amb + +infixl 1 _>>=_ + +ptype Int + +foo : Int -> Maybe Int +foo x = (Just x) >>= (\ x => Just 10)