git.iko.soy/elk
on 42f3721 help sign in
elk/compiler/src/Type/Unify.hs
693 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
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 ()
121-- UNIFICATION HELPERS
124data Context =
125 Context
126 { _first :: Variable
127 , _firstDesc :: Descriptor
128 , _second :: Variable
129 , _secondDesc :: Descriptor
130 }
133reorient :: Context -> Context
134reorient (Context var1 desc1 var2 desc2) =
135 Context var2 desc2 var1 desc1
139-- MERGE
142merge :: Context -> Content -> Unify ()
143merge (Context var1 (Descriptor _ rank1 _ _) var2 (Descriptor _ rank2 _ _)) content =
144 Unify $ \vars ok _ ->
145 ok vars =<<
146 UF.union var1 var2 (Descriptor content (min rank1 rank2) noMark Nothing)
149fresh :: Context -> Content -> Unify Variable
150fresh (Context _ (Descriptor _ rank1 _ _) _ (Descriptor _ rank2 _ _)) content =
151 register $ UF.fresh $
152 Descriptor content (min rank1 rank2) noMark Nothing
156-- ACTUALLY UNIFY THINGS
159guardedUnify :: Variable -> Variable -> Unify ()
160guardedUnify left right =
161 Unify $ \vars ok err ->
162 do equivalent <- UF.equivalent left right
163 if equivalent
164 then ok vars ()
165 else
166 do leftDesc <- UF.get left
167 rightDesc <- UF.get right
168 case actuallyUnify (Context left leftDesc right rightDesc) of
169 Unify k ->
170 k vars ok err
173subUnify :: Variable -> Variable -> Unify ()
174subUnify var1 var2 =
175 guardedUnify var1 var2
178actuallyUnify :: Context -> Unify ()
179actuallyUnify context@(Context _ (Descriptor firstContent _ _ _) _ (Descriptor secondContent _ _ _)) =
180 case firstContent of
181 FlexVar _ ->
182 unifyFlex context firstContent secondContent
184 FlexSuper super _ ->
185 unifyFlexSuper context super firstContent secondContent
187 RigidVar _ ->
188 unifyRigid context Nothing firstContent secondContent
190 RigidSuper super _ ->
191 unifyRigid context (Just super) firstContent secondContent
193 Alias home name args realVar ->
194 unifyAlias context home name args realVar secondContent
196 Structure flatType ->
197 unifyStructure context flatType firstContent secondContent
199 Error ->
200 -- If there was an error, just pretend it is okay. This lets us avoid
201 -- "cascading" errors where one problem manifests as multiple message.
202 merge context Error
206-- UNIFY FLEXIBLE VARIABLES
209unifyFlex :: Context -> Content -> Content -> Unify ()
210unifyFlex context content otherContent =
211 case otherContent of
212 Error ->
213 merge context Error
215 -- TODO see if wildcarding makes a noticable perf difference
217 FlexVar maybeName ->
218 merge context $
219 case maybeName of
220 Nothing ->
221 content
223 Just _ ->
224 otherContent
226 FlexSuper _ _ ->
227 merge context otherContent
229 RigidVar _ ->
230 merge context otherContent
232 RigidSuper _ _ ->
233 merge context otherContent
235 Alias _ _ _ _ ->
236 merge context otherContent
238 Structure _ ->
239 merge context otherContent
243-- UNIFY RIGID VARIABLES
246unifyRigid :: Context -> Maybe SuperType -> Content -> Content -> Unify ()
247unifyRigid context maybeSuper content otherContent =
248 case otherContent of
249 FlexVar _ ->
250 merge context content
252 FlexSuper otherSuper _ ->
253 case maybeSuper of
254 Just super ->
255 if combineRigidSupers super otherSuper then
256 merge context content
257 else
258 mismatch
260 Nothing ->
261 mismatch
263 RigidVar _ ->
264 mismatch
266 RigidSuper _ _ ->
267 mismatch
269 Alias _ _ _ _ ->
270 mismatch
272 Structure _ ->
273 mismatch
275 Error ->
276 merge context Error
280-- UNIFY SUPER VARIABLES
283unifyFlexSuper :: Context -> SuperType -> Content -> Content -> Unify ()
284unifyFlexSuper context super content otherContent =
285 case otherContent of
286 Structure flatType ->
287 unifyFlexSuperStructure context super flatType
289 RigidVar _ ->
290 mismatch
292 RigidSuper otherSuper _ ->
293 if combineRigidSupers otherSuper super then
294 merge context otherContent
295 else
296 mismatch
298 FlexVar _ ->
299 merge context content
301 FlexSuper otherSuper _ ->
302 case super of
303 Number ->
304 case otherSuper of
305 Number -> merge context content
306 Comparable -> merge context content
307 Appendable -> mismatch
308 CompAppend -> mismatch
310 Comparable ->
311 case otherSuper of
312 Comparable -> merge context otherContent
313 Number -> merge context otherContent
314 Appendable -> merge context (Type.unnamedFlexSuper CompAppend)
315 CompAppend -> merge context otherContent
317 Appendable ->
318 case otherSuper of
319 Appendable -> merge context otherContent
320 Comparable -> merge context (Type.unnamedFlexSuper CompAppend)
321 CompAppend -> merge context otherContent
322 Number -> mismatch
324 CompAppend ->
325 case otherSuper of
326 Comparable -> merge context content
327 Appendable -> merge context content
328 CompAppend -> merge context content
329 Number -> mismatch
331 Alias _ _ _ realVar ->
332 subUnify (_first context) realVar
334 Error ->
335 merge context Error
338combineRigidSupers :: SuperType -> SuperType -> Bool
339combineRigidSupers rigid flex =
340 rigid == flex
341 || (rigid == Number && flex == Comparable)
342 || (rigid == CompAppend && (flex == Comparable || flex == Appendable))
345atomMatchesSuper :: SuperType -> ModuleName.Canonical -> N.Name -> Bool
346atomMatchesSuper super home name =
347 case super of
348 Number ->
349 isNumber home name
351 Comparable ->
352 isNumber home name
353 || Error.isString home name
354 || Error.isChar home name
356 Appendable ->
357 Error.isString home name
359 CompAppend ->
360 Error.isString home name
363isNumber :: ModuleName.Canonical -> N.Name -> Bool
364isNumber home name =
365 home == ModuleName.basics
366 &&
367 (name == N.int || name == N.float)
370unifyFlexSuperStructure :: Context -> SuperType -> FlatType -> Unify ()
371unifyFlexSuperStructure context super flatType =
372 case flatType of
373 App1 home name [] ->
374 if atomMatchesSuper super home name then
375 merge context (Structure flatType)
376 else
377 mismatch
379 App1 home name [variable] | home == ModuleName.list && name == N.list ->
380 case super of
381 Number ->
382 mismatch
384 Appendable ->
385 merge context (Structure flatType)
387 Comparable ->
388 do comparableOccursCheck context
389 merge context (Structure flatType)
390 unifyComparableRecursive variable
392 CompAppend ->
393 do comparableOccursCheck context
394 merge context (Structure flatType)
395 unifyComparableRecursive variable
397 Tuple1 a b maybeC ->
398 case super of
399 Number ->
400 mismatch
402 Appendable ->
403 mismatch
405 Comparable ->
406 do comparableOccursCheck context
407 merge context (Structure flatType)
408 unifyComparableRecursive a
409 unifyComparableRecursive b
410 case maybeC of
411 Nothing ->
412 return ()
414 Just c ->
415 unifyComparableRecursive c
417 CompAppend ->
418 mismatch
420 _ ->
421 mismatch
424-- TODO: is there some way to avoid doing this?
425-- Do type classes require occurs checks?
426comparableOccursCheck :: Context -> Unify ()
427comparableOccursCheck (Context _ _ var _) =
428 Unify $ \vars ok err ->
429 do hasOccurred <- Occurs.occurs var
430 if hasOccurred
431 then err vars ()
432 else ok vars ()
435unifyComparableRecursive :: Variable -> Unify ()
436unifyComparableRecursive var =
437 do compVar <- register $
438 do (Descriptor _ rank _ _) <- UF.get var
439 UF.fresh $ Descriptor (Type.unnamedFlexSuper Comparable) rank noMark Nothing
440 guardedUnify compVar var
444-- UNIFY ALIASES
447unifyAlias :: Context -> ModuleName.Canonical -> N.Name -> [(N.Name, Variable)] -> Variable -> Content -> Unify ()
448unifyAlias context home name args realVar otherContent =
449 case otherContent of
450 FlexVar _ ->
451 merge context (Alias home name args realVar)
453 FlexSuper _ _ ->
454 subUnify realVar (_second context)
456 RigidVar _ ->
457 subUnify realVar (_second context)
459 RigidSuper _ _ ->
460 subUnify realVar (_second context)
462 Alias otherHome otherName otherArgs otherRealVar ->
463 if name == otherName && home == otherHome then
464 Unify $ \vars ok err ->
465 let
466 ok1 vars1 () =
467 case merge context otherContent of
468 Unify k ->
469 k vars1 ok err
470 in
471 unifyAliasArgs vars context args otherArgs ok1 err
473 else
474 subUnify realVar otherRealVar
476 Structure _ ->
477 subUnify realVar (_second context)
479 Error ->
480 merge context Error
483unifyAliasArgs :: [Variable] -> Context -> [(N.Name,Variable)] -> [(N.Name,Variable)] -> ([Variable] -> () -> IO r) -> ([Variable] -> () -> IO r) -> IO r
484unifyAliasArgs vars context args1 args2 ok err =
485 case args1 of
486 (_,arg1):others1 ->
487 case args2 of
488 (_,arg2):others2 ->
489 case subUnify arg1 arg2 of
490 Unify k ->
491 k vars
492 (\vs () -> unifyAliasArgs vs context others1 others2 ok err)
493 (\vs () -> unifyAliasArgs vs context others1 others2 err err)
495 _ ->
496 err vars ()
498 [] ->
499 case args2 of
500 [] ->
501 ok vars ()
503 _ ->
504 err vars ()
508-- UNIFY STRUCTURES
511unifyStructure :: Context -> FlatType -> Content -> Content -> Unify ()
512unifyStructure context flatType content otherContent =
513 case otherContent of
514 FlexVar _ ->
515 merge context content
517 FlexSuper super _ ->
518 unifyFlexSuperStructure (reorient context) super flatType
520 RigidVar _ ->
521 mismatch
523 RigidSuper _ _ ->
524 mismatch
526 Alias _ _ _ realVar ->
527 subUnify (_first context) realVar
529 Structure otherFlatType ->
530 case (flatType, otherFlatType) of
531 (App1 home name args, App1 otherHome otherName otherArgs) | home == otherHome && name == otherName ->
532 Unify $ \vars ok err ->
533 let
534 ok1 vars1 () =
535 case merge context otherContent of
536 Unify k ->
537 k vars1 ok err
538 in
539 unifyArgs vars context args otherArgs ok1 err
541 (Fun1 arg1 res1, Fun1 arg2 res2) ->
542 do subUnify arg1 arg2
543 subUnify res1 res2
544 merge context otherContent
546 (EmptyRecord1, EmptyRecord1) ->
547 merge context otherContent
549 (Record1 fields ext, EmptyRecord1) | Map.null fields ->
550 subUnify ext (_second context)
552 (EmptyRecord1, Record1 fields ext) | Map.null fields ->
553 subUnify (_first context) ext
555 (Record1 fields1 ext1, Record1 fields2 ext2) ->
556 Unify $ \vars ok err ->
557 do structure1 <- gatherFields fields1 ext1
558 structure2 <- gatherFields fields2 ext2
559 case unifyRecord context structure1 structure2 of
560 Unify k ->
561 k vars ok err
563 (Tuple1 a b Nothing, Tuple1 x y Nothing) ->
564 do subUnify a x
565 subUnify b y
566 merge context otherContent
568 (Tuple1 a b (Just c), Tuple1 x y (Just z)) ->
569 do subUnify a x
570 subUnify b y
571 subUnify c z
572 merge context otherContent
574 (Unit1, Unit1) ->
575 merge context otherContent
577 _ ->
578 mismatch
580 Error ->
581 merge context Error
585-- UNIFY ARGS
588unifyArgs :: [Variable] -> Context -> [Variable] -> [Variable] -> ([Variable] -> () -> IO r) -> ([Variable] -> () -> IO r) -> IO r
589unifyArgs vars context args1 args2 ok err =
590 case args1 of
591 arg1:others1 ->
592 case args2 of
593 arg2:others2 ->
594 case subUnify arg1 arg2 of
595 Unify k ->
596 k vars
597 (\vs () -> unifyArgs vs context others1 others2 ok err)
598 (\vs () -> unifyArgs vs context others1 others2 err err)
600 _ ->
601 err vars ()
603 [] ->
604 case args2 of
605 [] ->
606 ok vars ()
608 _ ->
609 err vars ()
613-- UNIFY RECORDS
616unifyRecord :: Context -> RecordStructure -> RecordStructure -> Unify ()
617unifyRecord context (RecordStructure fields1 ext1) (RecordStructure fields2 ext2) =
618 let
619 sharedFields = Map.intersectionWith (,) fields1 fields2
620 uniqueFields1 = Map.difference fields1 fields2
621 uniqueFields2 = Map.difference fields2 fields1
622 in
623 if Map.null uniqueFields1 then
625 if Map.null uniqueFields2 then
626 do subUnify ext1 ext2
627 unifySharedFields context sharedFields Map.empty ext1
629 else
630 do subRecord <- fresh context (Structure (Record1 uniqueFields2 ext2))
631 subUnify ext1 subRecord
632 unifySharedFields context sharedFields Map.empty subRecord
634 else
636 if Map.null uniqueFields2 then
637 do subRecord <- fresh context (Structure (Record1 uniqueFields1 ext1))
638 subUnify subRecord ext2
639 unifySharedFields context sharedFields Map.empty subRecord
641 else
642 do let otherFields = Map.union uniqueFields1 uniqueFields2
643 ext <- fresh context Type.unnamedFlexVar
644 sub1 <- fresh context (Structure (Record1 uniqueFields1 ext))
645 sub2 <- fresh context (Structure (Record1 uniqueFields2 ext))
646 subUnify ext1 sub2
647 subUnify sub1 ext2
648 unifySharedFields context sharedFields otherFields ext
651unifySharedFields :: Context -> Map.Map N.Name (Variable, Variable) -> Map.Map N.Name Variable -> Variable -> Unify ()
652unifySharedFields context sharedFields otherFields ext =
653 do matchingFields <- Map.traverseMaybeWithKey unifyField sharedFields
654 if Map.size sharedFields == Map.size matchingFields
655 then merge context (Structure (Record1 (Map.union matchingFields otherFields) ext))
656 else mismatch
659unifyField :: N.Name -> (Variable, Variable) -> Unify (Maybe Variable)
660unifyField _ (actual, expected) =
661 Unify $ \vars ok _ ->
662 case subUnify actual expected of
663 Unify k ->
664 k vars
665 (\vs () -> ok vs (Just actual))
666 (\vs () -> ok vs Nothing)
670-- GATHER RECORD STRUCTURE
673data RecordStructure =
674 RecordStructure
675 { _fields :: Map.Map N.Name Variable
676 , _extension :: Variable
677 }
680gatherFields :: Map.Map N.Name Variable -> Variable -> IO RecordStructure
681gatherFields fields variable =
682 do (Descriptor content _ _ _) <- UF.get variable
683 case content of
684 Structure (Record1 subFields subExt) ->
685 gatherFields (Map.union fields subFields) subExt
687 Alias _ _ _ var ->
688 -- TODO may be dropping useful alias info here
689 gatherFields fields var
691 _ ->
692 return (RecordStructure fields variable)