310378e · rowtype-yoga/purescript-native

git.iko.soy/rowtype-yoga/purescript-native

on golang help sign in

Support constrained types in the subsumes check #138

310378ePhil Freeman13 years ago

examples/passing/TypeClasses.purs+6−1

compare with golang

unifiedsplit

@@ -13,6 +13,9 @@ f x = show x

14test2 = \ -> f "testing"

16+test7 :: forall a. (Show a) => a -> String

17+test7 = show

18+

16data Data a = Data a

19data Data a = Data a

18instance (TypeClasses.Show a) => TypeClasses.Show (Data a) where

21instance (TypeClasses.Show a) => TypeClasses.Show (Data a) where

@@ -52,5 +55,7 @@ test6 = \ -> show ["testing"]

53module Main where

56module Main where

58+import TypeClasses

59+

55−main = Trace.trace "Done"

60+main = Trace.trace (test7 "Done")

src/Language/PureScript/TypeChecker/Types.hs+34−20

@@ -428,7 +428,7 @@ infer' (Accessor prop val) = do

428 Nothing -> do

429 field <- fresh

430 rest <- fresh

431− objTy `subsumes` Object (RCons prop field rest)

431+ _ <- subsumes Nothing objTy (Object (RCons prop field rest))

432 return $ TypedValue True (Accessor prop typed) field

433 Just ty -> return $ TypedValue True (Accessor prop typed) ty

434infer' (Abs args ret) = do

@@ -609,7 +609,7 @@ inferBinder val (NullaryBinder ctor) = do

609 Just moduleName <- checkCurrentModule <$> get

610 case M.lookup (qualify moduleName ctor) (dataConstructors env) of

611 Just (ty, _) -> do

612− ty `subsumes` val

612+ _ <- subsumes Nothing ty val

613 return M.empty

614 _ -> throwError $ "Constructor " ++ show ctor ++ " is not defined"

615inferBinder val (UnaryBinder ctor binder) = do

@@ -620,7 +620,7 @@ inferBinder val (UnaryBinder ctor binder) = do

620 fn <- replaceAllVarsWithUnknowns ty

621 case fn of

622 Function [obj] ret -> do

623− val `subsumes` ret

623+ _ <- subsumes Nothing val ret

624 inferBinder obj binder

625 _ -> throwError $ "Constructor " ++ show ctor ++ " is not a unary constructor"

626 _ -> throwError $ "Constructor " ++ show ctor ++ " is not defined"

@@ -818,19 +818,24 @@ check' (App f args) ret = do

818 f'@(TypedValue _ _ ft) <- infer f

819 app <- checkFunctionApplication f' ft args ret

820 return $ app

821−check' (Var var) ty = do

821+check' v@(Var var) ty = do

822 Just moduleName <- checkCurrentModule <$> get

823 ty1 <- lookupVariable moduleName var

824 repl <- replaceAllTypeSynonyms ty1

825− repl `subsumes` ty

825+ v' <- subsumes (Just v) repl ty

826+ case v' of

827+ Nothing -> throwError "Unable to check type subsumption"

826− return $ Var var

828+ Just v'' -> return v''

827check' (TypedValue checkType val ty1) ty2 = do

829check' (TypedValue checkType val ty1) ty2 = do

828 Just moduleName <- checkCurrentModule <$> get

830 Just moduleName <- checkCurrentModule <$> get

829 kind <- liftCheck $ kindOf moduleName ty1

831 kind <- liftCheck $ kindOf moduleName ty1

