@@ -53,14 +53,47 @@ typeOf :: Ident -> Value -> Check PolyType
5353typeOf name val = do
5454 me <- fresh
5555 (cs, n) <- typeConstraints (M.singleton name me) val
56− solution <- solveTypeConstraints ((TypeConstraint me (TUnknown n)) : cs) emptyTypeSolution
57− return $ varIfUnknown $ fst (runTypeSolution solution) n
56+ let allConstraints = TypeConstraint me (TUnknown n) : cs
57+ solution <- solveTypeConstraints allConstraints emptyTypeSolution
58+ let ty = fst (runTypeSolution solution) n
59+ allUnknownsBecameQuantified allConstraints solution ty
60+ return $ varIfUnknown ty
61+
62+allUnknownsBecameQuantified :: [TypeConstraint] -> TypeSolution -> Type -> Check ()
63+allUnknownsBecameQuantified cs solution ty = do
64+ let
65+ typesMentioned = findUnknownTypes ty
66+ unknownTypes = nub $ flip concatMap cs $ \c -> case c of
67+ TypeConstraint u t -> u : findUnknownTypes t
68+ RowConstraint _ r -> findUnknownTypes r
69+ unsolvedTypes = filter (\n -> TUnknown n == fst (runTypeSolution solution) n) unknownTypes
70+ guardWith "Unsolved type variable" $ null $ unsolvedTypes \\ typesMentioned
71+ let
72+ rowsMentioned = findUnknownRows ty
73+ unknownRows = nub $ flip concatMap cs $ \c -> case c of
74+ TypeConstraint _ t -> findUnknownRows t
75+ RowConstraint u r -> u : findUnknownRows r
76+ unsolvedRows = filter (\n -> RUnknown n == snd (runTypeSolution solution) n) unknownRows
77+ guardWith ("Unsolved row variable" ++ show (unsolvedRows \\ rowsMentioned) ++ ", " ++ show cs) $ null $ unsolvedRows \\ rowsMentioned
78+
79+findUnknownTypes :: (Data d) => d -> [Int]
80+findUnknownTypes = everything (++) (mkQ [] f)
81+ where
82+ f :: Type -> [Int]
83+ f (TUnknown n) = [n]
84+ f _ = []
85+
86+findUnknownRows :: (Data d) => d -> [Int]
87+findUnknownRows = everything (++) (mkQ [] f)
88+ where
89+ f :: Row -> [Int]
90+ f (RUnknown n) = [n]
91+ f _ = []
5892
5993varIfUnknown :: Type -> PolyType
6094varIfUnknown ty =
6195 let
6296 (ty', m) = flip runState M.empty $ everywhereM (flip extM g $ mkM f) ty
63− -- TODO : check no nested unknowns
6497 in
6598 PolyType (sort $ nub $ M.elems m) ty'
6699 where
@@ -478,7 +511,7 @@ unifyRows r1 r2 =
478511 unifyRows' ((name, ty):row) r others (RUnknown u) = do
479512 u' <- fresh
480513 cs <- unifyRows' row r others (RUnknown u')
481− return [ RowConstraint u (RCons name ty (RUnknown u')) ]
514+ return (RowConstraint u (RCons name ty (RUnknown u')) : cs)
482515 unifyRows' [] REmpty [] REmpty = return []
483516 unifyRows' sd1 r1 sd2 r2 = throwError $ "Cannot unify " ++ show (fromList (sd1, r1)) ++ " with " ++ show (fromList (sd2, r2)) ++ "."
484517 toList :: Row -> ([(String, Type)], Row)