GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-16 20:03:27 +03:00
Code Issues Projects Releases Wiki Activity

Now wild cards in the types of module parameters

Browse Source
This commit is contained in:
Iavor S. Diatchki 2017-10-05 13:49:25 -07:00
parent f7adf8f4ba
commit f64f051842
2 changed files with 5 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
src/Cryptol/TypeCheck/Infer.hs
View File

@ -633,7 +633,7 @@ guessType exprMap b@(P.Bind { .. }) =
case bSignature of
Just s ->
do s1 <- checkSchema s
do s1 <- checkSchema True s
return ((name, ExtVar (fst s1)), Left (checkSigB b s1))
Nothing
@ -851,7 +851,7 @@ inferDs ds continue = checkTyDecls =<< orderTyDecls (mapMaybe toTyDecl ds)
checkParameterFun x =
do (s,gs) <- checkSchema (P.pfSchema x)
do (s,gs) <- checkSchema False (P.pfSchema x)
su <- proveImplication (Just (thing (P.pfName x)))
(sVars s) (sProps s) gs
unless (isEmptySubst su) $

6
src/Cryptol/TypeCheck/Kind.hs
View File

@ -39,11 +39,11 @@ import Control.Monad(unless,forM)
-- | Check a type signature.
checkSchema :: P.Schema Name -> InferM (Schema, [Goal])
checkSchema (P.Forall xs ps t mb) =
checkSchema :: Bool -> P.Schema Name -> InferM (Schema, [Goal])
checkSchema withWild (P.Forall xs ps t mb) =
do ((xs1,(ps1,t1)), gs) <-
collectGoals $
rng $ withTParams True schemaParam xs $
rng $ withTParams withWild schemaParam xs $
do ps1 <- mapM checkProp ps
t1 <- doCheckType t (Just KType)
return (ps1,t1)