git.iko.soy/elk
on 6a96e21 help sign in
elk/compiler/src/Type/Unify.hs
716 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 merge context Error
222-- UNIFY FLEXIBLE VARIABLES
225unifyFlex :: Context -> Content -> Content -> Unify ()
226unifyFlex context content otherContent =
227 case otherContent of
228 Error ->
229 merge context Error
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 merge context Error
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 Appendable -> mismatch
324 CompAppend -> mismatch
326 Comparable ->
327 case otherSuper of
328 Comparable -> merge context otherContent
329 Number -> merge context otherContent
330 Appendable -> merge context (Type.unnamedFlexSuper CompAppend)
331 CompAppend -> merge context otherContent
333 Appendable ->
334 case otherSuper of
335 Appendable -> merge context otherContent
336 Comparable -> merge context (Type.unnamedFlexSuper CompAppend)
337 CompAppend -> merge context otherContent
338 Number -> mismatch
340 CompAppend ->
341 case otherSuper of
342 Comparable -> merge context content
343 Appendable -> merge context content
344 CompAppend -> merge context content
345 Number -> mismatch
347 Alias _ _ _ realVar ->
348 subUnify (_first context) realVar
350 Error ->
351 merge context Error
354combineRigidSupers :: SuperType -> SuperType -> Bool
355combineRigidSupers rigid flex =
356 rigid == flex
357 || (rigid == Number && flex == Comparable)
358 || (rigid == CompAppend && (flex == Comparable || flex == Appendable))
361atomMatchesSuper :: SuperType -> ModuleName.Canonical -> N.Name -> Bool
362atomMatchesSuper super home name =
363 case super of
364 Number ->
365 isNumber home name
367 Comparable ->
368 isNumber home name
369 || Error.isString home name
370 || Error.isChar home name
372 Appendable ->
373 Error.isString home name
375 CompAppend ->
376 Error.isString home name
379isNumber :: ModuleName.Canonical -> N.Name -> Bool
380isNumber home name =
381 home == ModuleName.basics
382 &&
383 (name == N.int || name == N.float)
386unifyFlexSuperStructure :: Context -> SuperType -> FlatType -> Unify ()
387unifyFlexSuperStructure context super flatType =
388 case flatType of
389 App1 home name [] ->
390 if atomMatchesSuper super home name then
391 merge context (Structure flatType)
392 else
393 mismatch
395 App1 home name [variable] | home == ModuleName.list && name == N.list ->
396 case super of
397 Number ->
398 mismatch
400 Appendable ->
401 merge context (Structure flatType)
403 Comparable ->
404 do comparableOccursCheck context
405 merge context (Structure flatType)
406 unifyComparableRecursive variable
408 CompAppend ->
409 do comparableOccursCheck context
410 merge context (Structure flatType)
411 unifyComparableRecursive variable
413 Tuple1 a b maybeC ->
414 case super of
415 Number ->
416 mismatch
418 Appendable ->
419 mismatch
421 Comparable ->
422 do comparableOccursCheck context
423 merge context (Structure flatType)
424 unifyComparableRecursive a
425 unifyComparableRecursive b
426 case maybeC of
427 Nothing ->
428 return ()
430 Just c ->
431 unifyComparableRecursive c
433 CompAppend ->
434 mismatch
436 _ ->
437 mismatch
440-- TODO: is there some way to avoid doing this?
441-- Do type classes require occurs checks?
442comparableOccursCheck :: Context -> Unify ()
443comparableOccursCheck (Context _ _ var _) =
444 Unify $ \vars ok err ->
445 do hasOccurred <- Occurs.occurs var
446 if hasOccurred
447 then err vars ()
448 else ok vars ()
451unifyComparableRecursive :: Variable -> Unify ()
452unifyComparableRecursive var =
453 do compVar <- register $
454 do (Descriptor _ rank _ _) <- UF.get var
455 UF.fresh $ Descriptor (Type.unnamedFlexSuper Comparable) rank noMark Nothing
456 guardedUnify compVar var
460-- UNIFY ALIASES
463unifyAlias :: Context -> ModuleName.Canonical -> N.Name -> [(N.Name, Variable)] -> Variable -> Content -> Unify ()
464unifyAlias context home name args realVar otherContent =
465 case otherContent of
466 FlexVar _ ->
467 merge context (Alias home name args realVar)
469 FlexSuper _ _ ->
470 subUnify realVar (_second context)
472 RigidVar _ ->
473 subUnify realVar (_second context)
475 RigidSuper _ _ ->
476 subUnify realVar (_second context)
478 Alias otherHome otherName otherArgs otherRealVar ->
479 if name == otherName && home == otherHome then
480 Unify $ \vars ok err ->
481 let
482 ok1 vars1 () =
483 case merge context otherContent of
484 Unify k ->
485 k vars1 ok err
486 in
487 unifyAliasArgs vars context args otherArgs ok1 err
489 else
490 subUnify realVar otherRealVar
492 Structure _ ->
493 subUnify realVar (_second context)
495 Error ->
496 merge context Error
499unifyAliasArgs :: [Variable] -> Context -> [(N.Name,Variable)] -> [(N.Name,Variable)] -> ([Variable] -> () -> IO r) -> ([Variable] -> () -> IO r) -> IO r
500unifyAliasArgs vars context args1 args2 ok err =
501 case args1 of
502 (_,arg1):others1 ->
503 case args2 of
504 (_,arg2):others2 ->
505 case subUnify arg1 arg2 of
506 Unify k ->
507 k vars
508 (\vs () -> unifyAliasArgs vs context others1 others2 ok err)
509 (\vs () -> unifyAliasArgs vs context others1 others2 err err)
511 _ ->
512 err vars ()
514 [] ->
515 case args2 of
516 [] ->
517 ok vars ()
519 _ ->
520 err vars ()
524-- UNIFY STRUCTURES
527unifyStructure :: Context -> FlatType -> Content -> Content -> Unify ()
528unifyStructure context flatType content otherContent =
529 case otherContent of
530 FlexVar _ ->
531 merge context content
533 FlexSuper super _ ->
534 unifyFlexSuperStructure (reorient context) super flatType
536 RigidVar _ ->
537 mismatch
539 RigidSuper _ _ ->
540 mismatch
542 Alias _ _ _ realVar ->
543 subUnify (_first context) realVar
545 Structure otherFlatType ->
546 case (flatType, otherFlatType) of
547 (App1 home name args, App1 otherHome otherName otherArgs) | home == otherHome && name == otherName ->
548 Unify $ \vars ok err ->
549 let
550 ok1 vars1 () =
551 case merge context otherContent of
552 Unify k ->
553 k vars1 ok err
554 in
555 unifyArgs vars context args otherArgs ok1 err
557 (Fun1 arg1 res1, Fun1 arg2 res2) ->
558 do try2
559 (subUnify arg1 arg2)
560 (subUnify res1 res2)
561 merge context otherContent
563 (EmptyRecord1, EmptyRecord1) ->
564 merge context otherContent
566 (Record1 fields ext, EmptyRecord1) | Map.null fields ->
567 subUnify ext (_second context)
569 (EmptyRecord1, Record1 fields ext) | Map.null fields ->
570 subUnify (_first context) ext
572 (Record1 fields1 ext1, Record1 fields2 ext2) ->
573 Unify $ \vars ok err ->
574 do structure1 <- gatherFields fields1 ext1
575 structure2 <- gatherFields fields2 ext2
576 case unifyRecord context structure1 structure2 of
577 Unify k ->
578 k vars ok err
580 (Tuple1 a b Nothing, Tuple1 x y Nothing) ->
581 do try2
582 (subUnify a x)
583 (subUnify b y)
584 merge context otherContent
586 (Tuple1 a b (Just c), Tuple1 x y (Just z)) ->
587 do try3
588 (subUnify a x)
589 (subUnify b y)
590 (subUnify c z)
591 merge context otherContent
593 (Unit1, Unit1) ->
594 merge context otherContent
596 _ ->
597 mismatch
599 Error ->
600 merge context Error
604-- UNIFY ARGS
607unifyArgs :: [Variable] -> Context -> [Variable] -> [Variable] -> ([Variable] -> () -> IO r) -> ([Variable] -> () -> IO r) -> IO r
608unifyArgs vars context args1 args2 ok err =
609 case args1 of
610 arg1:others1 ->
611 case args2 of
612 arg2:others2 ->
613 case subUnify arg1 arg2 of
614 Unify k ->
615 k vars
616 (\vs () -> unifyArgs vs context others1 others2 ok err)
617 (\vs () -> unifyArgs vs context others1 others2 err err)
619 _ ->
620 err vars ()
622 [] ->
623 case args2 of
624 [] ->
625 ok vars ()
627 _ ->
628 err vars ()
632-- UNIFY RECORDS
635unifyRecord :: Context -> RecordStructure -> RecordStructure -> Unify ()
636unifyRecord context (RecordStructure fields1 ext1) (RecordStructure fields2 ext2) =
637 let
638 sharedFields = Map.intersectionWith (,) fields1 fields2
639 uniqueFields1 = Map.difference fields1 fields2
640 uniqueFields2 = Map.difference fields2 fields1
641 in
642 if Map.null uniqueFields1 then
644 if Map.null uniqueFields2 then
645 try2
646 (subUnify ext1 ext2)
647 (unifySharedFields context sharedFields Map.empty ext1)
649 else
650 do subRecord <- fresh context (Structure (Record1 uniqueFields2 ext2))
651 try2
652 (subUnify ext1 subRecord)
653 (unifySharedFields context sharedFields Map.empty subRecord)
655 else
657 if Map.null uniqueFields2 then
658 do subRecord <- fresh context (Structure (Record1 uniqueFields1 ext1))
659 try2
660 (subUnify subRecord ext2)
661 (unifySharedFields context sharedFields Map.empty subRecord)
663 else
664 do let otherFields = Map.union uniqueFields1 uniqueFields2
665 ext <- fresh context Type.unnamedFlexVar
666 sub1 <- fresh context (Structure (Record1 uniqueFields1 ext))
667 sub2 <- fresh context (Structure (Record1 uniqueFields2 ext))
668 try3
669 (subUnify ext1 sub2)
670 (subUnify sub1 ext2)
671 (unifySharedFields context sharedFields otherFields ext)
674unifySharedFields :: Context -> Map.Map N.Name (Variable, Variable) -> Map.Map N.Name Variable -> Variable -> Unify ()
675unifySharedFields context sharedFields otherFields ext =
676 do matchingFields <- Map.traverseMaybeWithKey unifyField sharedFields
677 if Map.size sharedFields == Map.size matchingFields
678 then merge context (Structure (Record1 (Map.union matchingFields otherFields) ext))
679 else mismatch
682unifyField :: N.Name -> (Variable, Variable) -> Unify (Maybe Variable)
683unifyField _ (actual, expected) =
684 Unify $ \vars ok _ ->
685 case subUnify actual expected of
686 Unify k ->
687 k vars
688 (\vs () -> ok vs (Just actual))
689 (\vs () -> ok vs Nothing)
693-- GATHER RECORD STRUCTURE
696data RecordStructure =
697 RecordStructure
698 { _fields :: Map.Map N.Name Variable
699 , _extension :: Variable
700 }
703gatherFields :: Map.Map N.Name Variable -> Variable -> IO RecordStructure
704gatherFields fields variable =
705 do (Descriptor content _ _ _) <- UF.get variable
706 case content of
707 Structure (Record1 subFields subExt) ->
708 gatherFields (Map.union fields subFields) subExt
710 Alias _ _ _ var ->
711 -- TODO may be dropping useful alias info here
712 gatherFields fields var
714 _ ->
715 return (RecordStructure fields variable)