git.iko.soy/elk
on 6c19c6e help sign in
elk/compiler/src/Type/Unify.hs
698 lines 17 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
11import qualified Data.Name as Name
13import qualified Elm.ModuleName as ModuleName
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
106 (>>) (Unify ka) (Unify kb) =
107 Unify $ \vars ok err ->
108 let
109 ok1 vars1 _ = kb vars1 ok err
110 in
111 ka vars ok1 err
114register :: IO Variable -> Unify Variable
115register mkVar =
116 Unify $ \vars ok _ ->
117 do var <- mkVar
118 ok (var:vars) var
121mismatch :: Unify a
122mismatch =
123 Unify $ \vars _ err ->
124 err vars ()
128-- UNIFICATION HELPERS
131data Context =
132 Context
133 { _first :: Variable
134 , _firstDesc :: Descriptor
135 , _second :: Variable
136 , _secondDesc :: Descriptor
137 }
140reorient :: Context -> Context
141reorient (Context var1 desc1 var2 desc2) =
142 Context var2 desc2 var1 desc1
146-- MERGE
149merge :: Context -> Content -> Unify ()
150merge (Context var1 (Descriptor _ rank1 _ _) var2 (Descriptor _ rank2 _ _)) content =
151 Unify $ \vars ok _ ->
152 ok vars =<<
153 UF.union var1 var2 (Descriptor content (min rank1 rank2) noMark Nothing)
156fresh :: Context -> Content -> Unify Variable
157fresh (Context _ (Descriptor _ rank1 _ _) _ (Descriptor _ rank2 _ _)) content =
158 register $ UF.fresh $
159 Descriptor content (min rank1 rank2) noMark Nothing
163-- ACTUALLY UNIFY THINGS
166guardedUnify :: Variable -> Variable -> Unify ()
167guardedUnify left right =
168 Unify $ \vars ok err ->
169 do equivalent <- UF.equivalent left right
170 if equivalent
171 then ok vars ()
172 else
173 do leftDesc <- UF.get left
174 rightDesc <- UF.get right
175 case actuallyUnify (Context left leftDesc right rightDesc) of
176 Unify k ->
177 k vars ok err
180subUnify :: Variable -> Variable -> Unify ()
181subUnify var1 var2 =
182 guardedUnify var1 var2
185actuallyUnify :: Context -> Unify ()
186actuallyUnify context@(Context _ (Descriptor firstContent _ _ _) _ (Descriptor secondContent _ _ _)) =
187 case firstContent of
188 FlexVar _ ->
189 unifyFlex context firstContent secondContent
191 FlexSuper super _ ->
192 unifyFlexSuper context super firstContent secondContent
194 RigidVar _ ->
195 unifyRigid context Nothing firstContent secondContent
197 RigidSuper super _ ->
198 unifyRigid context (Just super) firstContent secondContent
200 Alias home name args realVar ->
201 unifyAlias context home name args realVar secondContent
203 Structure flatType ->
204 unifyStructure context flatType firstContent secondContent
206 Error ->
207 -- If there was an error, just pretend it is okay. This lets us avoid
208 -- "cascading" errors where one problem manifests as multiple message.
209 merge context Error
213-- UNIFY FLEXIBLE VARIABLES
216unifyFlex :: Context -> Content -> Content -> Unify ()
217unifyFlex context content otherContent =
218 case otherContent of
219 Error ->
220 merge context Error
222 FlexVar maybeName ->
223 merge context $
224 case maybeName of
225 Nothing ->
226 content
228 Just _ ->
229 otherContent
231 FlexSuper _ _ ->
232 merge context otherContent
234 RigidVar _ ->
235 merge context otherContent
237 RigidSuper _ _ ->
238 merge context otherContent
240 Alias _ _ _ _ ->
241 merge context otherContent
243 Structure _ ->
244 merge context otherContent
248-- UNIFY RIGID VARIABLES
251unifyRigid :: Context -> Maybe SuperType -> Content -> Content -> Unify ()
252unifyRigid context maybeSuper content otherContent =
253 case otherContent of
254 FlexVar _ ->
255 merge context content
257 FlexSuper otherSuper _ ->
258 case maybeSuper of
259 Just super ->
260 if combineRigidSupers super otherSuper then
261 merge context content
262 else
263 mismatch
265 Nothing ->
266 mismatch
268 RigidVar _ ->
269 mismatch
271 RigidSuper _ _ ->
272 mismatch
274 Alias _ _ _ _ ->
275 mismatch
277 Structure _ ->
278 mismatch
280 Error ->
281 merge context Error
285-- UNIFY SUPER VARIABLES
288unifyFlexSuper :: Context -> SuperType -> Content -> Content -> Unify ()
289unifyFlexSuper context super content otherContent =
290 case otherContent of
291 Structure flatType ->
292 unifyFlexSuperStructure context super flatType
294 RigidVar _ ->
295 mismatch
297 RigidSuper otherSuper _ ->
298 if combineRigidSupers otherSuper super then
299 merge context otherContent
300 else
301 mismatch
303 FlexVar _ ->
304 merge context content
306 FlexSuper otherSuper _ ->
307 case super of
308 Number ->
309 case otherSuper of
310 Number -> merge context content
311 Comparable -> merge context content
312 Appendable -> mismatch
313 CompAppend -> mismatch
315 Comparable ->
316 case otherSuper of
317 Comparable -> merge context otherContent
318 Number -> merge context otherContent
319 Appendable -> merge context (Type.unnamedFlexSuper CompAppend)
320 CompAppend -> merge context otherContent
322 Appendable ->
323 case otherSuper of
324 Appendable -> merge context otherContent
325 Comparable -> merge context (Type.unnamedFlexSuper CompAppend)
326 CompAppend -> merge context otherContent
327 Number -> mismatch
329 CompAppend ->
330 case otherSuper of
331 Comparable -> merge context content
332 Appendable -> merge context content
333 CompAppend -> merge context content
334 Number -> mismatch
336 Alias _ _ _ realVar ->
337 subUnify (_first context) realVar
339 Error ->
340 merge context Error
343combineRigidSupers :: SuperType -> SuperType -> Bool
344combineRigidSupers rigid flex =
345 rigid == flex
346 || (rigid == Number && flex == Comparable)
347 || (rigid == CompAppend && (flex == Comparable || flex == Appendable))
350atomMatchesSuper :: SuperType -> ModuleName.Canonical -> Name.Name -> Bool
351atomMatchesSuper super home name =
352 case super of
353 Number ->
354 isNumber home name
356 Comparable ->
357 isNumber home name
358 || Error.isString home name
359 || Error.isChar home name
361 Appendable ->
362 Error.isString home name
364 CompAppend ->
365 Error.isString home name
368isNumber :: ModuleName.Canonical -> Name.Name -> Bool
369isNumber home name =
370 home == ModuleName.basics
371 &&
372 (name == Name.int || name == Name.float)
375unifyFlexSuperStructure :: Context -> SuperType -> FlatType -> Unify ()
376unifyFlexSuperStructure context super flatType =
377 case flatType of
378 App1 home name [] ->
379 if atomMatchesSuper super home name then
380 merge context (Structure flatType)
381 else
382 mismatch
384 App1 home name [variable] | home == ModuleName.list && name == Name.list ->
385 case super of
386 Number ->
387 mismatch
389 Appendable ->
390 merge context (Structure flatType)
392 Comparable ->
393 do comparableOccursCheck context
394 merge context (Structure flatType)
395 unifyComparableRecursive variable
397 CompAppend ->
398 do comparableOccursCheck context
399 merge context (Structure flatType)
400 unifyComparableRecursive variable
402 Tuple1 a b maybeC ->
403 case super of
404 Number ->
405 mismatch
407 Appendable ->
408 mismatch
410 Comparable ->
411 do comparableOccursCheck context
412 merge context (Structure flatType)
413 unifyComparableRecursive a
414 unifyComparableRecursive b
415 case maybeC of
416 Nothing ->
417 return ()
419 Just c ->
420 unifyComparableRecursive c
422 CompAppend ->
423 mismatch
425 _ ->
426 mismatch
429-- TODO: is there some way to avoid doing this?
430-- Do type classes require occurs checks?
431comparableOccursCheck :: Context -> Unify ()
432comparableOccursCheck (Context _ _ var _) =
433 Unify $ \vars ok err ->
434 do hasOccurred <- Occurs.occurs var
435 if hasOccurred
436 then err vars ()
437 else ok vars ()
440unifyComparableRecursive :: Variable -> Unify ()
441unifyComparableRecursive var =
442 do compVar <- register $
443 do (Descriptor _ rank _ _) <- UF.get var
444 UF.fresh $ Descriptor (Type.unnamedFlexSuper Comparable) rank noMark Nothing
445 guardedUnify compVar var
449-- UNIFY ALIASES
452unifyAlias :: Context -> ModuleName.Canonical -> Name.Name -> [(Name.Name, Variable)] -> Variable -> Content -> Unify ()
453unifyAlias context home name args realVar otherContent =
454 case otherContent of
455 FlexVar _ ->
456 merge context (Alias home name args realVar)
458 FlexSuper _ _ ->
459 subUnify realVar (_second context)
461 RigidVar _ ->
462 subUnify realVar (_second context)
464 RigidSuper _ _ ->
465 subUnify realVar (_second context)
467 Alias otherHome otherName otherArgs otherRealVar ->
468 if name == otherName && home == otherHome then
469 Unify $ \vars ok err ->
470 let
471 ok1 vars1 () =
472 case merge context otherContent of
473 Unify k ->
474 k vars1 ok err
475 in
476 unifyAliasArgs vars context args otherArgs ok1 err
478 else
479 subUnify realVar otherRealVar
481 Structure _ ->
482 subUnify realVar (_second context)
484 Error ->
485 merge context Error
488unifyAliasArgs :: [Variable] -> Context -> [(Name.Name,Variable)] -> [(Name.Name,Variable)] -> ([Variable] -> () -> IO r) -> ([Variable] -> () -> IO r) -> IO r
489unifyAliasArgs vars context args1 args2 ok err =
490 case args1 of
491 (_,arg1):others1 ->
492 case args2 of
493 (_,arg2):others2 ->
494 case subUnify arg1 arg2 of
495 Unify k ->
496 k vars
497 (\vs () -> unifyAliasArgs vs context others1 others2 ok err)
498 (\vs () -> unifyAliasArgs vs context others1 others2 err err)
500 _ ->
501 err vars ()
503 [] ->
504 case args2 of
505 [] ->
506 ok vars ()
508 _ ->
509 err vars ()
513-- UNIFY STRUCTURES
516unifyStructure :: Context -> FlatType -> Content -> Content -> Unify ()
517unifyStructure context flatType content otherContent =
518 case otherContent of
519 FlexVar _ ->
520 merge context content
522 FlexSuper super _ ->
523 unifyFlexSuperStructure (reorient context) super flatType
525 RigidVar _ ->
526 mismatch
528 RigidSuper _ _ ->
529 mismatch
531 Alias _ _ _ realVar ->
532 subUnify (_first context) realVar
534 Structure otherFlatType ->
535 case (flatType, otherFlatType) of
536 (App1 home name args, App1 otherHome otherName otherArgs) | home == otherHome && name == otherName ->
537 Unify $ \vars ok err ->
538 let
539 ok1 vars1 () =
540 case merge context otherContent of
541 Unify k ->
542 k vars1 ok err
543 in
544 unifyArgs vars context args otherArgs ok1 err
546 (Fun1 arg1 res1, Fun1 arg2 res2) ->
547 do subUnify arg1 arg2
548 subUnify res1 res2
549 merge context otherContent
551 (EmptyRecord1, EmptyRecord1) ->
552 merge context otherContent
554 (Record1 fields ext, EmptyRecord1) | Map.null fields ->
555 subUnify ext (_second context)
557 (EmptyRecord1, Record1 fields ext) | Map.null fields ->
558 subUnify (_first context) ext
560 (Record1 fields1 ext1, Record1 fields2 ext2) ->
561 Unify $ \vars ok err ->
562 do structure1 <- gatherFields fields1 ext1
563 structure2 <- gatherFields fields2 ext2
564 case unifyRecord context structure1 structure2 of
565 Unify k ->
566 k vars ok err
568 (Tuple1 a b Nothing, Tuple1 x y Nothing) ->
569 do subUnify a x
570 subUnify b y
571 merge context otherContent
573 (Tuple1 a b (Just c), Tuple1 x y (Just z)) ->
574 do subUnify a x
575 subUnify b y
576 subUnify c z
577 merge context otherContent
579 (Unit1, Unit1) ->
580 merge context otherContent
582 _ ->
583 mismatch
585 Error ->
586 merge context Error
590-- UNIFY ARGS
593unifyArgs :: [Variable] -> Context -> [Variable] -> [Variable] -> ([Variable] -> () -> IO r) -> ([Variable] -> () -> IO r) -> IO r
594unifyArgs vars context args1 args2 ok err =
595 case args1 of
596 arg1:others1 ->
597 case args2 of
598 arg2:others2 ->
599 case subUnify arg1 arg2 of
600 Unify k ->
601 k vars
602 (\vs () -> unifyArgs vs context others1 others2 ok err)
603 (\vs () -> unifyArgs vs context others1 others2 err err)
605 _ ->
606 err vars ()
608 [] ->
609 case args2 of
610 [] ->
611 ok vars ()
613 _ ->
614 err vars ()
618-- UNIFY RECORDS
621unifyRecord :: Context -> RecordStructure -> RecordStructure -> Unify ()
622unifyRecord context (RecordStructure fields1 ext1) (RecordStructure fields2 ext2) =
623 let
624 sharedFields = Map.intersectionWith (,) fields1 fields2
625 uniqueFields1 = Map.difference fields1 fields2
626 uniqueFields2 = Map.difference fields2 fields1
627 in
628 if Map.null uniqueFields1 then
630 if Map.null uniqueFields2 then
631 do subUnify ext1 ext2
632 unifySharedFields context sharedFields Map.empty ext1
634 else
635 do subRecord <- fresh context (Structure (Record1 uniqueFields2 ext2))
636 subUnify ext1 subRecord
637 unifySharedFields context sharedFields Map.empty subRecord
639 else
641 if Map.null uniqueFields2 then
642 do subRecord <- fresh context (Structure (Record1 uniqueFields1 ext1))
643 subUnify subRecord ext2
644 unifySharedFields context sharedFields Map.empty subRecord
646 else
647 do let otherFields = Map.union uniqueFields1 uniqueFields2
648 ext <- fresh context Type.unnamedFlexVar
649 sub1 <- fresh context (Structure (Record1 uniqueFields1 ext))
650 sub2 <- fresh context (Structure (Record1 uniqueFields2 ext))
651 subUnify ext1 sub2
652 subUnify sub1 ext2
653 unifySharedFields context sharedFields otherFields ext
656unifySharedFields :: Context -> Map.Map Name.Name (Variable, Variable) -> Map.Map Name.Name Variable -> Variable -> Unify ()
657unifySharedFields context sharedFields otherFields ext =
658 do matchingFields <- Map.traverseMaybeWithKey unifyField sharedFields
659 if Map.size sharedFields == Map.size matchingFields
660 then merge context (Structure (Record1 (Map.union matchingFields otherFields) ext))
661 else mismatch
664unifyField :: Name.Name -> (Variable, Variable) -> Unify (Maybe Variable)
665unifyField _ (actual, expected) =
666 Unify $ \vars ok _ ->
667 case subUnify actual expected of
668 Unify k ->
669 k vars
670 (\vs () -> ok vs (Just actual))
671 (\vs () -> ok vs Nothing)
675-- GATHER RECORD STRUCTURE
678data RecordStructure =
679 RecordStructure
680 { _fields :: Map.Map Name.Name Variable
681 , _extension :: Variable
682 }
685gatherFields :: Map.Map Name.Name Variable -> Variable -> IO RecordStructure
686gatherFields fields variable =
687 do (Descriptor content _ _ _) <- UF.get variable
688 case content of
689 Structure (Record1 subFields subExt) ->
690 gatherFields (Map.union fields subFields) subExt
692 Alias _ _ _ var ->
693 -- TODO may be dropping useful alias info here
694 gatherFields fields var
696 _ ->
697 return (RecordStructure fields variable)