tests all pass

This commit is contained in:
Paul Chiusano 2018-08-13 12:38:53 -04:00
parent c29742a958
commit c87997e482
2 changed files with 11 additions and 12 deletions

View File

@ -492,9 +492,10 @@ synthesizeApp :: (Var v, Ord loc) => Type v loc -> Term v loc -> M v loc (Type v
synthesizeApp (Type.Effect'' es ft) arg =
scope (InSynthesizeApp ft arg) $ do
abilityCheck es
Type.Effect'' es t <- go ft
abilityCheck es
pure t
go ft
--Type.Effect'' es t <- go ft
--abilityCheck es
--pure t
where
go (Type.Forall' body) = do -- Forall1App
v <- ABT.freshen body freshenTypeVar
@ -1064,7 +1065,9 @@ solve ctx v t
abilityCheck' :: (Var v, Ord loc) => [Type v loc] -> [Type v loc] -> M v loc ()
abilityCheck' ambient requested = do
success <- flip allM requested $ \req -> do
ok <- flip anyM ambient $ \amb -> (True <$ subtype amb req) `orElse` pure False
-- NB - if there's an exact match, use that
let toCheck = maybe ambient pure $ find (== req) ambient
ok <- flip anyM toCheck $ \amb -> (True <$ subtype amb req) `orElse` pure False
case ok of
True -> pure True
-- allow a type variable to unify with the empty effect list

View File

@ -403,7 +403,7 @@ test = scope "typechecker" . tests $
|y = handle state 5 in ex ()
|
|() |]
, broken [r|--map/traverse
, checks [r|--map/traverse
|effect Noop where
| noop : a . a -> {Noop} a
|
@ -412,7 +412,7 @@ test = scope "typechecker" . tests $
|
|type List a = Nil | Cons a (List a)
|
|map : a b e . (a -> {e} b) -> List a -> {e} (List b)
|map : (a -> {eff!,eff2!} b) -> List a -> {eff!,eff2!} (List b)
|map f as = case as of
| List.Nil -> List.Nil
| List.Cons h t -> List.Cons (f h) (map f t)
@ -424,12 +424,8 @@ test = scope "typechecker" . tests $
|
|ex = (c 1 (c 2 (c 3 z)))
|
|-- doesn't currently work due to ability check failure,
|-- map has ` e . {e}` effects, but no effects are in scope
|-- seems we should tweak ability check - when no effects
|-- in scope, {e} can be instantiated to {}
|pure-map : List Text
|pure-map = map (a -> "hello") ex
|-- pure-map : List Text
|-- pure-map = map (a -> "hello") ex
|
|-- `map` is effect polymorphic
|zappy : () -> {Noop} (List UInt64)