git.iko.soy/elk
on 63243ca help sign in
elk/compiler/Type/Unify.hs
200 lines 8.5 kB history raw
1{-# OPTIONS_GHC -W #-}
2module Type.Unify (unify) where
4import Type.Type
5import qualified Data.UnionFind.IO as UF
6import qualified Data.Map as Map
7import qualified Data.Maybe as Maybe
8import qualified Type.State as TS
9import Control.Monad.State
10import SourceSyntax.Location
11import Type.PrettyPrint
12import Text.PrettyPrint (render)
14unify :: SrcSpan -> Variable -> Variable -> StateT TS.SolverState IO ()
15unify span variable1 variable2 = do
16 equivalent <- liftIO $ UF.equivalent variable1 variable2
17 if equivalent then return ()
18 else actuallyUnify span variable1 variable2
20actuallyUnify :: SrcSpan -> Variable -> Variable -> StateT TS.SolverState IO ()
21actuallyUnify span variable1 variable2 = do
22 desc1 <- liftIO $ UF.descriptor variable1
23 desc2 <- liftIO $ UF.descriptor variable2
24 let unify' = unify span
26 name' :: Maybe String
27 name' = case (name desc1, name desc2) of
28 (Just name1, Just name2) ->
29 case (flex desc1, flex desc2) of
30 (_, Flexible) -> Just name1
31 (Flexible, _) -> Just name2
32 (Is Number, Is _) -> Just name1
33 (Is _, Is Number) -> Just name2
34 (Is _, Is _) -> Just name1
35 (_, _) -> Nothing
36 (Just name1, _) -> Just name1
37 (_, Just name2) -> Just name2
38 _ -> Nothing
40 flex' :: Flex
41 flex' = case (flex desc1, flex desc2) of
42 (f, Flexible) -> f
43 (Flexible, f) -> f
44 (Is Number, Is _) -> Is Number
45 (Is _, Is Number) -> Is Number
46 (Is super, Is _) -> Is super
47 (_, _) -> Flexible
49 rank' :: Int
50 rank' = min (rank desc1) (rank desc2)
52 merge1 :: StateT TS.SolverState IO ()
53 merge1 = liftIO $ do
54 if rank desc1 < rank desc2 then UF.union variable2 variable1
55 else UF.union variable1 variable2
56 UF.modifyDescriptor variable1 $ \desc ->
57 desc { structure = structure desc1, flex = flex', name = name' }
59 merge2 :: StateT TS.SolverState IO ()
60 merge2 = liftIO $ do
61 if rank desc1 < rank desc2 then UF.union variable2 variable1
62 else UF.union variable1 variable2
63 UF.modifyDescriptor variable2 $ \desc ->
64 desc { structure = structure desc2, flex = flex', name = name' }
66 merge = if rank desc1 < rank desc2 then merge1 else merge2
68 fresh :: Maybe (Term1 Variable) -> StateT TS.SolverState IO Variable
69 fresh structure = do
70 var <- liftIO . UF.fresh $ Descriptor {
71 structure = structure, rank = rank', flex = flex',
72 name = name', copy = Nothing, mark = noMark
73 }
74 TS.register var
76 flexAndUnify var = do
77 liftIO $ UF.modifyDescriptor var $ \desc -> desc { flex = Flexible }
78 unify' variable1 variable2
80 unifyNumber svar name
81 | name `elem` ["Int","Float","number"] = flexAndUnify svar
82 | otherwise = TS.addError span (Just hint) variable1 variable2
83 where hint = "A number must be an Int or Float."
85 comparableError maybe =
86 TS.addError span (Just $ Maybe.fromMaybe msg maybe) variable1 variable2
87 where msg = "A comparable must be an Int, Float, Char, String, list, or tuple."
89 unifyComparable var name
90 | name `elem` ["Int","Float","Char","String","comparable"] = flexAndUnify var
91 | otherwise = comparableError Nothing
93 unifyComparableStructure varSuper varFlex =
94 do struct <- liftIO $ collectApps varFlex
95 case struct of
96 Other -> comparableError Nothing
97 List v -> do flexAndUnify varSuper
98 unify' v =<< liftIO (var $ Is Comparable)
99 Tuple vs
100 | length vs > 6 ->
101 comparableError $ Just "Cannot compare a tuple with more than 6 elements."
102 | otherwise ->
103 do flexAndUnify varSuper
104 cmpVars <- liftIO $ forM [1..length vs] $ \_ -> var (Is Comparable)
105 zipWithM_ unify' vs cmpVars
107 unifyAppendable varSuper varFlex =
108 do struct <- liftIO $ collectApps varFlex
109 case struct of
110 List _ -> flexAndUnify varSuper
111 _ -> comparableError Nothing
113 rigidError variable = TS.addError span (Just hint) variable1 variable2
114 where
115 var = "'" ++ render (pretty Never variable) ++ "'"
116 hint = "Cannot unify rigid type variable " ++ var ++
117 ".\nThe problem probably relates to a type annotation. Note that rigid type\n\
118 \variables are not shared between a top-level and let-bound type annotations."
120 superUnify =
121 case (flex desc1, flex desc2, name desc1, name desc2) of
122 (Is super1, Is super2, _, _)
123 | super1 == super2 -> merge
124 (Is Number, Is Comparable, _, _) -> merge1
125 (Is Comparable, Is Number, _, _) -> merge2
127 (Is Number, _, _, Just name) -> unifyNumber variable1 name
128 (_, Is Number, Just name, _) -> unifyNumber variable2 name
130 (Is Comparable, _, _, Just name) -> unifyComparable variable1 name
131 (_, Is Comparable, Just name, _) -> unifyComparable variable2 name
132 (Is Comparable, _, _, _) -> unifyComparableStructure variable1 variable2
133 (_, Is Comparable, _, _) -> unifyComparableStructure variable2 variable1
135 (Is Appendable, _, _, Just ctor)
136 | ctor `elem` ["Text.Text","String"] -> flexAndUnify variable1
137 (_, Is Appendable, Just ctor, _)
138 | ctor `elem` ["Text.Text","String"] -> flexAndUnify variable2
139 (Is Appendable, _, _, _) -> unifyAppendable variable1 variable2
140 (_, Is Appendable, _, _) -> unifyAppendable variable2 variable1
142 (Rigid, _, _, _) -> rigidError variable1
143 (_, Rigid, _, _) -> rigidError variable2
144 _ -> TS.addError span Nothing variable1 variable2
146 case (structure desc1, structure desc2) of
147 (Nothing, Nothing) | flex desc1 == Flexible && flex desc1 == Flexible -> merge
148 (Nothing, _) | flex desc1 == Flexible -> merge2
149 (_, Nothing) | flex desc2 == Flexible -> merge1
151 (Just (Var1 v), _) -> unify' v variable2
152 (_, Just (Var1 v)) -> unify' v variable1
154 (Nothing, _) -> superUnify
155 (_, Nothing) -> superUnify
157 (Just type1, Just type2) ->
158 case (type1,type2) of
159 (App1 term1 term2, App1 term1' term2') ->
160 do merge
161 unify' term1 term1'
162 unify' term2 term2'
163 (Fun1 term1 term2, Fun1 term1' term2') ->
164 do merge
165 unify' term1 term1'
166 unify' term2 term2'
168 (EmptyRecord1, EmptyRecord1) ->
169 return ()
171 (Record1 fields ext, EmptyRecord1) | Map.null fields -> unify' ext variable2
172 (EmptyRecord1, Record1 fields ext) | Map.null fields -> unify' ext variable1
174 (Record1 fields1 ext1, Record1 fields2 ext2) ->
175 do sequence . concat . Map.elems $ Map.intersectionWith (zipWith unify') fields1 fields2
176 let mkRecord fs ext = fresh . Just $ Record1 fs ext
177 case (Map.null fields1', Map.null fields2') of
178 (True , True ) -> unify' ext1 ext2
179 (True , False) -> do
180 record2' <- mkRecord fields2' ext2
181 unify' ext1 record2'
182 (False, True ) -> do
183 record1' <- mkRecord fields1' ext1
184 unify' record1' ext2
185 (False, False) -> do
186 record1' <- mkRecord fields1' =<< fresh Nothing
187 record2' <- mkRecord fields2' =<< fresh Nothing
188 unify' record1' ext2
189 unify' ext1 record2'
190 where
191 fields1' = unmerged fields1 fields2
192 fields2' = unmerged fields2 fields1
194 unmerged a b = Map.filter (not . null) $ Map.union (Map.intersectionWith eat a b) a
196 eat (_:xs) (_:ys) = eat xs ys
197 eat xs _ = xs
199 _ -> TS.addError span Nothing variable1 variable2