git.iko.soy/elk
on ca2be8a help sign in
elk/src/Type/Unify.hs
713 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 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 return ()
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 home == ModuleName.basics
364 &&
365 case super of
366 Number ->
367 name == N.int
368 || name == N.float
370 Comparable ->
371 name == N.int
372 || name == N.float
373 || name == N.string
374 || name == N.char
376 Appendable ->
377 name == N.string
379 CompAppend ->
380 name == N.string
383unifyFlexSuperStructure :: Context -> SuperType -> FlatType -> Unify ()
384unifyFlexSuperStructure context super flatType =
385 case flatType of
386 App1 home name [] ->
387 if atomMatchesSuper super home name then
388 merge context (Structure flatType)
389 else
390 mismatch
392 App1 home name [variable] | home == ModuleName.list && name == N.list ->
393 case super of
394 Number ->
395 mismatch
397 Appendable ->
398 merge context (Structure flatType)
400 Comparable ->
401 do comparableOccursCheck context
402 merge context (Structure flatType)
403 unifyComparableRecursive variable
405 CompAppend ->
406 do comparableOccursCheck context
407 merge context (Structure flatType)
408 unifyComparableRecursive variable
410 Tuple1 a b maybeC ->
411 case super of
412 Number ->
413 mismatch
415 Appendable ->
416 mismatch
418 Comparable ->
419 do comparableOccursCheck context
420 merge context (Structure flatType)
421 unifyComparableRecursive a
422 unifyComparableRecursive b
423 case maybeC of
424 Nothing ->
425 return ()
427 Just c ->
428 unifyComparableRecursive c
430 CompAppend ->
431 mismatch
433 _ ->
434 mismatch
437-- TODO: is there some way to avoid doing this?
438-- Do type classes require occurs checks?
439comparableOccursCheck :: Context -> Unify ()
440comparableOccursCheck (Context _ _ var _) =
441 Unify $ \vars ok err ->
442 do hasOccurred <- Occurs.occurs var
443 if hasOccurred
444 then err vars ()
445 else ok vars ()
448unifyComparableRecursive :: Variable -> Unify ()
449unifyComparableRecursive var =
450 do compVar <- register $
451 do (Descriptor _ rank _ _) <- UF.get var
452 UF.fresh $ Descriptor (Type.unnamedFlexSuper Comparable) rank noMark Nothing
453 guardedUnify compVar var
457-- UNIFY ALIASES
460unifyAlias :: Context -> ModuleName.Canonical -> N.Name -> [(N.Name, Variable)] -> Variable -> Content -> Unify ()
461unifyAlias context home name args realVar otherContent =
462 case otherContent of
463 FlexVar _ ->
464 merge context (Alias home name args realVar)
466 FlexSuper _ _ ->
467 subUnify realVar (_second context)
469 RigidVar _ ->
470 subUnify realVar (_second context)
472 RigidSuper _ _ ->
473 subUnify realVar (_second context)
475 Alias otherHome otherName otherArgs otherRealVar ->
476 if name == otherName && home == otherHome then
477 Unify $ \vars ok err ->
478 let
479 ok1 vars1 () =
480 case merge context otherContent of
481 Unify k ->
482 k vars1 ok err
483 in
484 unifyAliasArgs vars context args otherArgs ok1 err
486 else
487 subUnify realVar otherRealVar
489 Structure _ ->
490 subUnify realVar (_second context)
492 Error ->
493 return ()
496unifyAliasArgs :: [Variable] -> Context -> [(N.Name,Variable)] -> [(N.Name,Variable)] -> ([Variable] -> () -> IO r) -> ([Variable] -> () -> IO r) -> IO r
497unifyAliasArgs vars context args1 args2 ok err =
498 case args1 of
499 (_,arg1):others1 ->
500 case args2 of
501 (_,arg2):others2 ->
502 case subUnify arg1 arg2 of
503 Unify k ->
504 k vars
505 (\vs () -> unifyAliasArgs vs context others1 others2 ok err)
506 (\vs () -> unifyAliasArgs vs context others1 others2 err err)
508 _ ->
509 err vars ()
511 [] ->
512 case args2 of
513 [] ->
514 ok vars ()
516 _ ->
517 err vars ()
521-- UNIFY STRUCTURES
524unifyStructure :: Context -> FlatType -> Content -> Content -> Unify ()
525unifyStructure context flatType content otherContent =
526 case otherContent of
527 FlexVar _ ->
528 merge context content
530 FlexSuper super _ ->
531 unifyFlexSuperStructure (reorient context) super flatType
533 RigidVar _ ->
534 mismatch
536 RigidSuper _ _ ->
537 mismatch
539 Alias _ _ _ realVar ->
540 subUnify (_first context) realVar
542 Structure otherFlatType ->
543 case (flatType, otherFlatType) of
544 (App1 home name args, App1 otherHome otherName otherArgs) | home == otherHome && name == otherName ->
545 Unify $ \vars ok err ->
546 let
547 ok1 vars1 () =
548 case merge context otherContent of
549 Unify k ->
550 k vars1 ok err
551 in
552 unifyArgs vars context args otherArgs ok1 err
554 (Fun1 arg1 res1, Fun1 arg2 res2) ->
555 do try2
556 (subUnify arg1 arg2)
557 (subUnify res1 res2)
558 merge context otherContent
560 (EmptyRecord1, EmptyRecord1) ->
561 merge context otherContent
563 (Record1 fields ext, EmptyRecord1) | Map.null fields ->
564 subUnify ext (_second context)
566 (EmptyRecord1, Record1 fields ext) | Map.null fields ->
567 subUnify (_first context) ext
569 (Record1 fields1 ext1, Record1 fields2 ext2) ->
570 Unify $ \vars ok err ->
571 do structure1 <- gatherFields fields1 ext1
572 structure2 <- gatherFields fields2 ext2
573 case unifyRecord context structure1 structure2 of
574 Unify k ->
575 k vars ok err
577 (Tuple1 a b Nothing, Tuple1 x y Nothing) ->
578 do try2
579 (subUnify a x)
580 (subUnify b y)
581 merge context otherContent
583 (Tuple1 a b (Just c), Tuple1 x y (Just z)) ->
584 do try3
585 (subUnify a x)
586 (subUnify b y)
587 (subUnify c z)
588 merge context otherContent
590 (Unit1, Unit1) ->
591 merge context otherContent
593 _ ->
594 mismatch
596 Error ->
597 return ()
601-- UNIFY ARGS
604unifyArgs :: [Variable] -> Context -> [Variable] -> [Variable] -> ([Variable] -> () -> IO r) -> ([Variable] -> () -> IO r) -> IO r
605unifyArgs vars context args1 args2 ok err =
606 case args1 of
607 arg1:others1 ->
608 case args2 of
609 arg2:others2 ->
610 case subUnify arg1 arg2 of
611 Unify k ->
612 k vars
613 (\vs () -> unifyArgs vs context others1 others2 ok err)
614 (\vs () -> unifyArgs vs context others1 others2 err err)
616 _ ->
617 err vars ()
619 [] ->
620 case args2 of
621 [] ->
622 ok vars ()
624 _ ->
625 err vars ()
629-- UNIFY RECORDS
632unifyRecord :: Context -> RecordStructure -> RecordStructure -> Unify ()
633unifyRecord context (RecordStructure fields1 ext1) (RecordStructure fields2 ext2) =
634 let
635 sharedFields = Map.intersectionWith (,) fields1 fields2
636 uniqueFields1 = Map.difference fields1 fields2
637 uniqueFields2 = Map.difference fields2 fields1
638 in
639 if Map.null uniqueFields1 then
641 if Map.null uniqueFields2 then
642 try2
643 (subUnify ext1 ext2)
644 (unifySharedFields context sharedFields Map.empty ext1)
646 else
647 do subRecord <- fresh context (Structure (Record1 uniqueFields2 ext2))
648 try2
649 (subUnify ext1 subRecord)
650 (unifySharedFields context sharedFields Map.empty subRecord)
652 else
654 if Map.null uniqueFields2 then
655 do subRecord <- fresh context (Structure (Record1 uniqueFields1 ext1))
656 try2
657 (subUnify subRecord ext2)
658 (unifySharedFields context sharedFields Map.empty subRecord)
660 else
661 do let otherFields = Map.union uniqueFields1 uniqueFields2
662 ext <- fresh context Type.unnamedFlexVar
663 sub1 <- fresh context (Structure (Record1 uniqueFields1 ext))
664 sub2 <- fresh context (Structure (Record1 uniqueFields2 ext))
665 try3
666 (subUnify ext1 sub2)
667 (subUnify sub1 ext2)
668 (unifySharedFields context sharedFields otherFields ext)
671unifySharedFields :: Context -> Map.Map N.Name (Variable, Variable) -> Map.Map N.Name Variable -> Variable -> Unify ()
672unifySharedFields context sharedFields otherFields ext =
673 do matchingFields <- Map.traverseMaybeWithKey unifyField sharedFields
674 if Map.size sharedFields == Map.size matchingFields
675 then merge context (Structure (Record1 (Map.union matchingFields otherFields) ext))
676 else mismatch
679unifyField :: N.Name -> (Variable, Variable) -> Unify (Maybe Variable)
680unifyField _ (actual, expected) =
681 Unify $ \vars ok _ ->
682 case subUnify actual expected of
683 Unify k ->
684 k vars
685 (\vs () -> ok vs (Just actual))
686 (\vs () -> ok vs Nothing)
690-- GATHER RECORD STRUCTURE
693data RecordStructure =
694 RecordStructure
695 { _fields :: Map.Map N.Name Variable
696 , _extension :: Variable
697 }
700gatherFields :: Map.Map N.Name Variable -> Variable -> IO RecordStructure
701gatherFields fields variable =
702 do (Descriptor content _ _ _) <- UF.get variable
703 case content of
704 Structure (Record1 subFields subExt) ->
705 gatherFields (Map.union fields subFields) subExt
707 Alias _ _ _ var ->
708 -- TODO may be dropping useful alias info here
709 gatherFields fields var
711 _ ->
712 return (RecordStructure fields variable)