@@ -428,7 +428,7 @@ infer' (Accessor prop val) = do
428428 Nothing -> do
429429 field <- fresh
430430 rest <- fresh
431− objTy `subsumes` Object (RCons prop field rest)
431+ _ <- subsumes Nothing objTy (Object (RCons prop field rest))
432432 return $ TypedValue True (Accessor prop typed) field
433433 Just ty -> return $ TypedValue True (Accessor prop typed) ty
434434infer' (Abs args ret) = do
@@ -609,7 +609,7 @@ inferBinder val (NullaryBinder ctor) = do
609609 Just moduleName <- checkCurrentModule <$> get
610610 case M.lookup (qualify moduleName ctor) (dataConstructors env) of
611611 Just (ty, _) -> do
612− ty `subsumes` val
612+ _ <- subsumes Nothing ty val
613613 return M.empty
614614 _ -> throwError $ "Constructor " ++ show ctor ++ " is not defined"
615615inferBinder val (UnaryBinder ctor binder) = do
@@ -620,7 +620,7 @@ inferBinder val (UnaryBinder ctor binder) = do
620620 fn <- replaceAllVarsWithUnknowns ty
621621 case fn of
622622 Function [obj] ret -> do
623− val `subsumes` ret
623+ _ <- subsumes Nothing val ret
624624 inferBinder obj binder
625625 _ -> throwError $ "Constructor " ++ show ctor ++ " is not a unary constructor"
626626 _ -> throwError $ "Constructor " ++ show ctor ++ " is not defined"
@@ -818,19 +818,24 @@ check' (App f args) ret = do
818818 f'@(TypedValue _ _ ft) <- infer f
819819 app <- checkFunctionApplication f' ft args ret
820820 return $ app
821−check' (Var var) ty = do
821+check' v@(Var var) ty = do
822822 Just moduleName <- checkCurrentModule <$> get
823823 ty1 <- lookupVariable moduleName var
824824 repl <- replaceAllTypeSynonyms ty1
825− repl `subsumes` ty
826− return $ Var var
825+ v' <- subsumes (Just v) repl ty
826+ case v' of
827+ Nothing -> throwError "Unable to check type subsumption"
828+ Just v'' -> return v''
827829check' (TypedValue checkType val ty1) ty2 = do
828830 Just moduleName <- checkCurrentModule <$> get
829831 kind <- liftCheck $ kindOf moduleName ty1
830832 guardWith ("Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star
831− ty1 `subsumes` ty2
832− val' <- if checkType then check val ty1 else return val
833− return $ TypedValue True val' ty1
833+ val' <- subsumes (Just val) ty1 ty2
834+ case val' of
835+ Nothing -> throwError "Unable to check type subsumption"
836+ Just val'' -> do
837+ val''' <- if checkType then check val'' ty1 else return val''
838+ return $ TypedValue True val''' ty1
834839check' (Case vals binders) ret = do
835840 vals' <- mapM infer vals
836841 let ts = map (\(TypedValue _ _ t) -> t) vals'
@@ -869,7 +874,7 @@ check' (Constructor c) ty = do
869874 Nothing -> throwError $ "Constructor " ++ show c ++ " is undefined"
870875 Just (ty1, _) -> do
871876 repl <- replaceAllTypeSynonyms ty1
872− repl `subsumes` ty
877+ _ <- subsumes Nothing repl ty
873878 return $ Constructor c
874879check' val (SaturatedTypeSynonym name args) = do
875880 ty <- expandTypeSynonym name args
@@ -928,7 +933,7 @@ checkFunctionApplication' :: Value -> Type -> [Value] -> Type -> UnifyT Check Va
928933checkFunctionApplication' fn (Function argTys retTy) args ret = do
929934 guardWith "Incorrect number of function arguments" (length args == length argTys)
930935 args' <- zipWithM check args argTys
931− retTy `subsumes` ret
936+ _ <- subsumes Nothing retTy ret
932937 return $ App fn args'
933938checkFunctionApplication' fn (ForAll ident ty) args ret = do
934939 replaced <- replaceVarWithUnknown ident ty
@@ -954,8 +959,8 @@ checkFunctionApplication' _ fnTy args ret = throwError $ "Applying a function of
954959-- |
955960-- Check whether one type subsumes another, rethrowing errors to provide a better error message
956961--
957−subsumes :: Type -> Type -> UnifyT Check ()
958−subsumes ty1 ty2 = rethrow errorMessage $ subsumes' ty1 ty2
962+subsumes :: Maybe Value -> Type -> Type -> UnifyT Check (Maybe Value)
963+subsumes val ty1 ty2 = rethrow errorMessage $ subsumes' val ty1 ty2
959964 where
960965 errorMessage msg = "Error checking that type "
961966 ++ prettyPrintType ty1
@@ -966,12 +971,21 @@ subsumes ty1 ty2 = rethrow errorMessage $ subsumes' ty1 ty2
966971-- |
967972-- Check whether one type subsumes another
968973--
969−subsumes' :: Type -> Type -> UnifyT Check ()
970−subsumes' (ForAll ident ty1) ty2 = do
974+subsumes' :: Maybe Value -> Type -> Type -> UnifyT Check (Maybe Value)
975+subsumes' val (ForAll ident ty1) ty2 = do
971976 replaced <- replaceVarWithUnknown ident ty1
972− replaced `subsumes` ty2
973−subsumes' (Function args1 ret1) (Function args2 ret2) = do
974− zipWithM_ subsumes args2 args1
975− ret1 `subsumes` ret2
976−subsumes' ty1 ty2 = ty1 ?= ty2
977+ subsumes val replaced ty2
978+subsumes' val (Function args1 ret1) (Function args2 ret2) = do
979+ zipWithM_ (subsumes Nothing) args2 args1
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))
988+subsumes' val ty1 ty2 = do
989+ ty1 ?= ty2
990+ return val
977991