git.iko.soy/elk
on master help sign in
Add context to type constraints for better error messages. Fix big with generated constraints in which some constraints could be ignored.
45f834eevancz
elm/src/Types/Constrain.hs+34−20
compare with master
unifiedsplit
@@ -6,7 +6,7 @@ import Types
6import Data.List (foldl')
6import Data.List (foldl')
7import qualified Data.Set as Set
7import qualified Data.Set as Set
8import qualified Data.Map as Map
8import qualified Data.Map as Map
9−import Control.Monad (liftM,mapM)
9+import Control.Monad (liftM,mapM,zipWithM)
10import Control.Monad.State (evalState)
10import Control.Monad.State (evalState)
11import Guid
11import Guid
12
12
@@ -14,53 +14,64 @@ beta = VarT `liftM` guid
14unionA = Map.unionWith (++)
14unionA = Map.unionWith (++)
15unionsA = Map.unionsWith (++)
15unionsA = Map.unionsWith (++)
16
16
17+data Context a b = Context a b deriving (Eq,Show)
18+ctx e = Context e
19+
20+instance (Ord a, Eq c) => Ord (Context c a) where
21+ compare (Context _ x) (Context _ y) = compare x y
22+
17constrain hints expr = do
23constrain hints expr = do
18 (as,cs,t) <- inference expr
24 (as,cs,t) <- inference expr
19− let cMap = Map.intersectionWith (\s -> map (\v -> VarT v:<<: s)) (Map.fromList hints) as
25+ let cMap = Map.intersectionWithKey combine (Map.fromList hints) as
26+ where combine k s vs = map (\v -> ctx (Var k) $ VarT v :<<: s) vs
20− return $ Set.toList cs ++ (concat . map snd $ Map.toList cMap)
27+ return (Set.toList cs ++ (concatMap snd $ Map.toList cMap))
21
28
22−inference :: Expr -> GuidCounter (Map.Map String [X], Set.Set Constraint, Type)
29+inference :: Expr -> GuidCounter (Map.Map String [X], Set.Set (Context Expr Constraint), Type)
23inference (Var x) =
30inference (Var x) =
24 do b <- guid
31 do b <- guid
25 return (Map.singleton x [b], Set.empty, VarT b)
32 return (Map.singleton x [b], Set.empty, VarT b)
26−inference (App e1 e2) =
33+inference e@(App e1 e2) =
27 do (a1,c1,t1) <- inference e1
34 do (a1,c1,t1) <- inference e1
28 (a2,c2,t2) <- inference e2
35 (a2,c2,t2) <- inference e2
29 b <- beta
36 b <- beta
30 return ( unionA a1 a2
37 return ( unionA a1 a2
31− , Set.unions [c1,c2,Set.singleton $ t1 :=: (LambdaT t2 b)]
38+ , Set.unions [c1,c2,Set.singleton . ctx e $ t1 :=: (LambdaT t2 b)]
32 , b )
39 , b )
33inference (Lambda x e) =
40inference (Lambda x e) =
34 do (a,c,t) <- inference e
41 do (a,c,t) <- inference e
35 b <- beta
42 b <- beta
43+ v <- guid
36 return ( Map.delete x a
44 return ( Map.delete x a
37− , Set.union c . Set.fromList . map (\x -> VarT x :=: b) $
45+ , Set.union c . Set.fromList . map (\x -> ctx e $ VarT x :=: b) $
38− Map.findWithDefault [] x a
46+ Map.findWithDefault [v] x a
39 , LambdaT b t )
47 , LambdaT b t )
40inference (Let defs e) =
48inference (Let defs e) =
41 do (as,cs,t) <- inference e
49 do (as,cs,t) <- inference e
42 (ass, schemes) <- liftM unzip (mapM defScheme defs)
50 (ass, schemes) <- liftM unzip (mapM defScheme defs)
43 let assumptions = unionsA (as:ass)
51 let assumptions = unionsA (as:ass)
44 let names = map (\(Definition x _ _) -> x) defs
52 let names = map (\(Definition x _ _) -> x) defs
53+ let genCs name s = do
54+ v <- guid
45− let genCs name s = map (\x -> VarT x :<<: s) $ Map.findWithDefault [] name assumptions
55+ return . map (\x -> ctx (Var name) $ VarT x :<<: s) $ Map.findWithDefault [v] name assumptions
46− let cs' = Set.fromList . concat $ zipWith genCs names schemes
56+ cs' <- zipWithM genCs names schemes
47 return ( foldr Map.delete assumptions names
57 return ( foldr Map.delete assumptions names
48− , Set.union cs' cs
58+ , Set.union (Set.fromList . concat $ cs') cs
49 , t )
59 , t )
50
60
51−inference (Case e cases) =
61+inference ce@(Case e cases) =
52 do (as,cs,t) <- inference e
62 do (as,cs,t) <- inference e
53 (ass,css,ts) <- liftM unzip3 $ mapM (caseInference t) cases
63 (ass,css,ts) <- liftM unzip3 $ mapM (caseInference t) cases
54 return ( unionsA $ as:ass
64 return ( unionsA $ as:ass
65+ , let combine t1 t2 = ctx ce (t1 :=: t2) in
55− , Set.unions $ Set.fromList (zipWith (:=:) ts $ tail ts) : cs : css
66+ Set.unions $ Set.fromList (zipWith combine ts $ tail ts) : cs : css
56 , head ts)
67 , head ts)
57
68
58−inference (If e1 e2 e3) =
69+inference e@(If e1 e2 e3) =
59 do (a1,c1,t1) <- inference e1
70 do (a1,c1,t1) <- inference e1
60 (a2,c2,t2) <- inference e2
71 (a2,c2,t2) <- inference e2
61 (a3,c3,t3) <- inference e3
72 (a3,c3,t3) <- inference e3
62 return ( unionsA [a1,a2,a3]
73 return ( unionsA [a1,a2,a3]
63− , Set.unions [c1,c2,c3, Set.fromList [ t1 :=: bool, t2 :=: t3 ] ]
74+ , Set.unions [c1,c2,c3, Set.fromList [ ctx e1 (t1 :=: bool), ctx e (t2 :=: t3) ] ]
64 , t2 )
75 , t2 )
65
76
66inference (Data name es) = inference $ foldl' App (Var name) es
77inference (Data name es) = inference $ foldl' App (Var name) es
@@ -71,7 +82,7 @@ inference (Range e1 e2) = inference (Var "elmRange" `App` e1 `App` e2)
71inference other =
82inference other =
72 case other of
83 case other of
73 IntNum _ -> do t <- beta
84 IntNum _ -> do t <- beta
74− return (Map.empty, Set.singleton (t :<: number), t)
85+ return (Map.empty, Set.singleton (ctx other $ t :<: number), t)
75 FloatNum _ -> primitive float
86 FloatNum _ -> primitive float
76 Chr _ -> primitive char
87 Chr _ -> primitive char
77 Str _ -> primitive string
88 Str _ -> primitive string
@@ -93,8 +104,11 @@ namesIn (PData name ps) = concatMap namesIn ps
93defScheme (Definition name args e) =
104defScheme (Definition name args e) =
94 do argDict <- mapM (\a -> liftM ((,) a) guid) args
105 do argDict <- mapM (\a -> liftM ((,) a) guid) args
95 (as,cs,t) <- inference e
106 (as,cs,t) <- inference e
107+ let genCs (arg,x) = do
108+ v <- guid
96− let genCs (arg,x) = map (\y -> VarT x :=: VarT y) $ Map.findWithDefault [] arg as
109+ return . map (\y -> VarT x :=: VarT y) $ Map.findWithDefault [v] arg as
97− let cs' = concatMap genCs argDict
110+ cs' <- concat `liftM` mapM genCs argDict
111+ let cs'' = map (\(Context _ c) -> c) (Set.toList cs)
98 let tipe = foldr (==>) t $ map (VarT . snd) argDict
112 let tipe = foldr (==>) t $ map (VarT . snd) argDict
99− return (foldr Map.delete as args
113+ return ( foldr Map.delete as args
100− , Forall (map snd argDict) (cs' ++ Set.toList cs) tipe)
114+ , Forall (map snd argDict) (cs' ++ cs'') tipe)
elm/src/Types/Unify.hs+37−27
@@ -1,5 +1,5 @@
1
1
2−module Unify where
2+module Unify (unify) where
3
3
4import Constrain
4import Constrain
5import Control.Arrow (second)
5import Control.Arrow (second)
@@ -15,68 +15,78 @@ unify hints expr = run $ do
15 cs <- constrain hints expr
15 cs <- constrain hints expr
16 solver cs []
16 solver cs []
17
17
18+eq ctx t1 t2 = Context ctx (t1 :=: t2)
19+
18solver [] subs = return $ Right subs
20solver [] subs = return $ Right subs
19
21
20-------- Destruct Type-constructors --------
22-------- Destruct Type-constructors --------
21
23
22−solver ((t1@(ADT n1 ts1) :=: t2@(ADT n2 ts2)) : cs) subs =
24+solver ((Context ctx (t1@(ADT n1 ts1) :=: t2@(ADT n2 ts2))) : cs) subs =
23− if n1 /= n2 then uniError t1 t2 else
25+ if n1 /= n2 then uniError ctx t1 t2 else
24− solver (zipWith (:=:) ts1 ts2 ++ cs) subs
26+ solver (zipWith (eq ctx) ts1 ts2 ++ cs) subs
25−solver ((LambdaT t1 t2 :=: LambdaT t1' t2') : cs) subs =
27+solver ((Context ctx (LambdaT t1 t2 :=: LambdaT t1' t2')) : cs) subs =
26− solver ([ t1 :=: t1', t2 :=: t2' ] ++ cs) subs
28+ solver ([ eq ctx t1 t1', eq ctx t2 t2' ] ++ cs) subs
27
29
28-------- Type-equality --------
30-------- Type-equality --------
29
31
30−solver ((VarT x :=: t) : cs) subs =
32+solver ((Context ctx (VarT x :=: t)) : cs) subs =
31 solver (map (cSub x t) cs) . map (second $ tSub x t) $ (x,t):subs
33 solver (map (cSub x t) cs) . map (second $ tSub x t) $ (x,t):subs
32−solver ((t :=: VarT x) : cs) subs = solver ((VarT x :=: t) : cs) subs
34+solver ((Context ctx (t :=: VarT x)) : cs) subs = solver ((Context ctx (VarT x :=: t)) : cs) subs
33−solver ((t1 :=: t2) : cs) subs
35+solver ((Context ctx (t1 :=: t2)) : cs) subs
34 | t1 == t2 = solver cs subs
36 | t1 == t2 = solver cs subs
35− | otherwise = uniError t1 t2
37+ | otherwise = uniError ctx t1 t2
36
38
37-------- subtypes --------
39-------- subtypes --------
38
40
39−solver (c@(VarT x :<: SuperType n ts) : cs) subs
41+solver (c@(Context ctx (VarT x :<: SuperType n ts)) : cs) subs
40− | all isSuper cs = solver ((VarT x :=: ADT n []) : cs) subs
42+ | all isSuper cs = solver ((Context ctx (VarT x :=: ADT n [])) : cs) subs
41 | otherwise = solver (cs ++ [c]) subs
43 | otherwise = solver (cs ++ [c]) subs
42− where isSuper (VarT _ :<: _) = True
44+ where isSuper (Context _ (VarT _ :<: _)) = True
43 isSuper _ = False
45 isSuper _ = False
44−solver ((t@(ADT n1 []) :<: st@(SuperType n2 ts)) : cs) subs
46+solver ((Context ctx (t@(ADT n1 []) :<: st@(SuperType n2 ts))) : cs) subs
45 | n1 == n2 || Set.member t ts = solver cs subs
47 | n1 == n2 || Set.member t ts = solver cs subs
46 | otherwise = return . Left $ "Type error: " ++ show t ++
48 | otherwise = return . Left $ "Type error: " ++ show t ++
47− " is not a " ++ show st
49+ " is not a " ++ show st ++
50+ " in context " ++ show ctx
48−solver ((t@(ADT "List" [_]) :<: st@(SuperType n' ts')) : cs) subs
51+solver ((Context ctx (t@(ADT "List" [_]) :<: st@(SuperType n' ts'))) : cs) subs
49− | any f (Set.toList ts') = solver cs subs
52+ | any f (Set.toList ts') || Set.member t ts' = solver cs subs
50 | otherwise = return . Left $ "Type error: " ++ show t ++
53 | otherwise = return . Left $ "Type error: " ++ show t ++
51− " is not a " ++ show st
54+ " is not a " ++ show st ++
55+ " in context " ++ show ctx
52 where f (ADT "List" [VarT _]) = True
56 where f (ADT "List" [VarT _]) = True
53 f _ = False
57 f _ = False
54
58
55−solver ((t :<: st@(SuperType n ts)) : cs) subs
59+solver ((Context ctx (t :<: st@(SuperType n ts))) : cs) subs
56 | Set.member t ts = solver cs subs
60 | Set.member t ts = solver cs subs
57 | otherwise = return . Left $ "Type error: " ++ show t ++
61 | otherwise = return . Left $ "Type error: " ++ show t ++
58 " is not a " ++ show st
62 " is not a " ++ show st
59
63
60−solver ((t1 :<<: Forall xs cs' t2) : cs) subs = do
64+solver ((Context ctx (t1 :<<: Forall xs cs' t2)) : cs) subs = do
61 pairs <- mapM (\x -> liftM ((,) x . VarT) guid) xs
65 pairs <- mapM (\x -> liftM ((,) x . VarT) guid) xs
62 let t2' = foldr (uncurry tSub) t2 pairs
66 let t2' = foldr (uncurry tSub) t2 pairs
63− let cs'' = foldr (\(k,v) -> map (cSub k v)) cs' pairs
67+ let cs'' = foldr (\(k,v) -> map (cSub k v)) (map (Context ctx) cs') pairs
64− solver ((t1 :=: t2') : cs'' ++ cs) subs
68+ let constrs = ((Context ctx (t1 :=: t2')) : cs'' ++ cs)
69+ solver constrs subs
65
70
66
71
67−cSub k v (t1 :=: t2) = force $ tSub k v t1 :=: tSub k v t2
72+cSub k v (Context c (t1 :=: t2) ) = force . Context c $ tSub k v t1 :=: tSub k v t2
68−cSub k v (t :<: super) = force $ tSub k v t :<: super
73+cSub k v (Context c (t :<: super)) = force . Context c $ tSub k v t :<: super
69−cSub k v (t :<<: poly) = force $ tSub k v t :<<: poly
74+cSub k v (Context c (t :<<: poly)) = force . Context c $ tSub k v t :<<: poly
70
75
71tSub k v t@(VarT x) = if k == x then v else t
76tSub k v t@(VarT x) = if k == x then v else t
72tSub k v (LambdaT t1 t2) = force $ LambdaT (tSub k v t1) (tSub k v t2)
77tSub k v (LambdaT t1 t2) = force $ LambdaT (tSub k v t1) (tSub k v t2)
73tSub k v (ADT name ts) = ADT name (map (force . tSub k v) ts)
78tSub k v (ADT name ts) = ADT name (map (force . tSub k v) ts)
74
79
75−uniError t1 t2 =
80+uniError ctx t1 t2 =
76− return . Left $ "Type error: " ++ show t1 ++ " is not equal to " ++ show t2
81+ return . Left $ "Type error: " ++ show t1 ++
82+ " is not equal to " ++ show t2 ++
83+ " in context " ++ show ctx
77
84
78force x = x `deepseq` x
85force x = x `deepseq` x
79
86
87+instance (NFData a) => NFData (Context c a) where
88+ rnf (Context _ a) = a `deepseq` ()
89+
80instance NFData Constraint where
90instance NFData Constraint where
81 rnf (t1 :=: t2) = t1 `deepseq` t2 `deepseq` ()
91 rnf (t1 :=: t2) = t1 `deepseq` t2 `deepseq` ()
82 rnf (t :<: _) = t `deepseq` ()
92 rnf (t :<: _) = t `deepseq` ()