830 guardWith ("Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star

832 guardWith ("Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star

831− ty1 `subsumes` ty2

833+ val' <- subsumes (Just val) ty1 ty2

834+ case val' of

835+ Nothing -> throwError "Unable to check type subsumption"

836+ Just val'' -> do

832− val' <- if checkType then check val ty1 else return val

837+ val''' <- if checkType then check val'' ty1 else return val''

833− return $ TypedValue True val' ty1

838+ return $ TypedValue True val''' ty1

834check' (Case vals binders) ret = do

839check' (Case vals binders) ret = do

835 vals' <- mapM infer vals

840 vals' <- mapM infer vals

836 let ts = map (\(TypedValue _ _ t) -> t) vals'

841 let ts = map (\(TypedValue _ _ t) -> t) vals'

@@ -869,7 +874,7 @@ check' (Constructor c) ty = do

869 Nothing -> throwError $ "Constructor " ++ show c ++ " is undefined"

874 Nothing -> throwError $ "Constructor " ++ show c ++ " is undefined"

870 Just (ty1, _) -> do

875 Just (ty1, _) -> do

871 repl <- replaceAllTypeSynonyms ty1

876 repl <- replaceAllTypeSynonyms ty1

872− repl `subsumes` ty

877+ _ <- subsumes Nothing repl ty

873 return $ Constructor c

878 return $ Constructor c

874check' val (SaturatedTypeSynonym name args) = do

879check' val (SaturatedTypeSynonym name args) = do

875 ty <- expandTypeSynonym name args

880 ty <- expandTypeSynonym name args

@@ -928,7 +933,7 @@ checkFunctionApplication' :: Value -> Type -> [Value] -> Type -> UnifyT Check Va

928checkFunctionApplication' fn (Function argTys retTy) args ret = do

933checkFunctionApplication' fn (Function argTys retTy) args ret = do

929 guardWith "Incorrect number of function arguments" (length args == length argTys)

934 guardWith "Incorrect number of function arguments" (length args == length argTys)

930 args' <- zipWithM check args argTys

935 args' <- zipWithM check args argTys

931− retTy `subsumes` ret

936+ _ <- subsumes Nothing retTy ret

932 return $ App fn args'

937 return $ App fn args'

933checkFunctionApplication' fn (ForAll ident ty) args ret = do

938checkFunctionApplication' fn (ForAll ident ty) args ret = do

934 replaced <- replaceVarWithUnknown ident ty

939 replaced <- replaceVarWithUnknown ident ty

@@ -954,8 +959,8 @@ checkFunctionApplication' _ fnTy args ret = throwError $ "Applying a function of

954-- |

959-- |

955-- Check whether one type subsumes another, rethrowing errors to provide a better error message

960-- Check whether one type subsumes another, rethrowing errors to provide a better error message

956--

961--

957−subsumes :: Type -> Type -> UnifyT Check ()

962+subsumes :: Maybe Value -> Type -> Type -> UnifyT Check (Maybe Value)

958−subsumes ty1 ty2 = rethrow errorMessage $ subsumes' ty1 ty2

963+subsumes val ty1 ty2 = rethrow errorMessage $ subsumes' val ty1 ty2

959 where

964 where

960 errorMessage msg = "Error checking that type "

965 errorMessage msg = "Error checking that type "

961 ++ prettyPrintType ty1

966 ++ prettyPrintType ty1

@@ -966,12 +971,21 @@ subsumes ty1 ty2 = rethrow errorMessage $ subsumes' ty1 ty2

966-- |

971-- |

967-- Check whether one type subsumes another

972-- Check whether one type subsumes another

968--

973--

969−subsumes' :: Type -> Type -> UnifyT Check ()

974+subsumes' :: Maybe Value -> Type -> Type -> UnifyT Check (Maybe Value)

970−subsumes' (ForAll ident ty1) ty2 = do

975+subsumes' val (ForAll ident ty1) ty2 = do

971 replaced <- replaceVarWithUnknown ident ty1

976 replaced <- replaceVarWithUnknown ident ty1

972− replaced `subsumes` ty2

977+ subsumes val replaced ty2

973−subsumes' (Function args1 ret1) (Function args2 ret2) = do

978+subsumes' val (Function args1 ret1) (Function args2 ret2) = do

974− zipWithM_ subsumes args2 args1

979+ zipWithM_ (subsumes Nothing) args2 args1

975− ret1 `subsumes` ret2

980+ subsumes Nothing ret1 ret2

981+ return val

982+subsumes' (Just val) (ConstrainedType constraints ty1) ty2 = do

983+ env <- getEnv

984+ dicts <- getTypeClassDictionaries

985+ Just moduleName <- checkCurrentModule <$> get

986+ _ <- subsumes' Nothing ty1 ty2

987+ return . Just $ App val (map (flip TypeClassDictionary dicts) (qualifyAllUnqualifiedNames moduleName env constraints))

976−subsumes' ty1 ty2 = ty1 ?= ty2

988+subsumes' val ty1 ty2 = do

989+ ty1 ?= ty2

990+ return val

977

991