git.iko.soy/elk
on dc356df help sign in
elk/src/Type/Unify.hs
714 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.Canonical as Can
13import qualified AST.Module.Name as ModuleName
14import qualified Elm.Name as N
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] Can.Type Can.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.toSrcType v1
35 t2 <- Type.toSrcType 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 )
64-- TODO experiment with INLINE on the Unify instances
66instance Functor Unify where
67 fmap func (Unify kv) =
68 Unify $ \vars ok err ->
69 let
70 ok1 vars1 value =
71 ok vars1 (func value)
72 in
73 kv vars ok1 err
76instance Applicative Unify where
77 pure a =
78 Unify $ \vars ok _ ->
79 ok vars a
81 (<*>) (Unify kf) (Unify kv) =
82 Unify $ \vars ok err ->
83 let
84 ok1 vars1 func =
85 let
86 ok2 vars2 value =
87 ok vars2 (func value)
88 in
89 kv vars1 ok2 err
90 in
91 kf vars ok1 err
94instance Monad Unify where
95 return a =
96 Unify $ \vars ok _ ->
97 ok vars a
99 (>>=) (Unify ka) callback =
100 Unify $ \vars ok err ->
101 let
102 ok1 vars1 a =
103 case callback a of
104 Unify kb -> kb vars1 ok err
105 in
106 ka vars ok1 err
109register :: IO Variable -> Unify Variable
110register mkVar =
111 Unify $ \vars ok _ ->
112 do var <- mkVar
113 ok (var:vars) var
116mismatch :: Unify a
117mismatch =
118 Unify $ \vars _ err ->
119 err vars ()
122try2 :: Unify () -> Unify () -> Unify ()
123try2 (Unify k1) (Unify k2) =
124 Unify $ \vars ok err ->
125 let
126 ok1 vars1 () = k2 vars1 ok err
127 err1 vars1 () = k2 vars1 err err
128 in
129 k1 vars ok1 err1
132{-# INLINE try3 #-}
133try3 :: Unify () -> Unify () -> Unify () -> Unify ()
134try3 u1 u2 u3 =
135 try2 u1 (try2 u2 u3)
139-- UNIFICATION HELPERS
142data Context =
143 Context
144 { _first :: Variable
145 , _firstDesc :: Descriptor
146 , _second :: Variable
147 , _secondDesc :: Descriptor
148 }
151reorient :: Context -> Context
152reorient (Context var1 desc1 var2 desc2) =
153 Context var2 desc2 var1 desc1
157-- MERGE
160merge :: Context -> Content -> Unify ()
161merge (Context var1 (Descriptor _ rank1 _ _) var2 (Descriptor _ rank2 _ _)) content =
162 Unify $ \vars ok _ ->
163 ok vars =<<
164 UF.union var1 var2 (Descriptor content (min rank1 rank2) noMark Nothing)
167fresh :: Context -> Content -> Unify Variable
168fresh (Context _ (Descriptor _ rank1 _ _) _ (Descriptor _ rank2 _ _)) content =
169 register $ UF.fresh $
170 Descriptor content (min rank1 rank2) noMark Nothing
174-- ACTUALLY UNIFY THINGS
177guardedUnify :: Variable -> Variable -> Unify ()
178guardedUnify left right =
179 Unify $ \vars ok err ->
180 do equivalent <- UF.equivalent left right
181 if equivalent
182 then ok vars ()
183 else
184 do leftDesc <- UF.get left
185 rightDesc <- UF.get right
186 case actuallyUnify (Context left leftDesc right rightDesc) of
187 Unify k ->
188 k vars ok err
191subUnify :: Variable -> Variable -> Unify ()
192subUnify var1 var2 =
193 guardedUnify var1 var2
196actuallyUnify :: Context -> Unify ()
197actuallyUnify context@(Context _ (Descriptor firstContent _ _ _) _ (Descriptor secondContent _ _ _)) =
198 case firstContent of
199 FlexVar _ ->
200 unifyFlex context firstContent secondContent
202 FlexSuper super _ ->
203 unifyFlexSuper context super firstContent secondContent
205 RigidVar _ ->
206 unifyRigid context Nothing firstContent secondContent
208 RigidSuper super _ ->
209 unifyRigid context (Just super) firstContent secondContent
211 Alias home name args realVar ->
212 unifyAlias context home name args realVar secondContent
214 Structure flatType ->
215 unifyStructure context flatType firstContent secondContent
217 Error _ ->
218 -- If there was an error, just pretend it is okay. This lets us avoid
219 -- "cascading" errors where one problem manifests as multiple message.
220 return ()
224-- UNIFY FLEXIBLE VARIABLES
227unifyFlex :: Context -> Content -> Content -> Unify ()
228unifyFlex context content otherContent =
229 case otherContent of
230 Error _ ->
231 return ()
233 -- TODO see if wildcarding makes a noticable perf difference
235 FlexVar maybeName ->
236 merge context $
237 case maybeName of
238 Nothing ->
239 content
241 Just _ ->
242 otherContent
244 FlexSuper _ _ ->
245 merge context otherContent
247 RigidVar _ ->
248 merge context otherContent
250 RigidSuper _ _ ->
251 merge context otherContent
253 Alias _ _ _ _ ->
254 merge context otherContent
256 Structure _ ->
257 merge context otherContent
261-- UNIFY RIGID VARIABLES
264unifyRigid :: Context -> Maybe SuperType -> Content -> Content -> Unify ()
265unifyRigid context maybeSuper content otherContent =
266 case otherContent of
267 FlexVar _ ->
268 merge context content
270 FlexSuper otherSuper _ ->
271 case maybeSuper of
272 Just super ->
273 if combineRigidSupers super otherSuper then
274 merge context content
275 else
276 mismatch
278 Nothing ->
279 mismatch
281 RigidVar _ ->
282 mismatch
284 RigidSuper _ _ ->
285 mismatch
287 Alias _ _ _ _ ->
288 mismatch
290 Structure _ ->
291 mismatch
293 Error _ ->
294 return ()
298-- UNIFY SUPER VARIABLES
301unifyFlexSuper :: Context -> SuperType -> Content -> Content -> Unify ()
302unifyFlexSuper context super content otherContent =
303 case otherContent of
304 Structure flatType ->
305 unifyFlexSuperStructure context super flatType
307 RigidVar _ ->
308 mismatch
310 RigidSuper otherSuper _ ->
311 if combineRigidSupers otherSuper super then
312 merge context otherContent
313 else
314 mismatch
316 FlexVar _ ->
317 merge context content
319 FlexSuper otherSuper _ ->
320 case super of
321 Number ->
322 case otherSuper of
323 Number -> merge context content
324 Comparable -> merge context content
325 _ -> mismatch
327 Comparable ->
328 case otherSuper of
329 Comparable -> merge context otherContent
330 Number -> merge context otherContent
331 Appendable -> merge context (Type.unnamedFlexSuper CompAppend)
332 CompAppend -> merge context otherContent
334 Appendable ->
335 case otherSuper of
336 Appendable -> merge context otherContent
337 Comparable -> merge context (Type.unnamedFlexSuper CompAppend)
338 CompAppend -> merge context otherContent
339 Number -> mismatch
341 CompAppend ->
342 case otherSuper of
343 Comparable -> merge context content
344 Appendable -> merge context content
345 CompAppend -> merge context content
346 Number -> mismatch
348 Alias _ _ _ realVar ->
349 subUnify (_first context) realVar
351 Error _ ->
352 return ()
355combineRigidSupers :: SuperType -> SuperType -> Bool
356combineRigidSupers rigid flex =
357 rigid == flex
358 || (rigid == Number && flex == Comparable)
359 || (rigid == CompAppend && (flex == Comparable || flex == Appendable))
362atomMatchesSuper :: SuperType -> ModuleName.Canonical -> N.Name -> Bool
363atomMatchesSuper super home name =
364 home == ModuleName.basics
365 &&
366 case super of
367 Number ->
368 name == N.int
369 || name == N.float
371 Comparable ->
372 name == N.int
373 || name == N.float
374 || name == N.string
375 || name == N.char
377 Appendable ->
378 name == N.string
380 CompAppend ->
381 name == N.string
384unifyFlexSuperStructure :: Context -> SuperType -> FlatType -> Unify ()
385unifyFlexSuperStructure context super flatType =
386 case flatType of
387 App1 home name [] ->
388 if atomMatchesSuper super home name then
389 merge context (Structure flatType)
390 else
391 mismatch
393 App1 home name [variable] | home == ModuleName.list && name == N.list ->
394 case super of
395 Number ->
396 mismatch
398 Appendable ->
399 merge context (Structure flatType)
401 Comparable ->
402 do comparableOccursCheck context
403 merge context (Structure flatType)
404 unifyComparableRecursive variable
406 CompAppend ->
407 do comparableOccursCheck context
408 merge context (Structure flatType)
409 unifyComparableRecursive variable
411 Tuple1 a b maybeC ->
412 case super of
413 Number ->
414 mismatch
416 Appendable ->
417 mismatch
419 Comparable ->
420 do comparableOccursCheck context
421 merge context (Structure flatType)
422 unifyComparableRecursive a
423 unifyComparableRecursive b
424 case maybeC of
425 Nothing ->
426 return ()
428 Just c ->
429 unifyComparableRecursive c
431 CompAppend ->
432 mismatch
434 _ ->
435 mismatch
438-- TODO: is there some way to avoid doing this?
439-- Do type classes require occurs checks?
440comparableOccursCheck :: Context -> Unify ()
441comparableOccursCheck (Context _ _ var _) =
442 Unify $ \vars ok err ->
443 do hasOccurred <- Occurs.occurs var
444 if hasOccurred
445 then err vars ()
446 else ok vars ()
449unifyComparableRecursive :: Variable -> Unify ()
450unifyComparableRecursive var =
451 do compVar <- register $
452 do (Descriptor _ rank _ _) <- UF.get var
453 UF.fresh $ Descriptor (Type.unnamedFlexSuper Comparable) rank noMark Nothing
454 guardedUnify compVar var
458-- UNIFY ALIASES
461unifyAlias :: Context -> ModuleName.Canonical -> N.Name -> [(N.Name, Variable)] -> Variable -> Content -> Unify ()
462unifyAlias context home name args realVar otherContent =
463 case otherContent of
464 FlexVar _ ->
465 merge context (Alias home name args realVar)
467 FlexSuper _ _ ->
468 subUnify realVar (_second context)
470 RigidVar _ ->
471 subUnify realVar (_second context)
473 RigidSuper _ _ ->
474 subUnify realVar (_second context)
476 Alias otherHome otherName otherArgs otherRealVar ->
477 if name == otherName && home == otherHome then
478 Unify $ \vars ok err ->
479 let
480 ok1 vars1 () =
481 case merge context otherContent of
482 Unify k ->
483 k vars1 ok err
484 in
485 unifyAliasArgs vars context args otherArgs ok1 err
487 else
488 subUnify realVar otherRealVar
490 Structure _ ->
491 subUnify realVar (_second context)
493 Error _ ->
494 return ()
497unifyAliasArgs :: [Variable] -> Context -> [(N.Name,Variable)] -> [(N.Name,Variable)] -> ([Variable] -> () -> IO r) -> ([Variable] -> () -> IO r) -> IO r
498unifyAliasArgs vars context args1 args2 ok err =
499 case args1 of
500 (_,arg1):others1 ->
501 case args2 of
502 (_,arg2):others2 ->
503 case subUnify arg1 arg2 of
504 Unify k ->
505 k vars
506 (\vs () -> unifyAliasArgs vs context others1 others2 ok err)
507 (\vs () -> unifyAliasArgs vs context others1 others2 err err)
509 _ ->
510 err vars ()
512 [] ->
513 case args2 of
514 [] ->
515 ok vars ()
517 _ ->
518 err vars ()
522-- UNIFY STRUCTURES
525unifyStructure :: Context -> FlatType -> Content -> Content -> Unify ()
526unifyStructure context flatType content otherContent =
527 case otherContent of
528 FlexVar _ ->
529 merge context content
531 FlexSuper super _ ->
532 unifyFlexSuperStructure (reorient context) super flatType
534 RigidVar _ ->
535 mismatch
537 RigidSuper _ _ ->
538 mismatch
540 Alias _ _ _ realVar ->
541 subUnify (_first context) realVar
543 Structure otherFlatType ->
544 case (flatType, otherFlatType) of
545 (App1 home name args, App1 otherHome otherName otherArgs) | home == otherHome && name == otherName ->
546 Unify $ \vars ok err ->
547 let
548 ok1 vars1 () =
549 case merge context otherContent of
550 Unify k ->
551 k vars1 ok err
552 in
553 unifyArgs vars context args otherArgs ok1 err
555 (Fun1 arg1 res1, Fun1 arg2 res2) ->
556 do try2
557 (subUnify arg1 arg2)
558 (subUnify res1 res2)
559 merge context otherContent
561 (EmptyRecord1, EmptyRecord1) ->
562 merge context otherContent
564 (Record1 fields ext, EmptyRecord1) | Map.null fields ->
565 subUnify ext (_second context)
567 (EmptyRecord1, Record1 fields ext) | Map.null fields ->
568 subUnify (_first context) ext
570 (Record1 fields1 ext1, Record1 fields2 ext2) ->
571 Unify $ \vars ok err ->
572 do structure1 <- gatherFields fields1 ext1
573 structure2 <- gatherFields fields2 ext2
574 case unifyRecord context structure1 structure2 of
575 Unify k ->
576 k vars ok err
578 (Tuple1 a b Nothing, Tuple1 x y Nothing) ->
579 do try2
580 (subUnify a x)
581 (subUnify b y)
582 merge context otherContent
584 (Tuple1 a b (Just c), Tuple1 x y (Just z)) ->
585 do try3
586 (subUnify a x)
587 (subUnify b y)
588 (subUnify c z)
589 merge context otherContent
591 (Unit1, Unit1) ->
592 merge context otherContent
594 _ ->
595 mismatch
597 Error _ ->
598 return ()
602-- UNIFY ARGS
605unifyArgs :: [Variable] -> Context -> [Variable] -> [Variable] -> ([Variable] -> () -> IO r) -> ([Variable] -> () -> IO r) -> IO r
606unifyArgs vars context args1 args2 ok err =
607 case args1 of
608 arg1:others1 ->
609 case args2 of
610 arg2:others2 ->
611 case subUnify arg1 arg2 of
612 Unify k ->
613 k vars
614 (\vs () -> unifyArgs vs context others1 others2 ok err)
615 (\vs () -> unifyArgs vs context others1 others2 err err)
617 _ ->
618 err vars ()
620 [] ->
621 case args2 of
622 [] ->
623 ok vars ()
625 _ ->
626 err vars ()
630-- UNIFY RECORDS
633unifyRecord :: Context -> RecordStructure -> RecordStructure -> Unify ()
634unifyRecord context (RecordStructure fields1 ext1) (RecordStructure fields2 ext2) =
635 let
636 sharedFields = Map.intersectionWith (,) fields1 fields2
637 uniqueFields1 = Map.difference fields1 fields2
638 uniqueFields2 = Map.difference fields2 fields1
639 in
640 if Map.null uniqueFields1 then
642 if Map.null uniqueFields2 then
643 try2
644 (subUnify ext1 ext2)
645 (unifySharedFields context sharedFields Map.empty ext1)
647 else
648 do subRecord <- fresh context (Structure (Record1 uniqueFields2 ext2))
649 try2
650 (subUnify ext1 subRecord)
651 (unifySharedFields context sharedFields Map.empty subRecord)
653 else
655 if Map.null uniqueFields2 then
656 do subRecord <- fresh context (Structure (Record1 uniqueFields1 ext1))
657 try2
658 (subUnify subRecord ext2)
659 (unifySharedFields context sharedFields Map.empty subRecord)
661 else
662 do let otherFields = Map.union uniqueFields1 uniqueFields2
663 ext <- fresh context Type.unnamedFlexVar
664 sub1 <- fresh context (Structure (Record1 uniqueFields1 ext))
665 sub2 <- fresh context (Structure (Record1 uniqueFields2 ext))
666 try3
667 (subUnify ext1 sub2)
668 (subUnify sub1 ext2)
669 (unifySharedFields context sharedFields otherFields ext)
672unifySharedFields :: Context -> Map.Map N.Name (Variable, Variable) -> Map.Map N.Name Variable -> Variable -> Unify ()
673unifySharedFields context sharedFields otherFields ext =
674 do matchingFields <- Map.traverseMaybeWithKey unifyField sharedFields
675 if Map.size sharedFields == Map.size matchingFields
676 then merge context (Structure (Record1 (Map.union matchingFields otherFields) ext))
677 else mismatch
680unifyField :: N.Name -> (Variable, Variable) -> Unify (Maybe Variable)
681unifyField _ (actual, expected) =
682 Unify $ \vars ok _ ->
683 case subUnify actual expected of
684 Unify k ->
685 k vars
686 (\vs () -> ok vs (Just actual))
687 (\vs () -> ok vs Nothing)
691-- GATHER RECORD STRUCTURE
694data RecordStructure =
695 RecordStructure
696 { _fields :: Map.Map N.Name Variable
697 , _extension :: Variable
698 }
701gatherFields :: Map.Map N.Name Variable -> Variable -> IO RecordStructure
702gatherFields fields variable =
703 do (Descriptor content _ _ _) <- UF.get variable
704 case content of
705 Structure (Record1 subFields subExt) ->
706 gatherFields (Map.union fields subFields) subExt
708 Alias _ _ _ var ->
709 -- TODO may be dropping useful alias info here
710 gatherFields fields var
712 _ ->
713 return (RecordStructure fields variable)