git.iko.soy/elk
on 0bdfd73 help sign in
elk/src/Type/Unify.hs
712 lines 18 kB history raw
1{-# OPTIONS_GHC -Wall #-}
2{-# LANGUAGE OverloadedStrings, Rank2Types #-}
3module Type.Unify
4 ( Answer(..)
5 , unify
6 )
7 where
10import qualified Data.Map.Strict as Map
12import qualified AST.Module.Name as ModuleName
13import qualified Elm.Name as N
14import qualified Type.Error as Error
15import qualified Type.Occurs as Occurs
16import Type.Type as Type
17import qualified Type.UnionFind as UF
21-- UNIFY
24data Answer
25 = Ok [Variable]
26 | Err [Variable] Error.Type Error.Type
29unify :: Variable -> Variable -> IO Answer
30unify v1 v2 =
31 case guardedUnify v1 v2 of
32 Unify k ->
33 k [] onSuccess $ \vars () ->
34 do t1 <- Type.toErrorType v1
35 t2 <- Type.toErrorType v2
36 UF.union v1 v2 errorDescriptor
37 return (Err vars t1 t2)
40onSuccess :: [Variable] -> () -> IO Answer
41onSuccess vars () =
42 return (Ok vars)
45{-# NOINLINE errorDescriptor #-}
46errorDescriptor :: Descriptor
47errorDescriptor =
48 Descriptor Error noRank noMark Nothing
52-- CPS UNIFIER
55newtype Unify a =
56 Unify (forall r.
57 [Variable]
58 -> ([Variable] -> a -> IO r)
59 -> ([Variable] -> () -> IO r)
60 -> IO r
61 )
64instance Functor Unify where
65 fmap func (Unify kv) =
66 Unify $ \vars ok err ->
67 let
68 ok1 vars1 value =
69 ok vars1 (func value)
70 in
71 kv vars ok1 err
74instance Applicative Unify where
75 pure a =
76 Unify $ \vars ok _ ->
77 ok vars a
79 (<*>) (Unify kf) (Unify kv) =
80 Unify $ \vars ok err ->
81 let
82 ok1 vars1 func =
83 let
84 ok2 vars2 value =
85 ok vars2 (func value)
86 in
87 kv vars1 ok2 err
88 in
89 kf vars ok1 err
92instance Monad Unify where
93 return a =
94 Unify $ \vars ok _ ->
95 ok vars a
97 (>>=) (Unify ka) callback =
98 Unify $ \vars ok err ->
99 let
100 ok1 vars1 a =
101 case callback a of
102 Unify kb -> kb vars1 ok err
103 in
104 ka vars ok1 err
107register :: IO Variable -> Unify Variable
108register mkVar =
109 Unify $ \vars ok _ ->
110 do var <- mkVar
111 ok (var:vars) var
114mismatch :: Unify a
115mismatch =
116 Unify $ \vars _ err ->
117 err vars ()
120try2 :: Unify () -> Unify () -> Unify ()
121try2 (Unify k1) (Unify k2) =
122 Unify $ \vars ok err ->
123 let
124 ok1 vars1 () = k2 vars1 ok err
125 err1 vars1 () = k2 vars1 err err
126 in
127 k1 vars ok1 err1
130{-# INLINE try3 #-}
131try3 :: Unify () -> Unify () -> Unify () -> Unify ()
132try3 u1 u2 u3 =
133 try2 u1 (try2 u2 u3)
137-- UNIFICATION HELPERS
140data Context =
141 Context
142 { _first :: Variable
143 , _firstDesc :: Descriptor
144 , _second :: Variable
145 , _secondDesc :: Descriptor
146 }
149reorient :: Context -> Context
150reorient (Context var1 desc1 var2 desc2) =
151 Context var2 desc2 var1 desc1
155-- MERGE
158merge :: Context -> Content -> Unify ()
159merge (Context var1 (Descriptor _ rank1 _ _) var2 (Descriptor _ rank2 _ _)) content =
160 Unify $ \vars ok _ ->
161 ok vars =<<
162 UF.union var1 var2 (Descriptor content (min rank1 rank2) noMark Nothing)
165fresh :: Context -> Content -> Unify Variable
166fresh (Context _ (Descriptor _ rank1 _ _) _ (Descriptor _ rank2 _ _)) content =
167 register $ UF.fresh $
168 Descriptor content (min rank1 rank2) noMark Nothing
172-- ACTUALLY UNIFY THINGS
175guardedUnify :: Variable -> Variable -> Unify ()
176guardedUnify left right =
177 Unify $ \vars ok err ->
178 do equivalent <- UF.equivalent left right
179 if equivalent
180 then ok vars ()
181 else
182 do leftDesc <- UF.get left
183 rightDesc <- UF.get right
184 case actuallyUnify (Context left leftDesc right rightDesc) of
185 Unify k ->
186 k vars ok err
189subUnify :: Variable -> Variable -> Unify ()
190subUnify var1 var2 =
191 guardedUnify var1 var2
194actuallyUnify :: Context -> Unify ()
195actuallyUnify context@(Context _ (Descriptor firstContent _ _ _) _ (Descriptor secondContent _ _ _)) =
196 case firstContent of
197 FlexVar _ ->
198 unifyFlex context firstContent secondContent
200 FlexSuper super _ ->
201 unifyFlexSuper context super firstContent secondContent
203 RigidVar _ ->
204 unifyRigid context Nothing firstContent secondContent
206 RigidSuper super _ ->
207 unifyRigid context (Just super) firstContent secondContent
209 Alias home name args realVar ->
210 unifyAlias context home name args realVar secondContent
212 Structure flatType ->
213 unifyStructure context flatType firstContent secondContent
215 Error ->
216 -- If there was an error, just pretend it is okay. This lets us avoid
217 -- "cascading" errors where one problem manifests as multiple message.
218 return ()
222-- UNIFY FLEXIBLE VARIABLES
225unifyFlex :: Context -> Content -> Content -> Unify ()
226unifyFlex context content otherContent =
227 case otherContent of
228 Error ->
229 return ()
231 -- TODO see if wildcarding makes a noticable perf difference
233 FlexVar maybeName ->
234 merge context $
235 case maybeName of
236 Nothing ->
237 content
239 Just _ ->
240 otherContent
242 FlexSuper _ _ ->
243 merge context otherContent
245 RigidVar _ ->
246 merge context otherContent
248 RigidSuper _ _ ->
249 merge context otherContent
251 Alias _ _ _ _ ->
252 merge context otherContent
254 Structure _ ->
255 merge context otherContent
259-- UNIFY RIGID VARIABLES
262unifyRigid :: Context -> Maybe SuperType -> Content -> Content -> Unify ()
263unifyRigid context maybeSuper content otherContent =
264 case otherContent of
265 FlexVar _ ->
266 merge context content
268 FlexSuper otherSuper _ ->
269 case maybeSuper of
270 Just super ->
271 if combineRigidSupers super otherSuper then
272 merge context content
273 else
274 mismatch
276 Nothing ->
277 mismatch
279 RigidVar _ ->
280 mismatch
282 RigidSuper _ _ ->
283 mismatch
285 Alias _ _ _ _ ->
286 mismatch
288 Structure _ ->
289 mismatch
291 Error ->
292 return ()
296-- UNIFY SUPER VARIABLES
299unifyFlexSuper :: Context -> SuperType -> Content -> Content -> Unify ()
300unifyFlexSuper context super content otherContent =
301 case otherContent of
302 Structure flatType ->
303 unifyFlexSuperStructure context super flatType
305 RigidVar _ ->
306 mismatch
308 RigidSuper otherSuper _ ->
309 if combineRigidSupers otherSuper super then
310 merge context otherContent
311 else
312 mismatch
314 FlexVar _ ->
315 merge context content
317 FlexSuper otherSuper _ ->
318 case super of
319 Number ->
320 case otherSuper of
321 Number -> merge context content
322 Comparable -> merge context content
323 _ -> mismatch
325 Comparable ->
326 case otherSuper of
327 Comparable -> merge context otherContent
328 Number -> merge context otherContent
329 Appendable -> merge context (Type.unnamedFlexSuper CompAppend)
330 CompAppend -> merge context otherContent
332 Appendable ->
333 case otherSuper of
334 Appendable -> merge context otherContent
335 Comparable -> merge context (Type.unnamedFlexSuper CompAppend)
336 CompAppend -> merge context otherContent
337 Number -> mismatch
339 CompAppend ->
340 case otherSuper of
341 Comparable -> merge context content
342 Appendable -> merge context content
343 CompAppend -> merge context content
344 Number -> mismatch
346 Alias _ _ _ realVar ->
347 subUnify (_first context) realVar
349 Error ->
350 return ()
353combineRigidSupers :: SuperType -> SuperType -> Bool
354combineRigidSupers rigid flex =
355 rigid == flex
356 || (rigid == Number && flex == Comparable)
357 || (rigid == CompAppend && (flex == Comparable || flex == Appendable))
360atomMatchesSuper :: SuperType -> ModuleName.Canonical -> N.Name -> Bool
361atomMatchesSuper super home name =
362 home == ModuleName.basics
363 &&
364 case super of
365 Number ->
366 name == N.int
367 || name == N.float
369 Comparable ->
370 name == N.int
371 || name == N.float
372 || name == N.string
373 || name == N.char
375 Appendable ->
376 name == N.string
378 CompAppend ->
379 name == N.string
382unifyFlexSuperStructure :: Context -> SuperType -> FlatType -> Unify ()
383unifyFlexSuperStructure context super flatType =
384 case flatType of
385 App1 home name [] ->
386 if atomMatchesSuper super home name then
387 merge context (Structure flatType)
388 else
389 mismatch
391 App1 home name [variable] | home == ModuleName.list && name == N.list ->
392 case super of
393 Number ->
394 mismatch
396 Appendable ->
397 merge context (Structure flatType)
399 Comparable ->
400 do comparableOccursCheck context
401 merge context (Structure flatType)
402 unifyComparableRecursive variable
404 CompAppend ->
405 do comparableOccursCheck context
406 merge context (Structure flatType)
407 unifyComparableRecursive variable
409 Tuple1 a b maybeC ->
410 case super of
411 Number ->
412 mismatch
414 Appendable ->
415 mismatch
417 Comparable ->
418 do comparableOccursCheck context
419 merge context (Structure flatType)
420 unifyComparableRecursive a
421 unifyComparableRecursive b
422 case maybeC of
423 Nothing ->
424 return ()
426 Just c ->
427 unifyComparableRecursive c
429 CompAppend ->
430 mismatch
432 _ ->
433 mismatch
436-- TODO: is there some way to avoid doing this?
437-- Do type classes require occurs checks?
438comparableOccursCheck :: Context -> Unify ()
439comparableOccursCheck (Context _ _ var _) =
440 Unify $ \vars ok err ->
441 do hasOccurred <- Occurs.occurs var
442 if hasOccurred
443 then err vars ()
444 else ok vars ()
447unifyComparableRecursive :: Variable -> Unify ()
448unifyComparableRecursive var =
449 do compVar <- register $
450 do (Descriptor _ rank _ _) <- UF.get var
451 UF.fresh $ Descriptor (Type.unnamedFlexSuper Comparable) rank noMark Nothing
452 guardedUnify compVar var
456-- UNIFY ALIASES
459unifyAlias :: Context -> ModuleName.Canonical -> N.Name -> [(N.Name, Variable)] -> Variable -> Content -> Unify ()
460unifyAlias context home name args realVar otherContent =
461 case otherContent of
462 FlexVar _ ->
463 merge context (Alias home name args realVar)
465 FlexSuper _ _ ->
466 subUnify realVar (_second context)
468 RigidVar _ ->
469 subUnify realVar (_second context)
471 RigidSuper _ _ ->
472 subUnify realVar (_second context)
474 Alias otherHome otherName otherArgs otherRealVar ->
475 if name == otherName && home == otherHome then
476 Unify $ \vars ok err ->
477 let
478 ok1 vars1 () =
479 case merge context otherContent of
480 Unify k ->
481 k vars1 ok err
482 in
483 unifyAliasArgs vars context args otherArgs ok1 err
485 else
486 subUnify realVar otherRealVar
488 Structure _ ->
489 subUnify realVar (_second context)
491 Error ->
492 return ()
495unifyAliasArgs :: [Variable] -> Context -> [(N.Name,Variable)] -> [(N.Name,Variable)] -> ([Variable] -> () -> IO r) -> ([Variable] -> () -> IO r) -> IO r
496unifyAliasArgs vars context args1 args2 ok err =
497 case args1 of
498 (_,arg1):others1 ->
499 case args2 of
500 (_,arg2):others2 ->
501 case subUnify arg1 arg2 of
502 Unify k ->
503 k vars
504 (\vs () -> unifyAliasArgs vs context others1 others2 ok err)
505 (\vs () -> unifyAliasArgs vs context others1 others2 err err)
507 _ ->
508 err vars ()
510 [] ->
511 case args2 of
512 [] ->
513 ok vars ()
515 _ ->
516 err vars ()
520-- UNIFY STRUCTURES
523unifyStructure :: Context -> FlatType -> Content -> Content -> Unify ()
524unifyStructure context flatType content otherContent =
525 case otherContent of
526 FlexVar _ ->
527 merge context content
529 FlexSuper super _ ->
530 unifyFlexSuperStructure (reorient context) super flatType
532 RigidVar _ ->
533 mismatch
535 RigidSuper _ _ ->
536 mismatch
538 Alias _ _ _ realVar ->
539 subUnify (_first context) realVar
541 Structure otherFlatType ->
542 case (flatType, otherFlatType) of
543 (App1 home name args, App1 otherHome otherName otherArgs) | home == otherHome && name == otherName ->
544 Unify $ \vars ok err ->
545 let
546 ok1 vars1 () =
547 case merge context otherContent of
548 Unify k ->
549 k vars1 ok err
550 in
551 unifyArgs vars context args otherArgs ok1 err
553 (Fun1 arg1 res1, Fun1 arg2 res2) ->
554 do try2
555 (subUnify arg1 arg2)
556 (subUnify res1 res2)
557 merge context otherContent
559 (EmptyRecord1, EmptyRecord1) ->
560 merge context otherContent
562 (Record1 fields ext, EmptyRecord1) | Map.null fields ->
563 subUnify ext (_second context)
565 (EmptyRecord1, Record1 fields ext) | Map.null fields ->
566 subUnify (_first context) ext
568 (Record1 fields1 ext1, Record1 fields2 ext2) ->
569 Unify $ \vars ok err ->
570 do structure1 <- gatherFields fields1 ext1
571 structure2 <- gatherFields fields2 ext2
572 case unifyRecord context structure1 structure2 of
573 Unify k ->
574 k vars ok err
576 (Tuple1 a b Nothing, Tuple1 x y Nothing) ->
577 do try2
578 (subUnify a x)
579 (subUnify b y)
580 merge context otherContent
582 (Tuple1 a b (Just c), Tuple1 x y (Just z)) ->
583 do try3
584 (subUnify a x)
585 (subUnify b y)
586 (subUnify c z)
587 merge context otherContent
589 (Unit1, Unit1) ->
590 merge context otherContent
592 _ ->
593 mismatch
595 Error ->
596 return ()
600-- UNIFY ARGS
603unifyArgs :: [Variable] -> Context -> [Variable] -> [Variable] -> ([Variable] -> () -> IO r) -> ([Variable] -> () -> IO r) -> IO r
604unifyArgs vars context args1 args2 ok err =
605 case args1 of
606 arg1:others1 ->
607 case args2 of
608 arg2:others2 ->
609 case subUnify arg1 arg2 of
610 Unify k ->
611 k vars
612 (\vs () -> unifyArgs vs context others1 others2 ok err)
613 (\vs () -> unifyArgs vs context others1 others2 err err)
615 _ ->
616 err vars ()
618 [] ->
619 case args2 of
620 [] ->
621 ok vars ()
623 _ ->
624 err vars ()
628-- UNIFY RECORDS
631unifyRecord :: Context -> RecordStructure -> RecordStructure -> Unify ()
632unifyRecord context (RecordStructure fields1 ext1) (RecordStructure fields2 ext2) =
633 let
634 sharedFields = Map.intersectionWith (,) fields1 fields2
635 uniqueFields1 = Map.difference fields1 fields2
636 uniqueFields2 = Map.difference fields2 fields1
637 in
638 if Map.null uniqueFields1 then
640 if Map.null uniqueFields2 then
641 try2
642 (subUnify ext1 ext2)
643 (unifySharedFields context sharedFields Map.empty ext1)
645 else
646 do subRecord <- fresh context (Structure (Record1 uniqueFields2 ext2))
647 try2
648 (subUnify ext1 subRecord)
649 (unifySharedFields context sharedFields Map.empty subRecord)
651 else
653 if Map.null uniqueFields2 then
654 do subRecord <- fresh context (Structure (Record1 uniqueFields1 ext1))
655 try2
656 (subUnify subRecord ext2)
657 (unifySharedFields context sharedFields Map.empty subRecord)
659 else
660 do let otherFields = Map.union uniqueFields1 uniqueFields2
661 ext <- fresh context Type.unnamedFlexVar
662 sub1 <- fresh context (Structure (Record1 uniqueFields1 ext))
663 sub2 <- fresh context (Structure (Record1 uniqueFields2 ext))
664 try3
665 (subUnify ext1 sub2)
666 (subUnify sub1 ext2)
667 (unifySharedFields context sharedFields otherFields ext)
670unifySharedFields :: Context -> Map.Map N.Name (Variable, Variable) -> Map.Map N.Name Variable -> Variable -> Unify ()
671unifySharedFields context sharedFields otherFields ext =
672 do matchingFields <- Map.traverseMaybeWithKey unifyField sharedFields
673 if Map.size sharedFields == Map.size matchingFields
674 then merge context (Structure (Record1 (Map.union matchingFields otherFields) ext))
675 else mismatch
678unifyField :: N.Name -> (Variable, Variable) -> Unify (Maybe Variable)
679unifyField _ (actual, expected) =
680 Unify $ \vars ok _ ->
681 case subUnify actual expected of
682 Unify k ->
683 k vars
684 (\vs () -> ok vs (Just actual))
685 (\vs () -> ok vs Nothing)
689-- GATHER RECORD STRUCTURE
692data RecordStructure =
693 RecordStructure
694 { _fields :: Map.Map N.Name Variable
695 , _extension :: Variable
696 }
699gatherFields :: Map.Map N.Name Variable -> Variable -> IO RecordStructure
700gatherFields fields variable =
701 do (Descriptor content _ _ _) <- UF.get variable
702 case content of
703 Structure (Record1 subFields subExt) ->
704 gatherFields (Map.union fields subFields) subExt
706 Alias _ _ _ var ->
707 -- TODO may be dropping useful alias info here
708 gatherFields fields var
710 _ ->
711 return (RecordStructure fields variable)