git.iko.soy/elk
on 2799bc0 help sign in
elk/src/Type/Unify.hs
828 lines 23 kB history raw
1{-# OPTIONS_GHC -Wall #-}
2{-# LANGUAGE OverloadedStrings, Rank2Types #-}
3module Type.Unify
4 ( Answer(..)
5 , unify
6 , Problem(..)
7 )
8 where
11import Control.Monad (foldM, liftM2, zipWithM_)
12import qualified Data.Map.Strict as Map
14import qualified AST.Canonical as Can
15import qualified AST.Module.Name as ModuleName
16import qualified Elm.Name as N
17import qualified Type.Occurs as Occurs
18import Type.Type as Type
19import qualified Type.UnionFind as UF
23-- UNIFY
26data Answer
27 = Ok [Variable]
28 | Err [Variable] Problem Can.Type Can.Type
31unify :: Variable -> Variable -> IO Answer
32unify v1 v2 =
33 case guardedUnify ActualExpected v1 v2 of
34 Unify k ->
35 k [] onSuccess $ \vars problem ->
36 do t1 <- Type.toSrcType v1
37 t2 <- Type.toSrcType v2
38 UF.union v1 v2 errorDescriptor
39 return (Err vars problem t1 t2)
43onSuccess :: [Variable] -> () -> IO Answer
44onSuccess vars () =
45 return (Ok vars)
48{-# NOINLINE errorDescriptor #-}
49errorDescriptor :: Descriptor
50errorDescriptor =
51 Descriptor (Error "?") noRank noMark Nothing
55-- PROBLEM
58data Reason
59 = BadFields [(N.Name, Maybe Reason)]
60 | MessyFields [N.Name] [N.Name] [N.Name]
61 | IntFloat
62 | MissingArgs Int
63 | RigidClash N.Name N.Name
64 | NotPartOfSuper Type.SuperType
65 | RigidVarTooGeneric N.Name SpecificThing
66 | RigidSuperTooGeneric Type.SuperType N.Name SpecificThing
69data SpecificThing
70 = SpecificSuper Type.SuperType
71 | SpecificType N.Name
72 | SpecificFunction
73 | SpecificRecord
74 | SpecificUnit
75 | SpecificTuple
78flipReason :: Reason -> Reason
79flipReason reason =
80 case reason of
81 BadFields fields ->
82 BadFields (map (fmap (fmap flipReason)) fields)
84 MessyFields both left right ->
85 MessyFields both right left
87 IntFloat ->
88 IntFloat
90 MissingArgs num ->
91 MissingArgs num
93 RigidClash a b ->
94 RigidClash b a
96 NotPartOfSuper super ->
97 NotPartOfSuper super
99 RigidVarTooGeneric name specific ->
100 RigidVarTooGeneric name specific
102 RigidSuperTooGeneric super name specific ->
103 RigidSuperTooGeneric super name specific
107-- CPS UNIFIER
110newtype Unify a =
111 Unify (forall r.
112 [Variable]
113 -> ([Variable] -> a -> IO r)
114 -> ([Variable] -> Problem -> IO r)
115 -> IO r
116 )
119-- TODO experiment with INLINE on the Unify instances
121instance Functor Unify where
122 fmap func (Unify kv) =
123 Unify $ \vars ok err ->
124 let
125 ok1 vars1 value =
126 ok vars1 (func value)
127 in
128 kv vars ok1 err
131instance Applicative Unify where
132 pure a =
133 Unify $ \vars ok _ ->
134 ok vars a
136 (<*>) (Unify kf) (Unify kv) =
137 Unify $ \vars ok err ->
138 let
139 ok1 vars1 func =
140 let
141 ok2 vars2 value =
142 ok vars2 (func value)
143 in
144 kv vars1 ok2 err
145 in
146 kf vars ok1 err
149instance Monad Unify where
150 return a =
151 Unify $ \vars ok _ ->
152 ok vars a
154 (>>=) (Unify ka) callback =
155 Unify $ \vars ok err ->
156 let
157 ok1 vars1 a =
158 case callback a of
159 Unify kb -> kb vars1 ok err
160 in
161 ka vars ok1 err
164register :: IO Variable -> Unify Variable
165register mkVar =
166 Unify $ \vars ok _ ->
167 do var <- mkVar
168 ok (var:vars) var
172-- UNIFICATION HELPERS
175data Context =
176 Context
177 { _orientation :: Orientation
178 , _first :: Variable
179 , _firstDesc :: Descriptor
180 , _second :: Variable
181 , _secondDesc :: Descriptor
182 }
185data Orientation
186 = ExpectedActual
187 | ActualExpected
190reorient :: Context -> Context
191reorient (Context orientation var1 desc1 var2 desc2) =
192 let
193 otherOrientation =
194 case orientation of
195 ExpectedActual -> ActualExpected
196 ActualExpected -> ExpectedActual
197 in
198 Context otherOrientation var2 desc2 var1 desc1
202-- ERROR MESSAGES
205data Problem
206 = Reason Bool (Maybe Reason)
207 | Infinite
210mismatch :: Context -> Maybe Reason -> Unify a
211mismatch context@(Context orientation var1 _ var2 _) maybeReason =
212 Unify $ \vars _ err ->
213 do anyInfinite <- liftM2 (||) (Occurs.occurs var1) (Occurs.occurs var2)
214 if anyInfinite
215 then err vars Infinite
216 else
217 do args1 <- collectArgs [] var1
218 args2 <- collectArgs [] var2
220 hasDecoder <-
221 or <$> traverse detectDecoder (args1 ++ args2)
223 if length args1 /= length args2
224 then
225 do newVars <- foldM (subUnifyAnyway context) vars (zip args1 args2)
226 err newVars $ Reason hasDecoder $ Just $
227 MissingArgs (abs (length args2 - length args1))
228 else
229 err vars $ Reason hasDecoder $
230 case orientation of
231 ExpectedActual ->
232 maybeReason
234 ActualExpected ->
235 fmap flipReason maybeReason
238subUnifyAnyway :: Context -> [Variable] -> (Variable, Variable) -> IO [Variable]
239subUnifyAnyway context vars (arg1, arg2) =
240 case subUnify context arg1 arg2 of
241 Unify k ->
242 k vars (\vs _ -> return vs) (\vs _ -> return vs)
245collectArgs :: [Variable] -> Variable -> IO [Variable]
246collectArgs revArgs variable =
247 do (Descriptor content _ _ _) <- UF.get variable
248 case content of
249 Structure (Fun1 arg returnType) ->
250 collectArgs (arg : revArgs) returnType
252 _ ->
253 return $ variable : revArgs
256detectDecoder :: Variable -> IO Bool
257detectDecoder variable =
258 do (Descriptor content _ _ _) <- UF.get variable
259 case content of
260 Structure (App1 home name [_]) ->
261 return (home == ModuleName.jsonDecode && name == "Decoder")
263 _ ->
264 return False
268-- MERGE
271merge :: Context -> Content -> Unify ()
272merge (Context _ var1 (Descriptor _ rank1 _ _) var2 (Descriptor _ rank2 _ _)) content =
273 Unify $ \vars ok _ ->
274 ok vars =<<
275 UF.union var1 var2 (Descriptor content (min rank1 rank2) noMark Nothing)
278fresh :: Context -> Content -> Unify Variable
279fresh (Context _ _ (Descriptor _ rank1 _ _) _ (Descriptor _ rank2 _ _)) content =
280 register $ UF.fresh $
281 Descriptor content (min rank1 rank2) noMark Nothing
285-- ACTUALLY UNIFY THINGS
288guardedUnify :: Orientation -> Variable -> Variable -> Unify ()
289guardedUnify orientation left right =
290 Unify $ \vars ok err ->
291 do equivalent <- UF.equivalent left right
292 if equivalent
293 then ok vars ()
294 else
295 do leftDesc <- UF.get left
296 rightDesc <- UF.get right
297 case actuallyUnify (Context orientation left leftDesc right rightDesc) of
298 Unify k ->
299 k vars ok err
302subUnify :: Context -> Variable -> Variable -> Unify ()
303subUnify context var1 var2 =
304 guardedUnify (_orientation context) var1 var2
307actuallyUnify :: Context -> Unify ()
308actuallyUnify context@(Context _ _ (Descriptor firstContent _ _ _) _ (Descriptor secondContent _ _ _)) =
309 case firstContent of
310 FlexVar _ ->
311 unifyFlex context firstContent secondContent
313 FlexSuper super _ ->
314 unifyFlexSuper context super firstContent secondContent
316 RigidVar name ->
317 unifyRigid context Nothing name firstContent secondContent
319 RigidSuper super name ->
320 unifyRigid context (Just super) name firstContent secondContent
322 Alias home name args realVar ->
323 unifyAlias context home name args realVar secondContent
325 Structure flatType ->
326 unifyStructure context flatType firstContent secondContent
328 Error _ ->
329 -- If there was an error, just pretend it is okay. This lets us avoid
330 -- "cascading" errors where one problem manifests as multiple message.
331 return ()
335-- UNIFY FLEXIBLE VARIABLES
338unifyFlex :: Context -> Content -> Content -> Unify ()
339unifyFlex context content otherContent =
340 case otherContent of
341 Error _ ->
342 return ()
344 -- TODO see if wildcarding makes a noticable perf difference
346 FlexVar maybeName ->
347 merge context $
348 case maybeName of
349 Nothing ->
350 content
352 Just _ ->
353 otherContent
355 FlexSuper _ _ ->
356 merge context otherContent
358 RigidVar _ ->
359 merge context otherContent
361 RigidSuper _ _ ->
362 merge context otherContent
364 Alias _ _ _ _ ->
365 merge context otherContent
367 Structure _ ->
368 merge context otherContent
372-- UNIFY RIGID VARIABLES
375unifyRigid :: Context -> Maybe SuperType -> N.Name -> Content -> Content -> Unify ()
376unifyRigid context maybeSuper name content otherContent =
377 case otherContent of
378 FlexVar _ ->
379 merge context content
381 FlexSuper otherSuper _ ->
382 case maybeSuper of
383 Just super ->
384 if combineRigidSupers super otherSuper then
385 merge context content
386 else
387 mismatch context $ Just $
388 RigidSuperTooGeneric super name $ SpecificSuper otherSuper
390 Nothing ->
391 mismatch context $ Just $
392 RigidVarTooGeneric name $ SpecificSuper otherSuper
394 RigidVar otherName ->
395 mismatch context $ Just $
396 RigidClash name otherName
398 RigidSuper _ otherName ->
399 mismatch context $ Just $
400 RigidClash name otherName
402 Alias _ otherName _ _ ->
403 mismatch context $ Just $
404 maybe RigidVarTooGeneric RigidSuperTooGeneric maybeSuper name $
405 SpecificType otherName
407 Structure flatType ->
408 mismatch context $ Just $
409 maybe RigidVarTooGeneric RigidSuperTooGeneric maybeSuper name $
410 flatTypeToSpecificThing flatType
412 Error _ ->
413 return ()
416flatTypeToSpecificThing :: FlatType -> SpecificThing
417flatTypeToSpecificThing flatType =
418 case flatType of
419 App1 _ name _ ->
420 SpecificType name
422 Fun1 _ _ ->
423 SpecificFunction
425 EmptyRecord1 ->
426 SpecificRecord
428 Record1 _ _ ->
429 SpecificRecord
431 Unit1 ->
432 SpecificUnit
434 Tuple1 _ _ _ ->
435 SpecificTuple
439-- UNIFY SUPER VARIABLES
442unifyFlexSuper :: Context -> SuperType -> Content -> Content -> Unify ()
443unifyFlexSuper context super content otherContent =
444 case otherContent of
445 Structure flatType ->
446 unifyFlexSuperStructure context super flatType
448 RigidVar name ->
449 mismatch context $ Just $
450 RigidVarTooGeneric name (SpecificSuper super)
452 RigidSuper otherSuper name ->
453 if combineRigidSupers otherSuper super then
454 merge context otherContent
455 else
456 mismatch context $ Just $
457 RigidSuperTooGeneric otherSuper name (SpecificSuper super)
459 FlexVar _ ->
460 merge context content
462 FlexSuper otherSuper _ ->
463 case super of
464 Number ->
465 case otherSuper of
466 Number -> merge context content
467 Comparable -> merge context content
468 _ -> mismatch context Nothing -- NumberAppendableClash
470 Comparable ->
471 case otherSuper of
472 Comparable -> merge context otherContent
473 Number -> merge context otherContent
474 Appendable -> merge context (Type.unnamedFlexSuper CompAppend)
475 CompAppend -> merge context otherContent
477 Appendable ->
478 case otherSuper of
479 Appendable -> merge context otherContent
480 Comparable -> merge context (Type.unnamedFlexSuper CompAppend)
481 CompAppend -> merge context otherContent
482 Number -> mismatch context Nothing -- NumberAppendableClash
484 CompAppend ->
485 case otherSuper of
486 Comparable -> merge context content
487 Appendable -> merge context content
488 CompAppend -> merge context content
489 Number -> mismatch context Nothing -- NumberAppendableClash
491 Alias _ _ _ realVar ->
492 subUnify context (_first context) realVar
494 Error _ ->
495 return ()
498combineRigidSupers :: SuperType -> SuperType -> Bool
499combineRigidSupers rigid flex =
500 rigid == flex
501 || (rigid == Number && flex == Comparable)
502 || (rigid == CompAppend && (flex == Comparable || flex == Appendable))
505atomMatchesSuper :: SuperType -> ModuleName.Canonical -> N.Name -> Bool
506atomMatchesSuper super home name =
507 home == ModuleName.basics
508 &&
509 case super of
510 Number ->
511 name == N.int
512 || name == N.float
514 Comparable ->
515 name == N.int
516 || name == N.float
517 || name == N.string
518 || name == N.char
520 Appendable ->
521 name == N.string
523 CompAppend ->
524 name == N.string
527unifyFlexSuperStructure :: Context -> SuperType -> FlatType -> Unify ()
528unifyFlexSuperStructure context super flatType =
529 case flatType of
530 App1 home name [] ->
531 if atomMatchesSuper super home name then
532 merge context (Structure flatType)
533 else
534 mismatch context $ Just $ NotPartOfSuper super
536 App1 home name [variable] | home == ModuleName.list && name == N.list ->
537 case super of
538 Number ->
539 mismatch context $ Just $ NotPartOfSuper super
541 Appendable ->
542 merge context (Structure flatType)
544 Comparable ->
545 do comparableOccursCheck context
546 merge context (Structure flatType)
547 unifyComparableRecursive (_orientation context) variable
549 CompAppend ->
550 do comparableOccursCheck context
551 merge context (Structure flatType)
552 unifyComparableRecursive (_orientation context) variable
554 Tuple1 a b maybeC ->
555 case super of
556 Number ->
557 mismatch context $ Just $ NotPartOfSuper super
559 Appendable ->
560 mismatch context $ Just $ NotPartOfSuper super
562 Comparable ->
563 do comparableOccursCheck context
564 merge context (Structure flatType)
565 let orientation = _orientation context
566 unifyComparableRecursive orientation a
567 unifyComparableRecursive orientation b
568 case maybeC of
569 Nothing ->
570 return ()
572 Just c ->
573 unifyComparableRecursive orientation c
575 CompAppend ->
576 mismatch context $ Just $ NotPartOfSuper super
578 _ ->
579 mismatch context $ Just $ NotPartOfSuper super
582-- TODO: is there some way to avoid doing this?
583-- Do type classes require occurs checks?
584comparableOccursCheck :: Context -> Unify ()
585comparableOccursCheck (Context _ _ _ var _) =
586 Unify $ \vars ok err ->
587 do hasOccurred <- Occurs.occurs var
588 if hasOccurred
589 then err vars Infinite
590 else ok vars ()
593unifyComparableRecursive :: Orientation -> Variable -> Unify ()
594unifyComparableRecursive orientation var =
595 do compVar <- register $
596 do (Descriptor _ rank _ _) <- UF.get var
597 UF.fresh $ Descriptor (Type.unnamedFlexSuper Comparable) rank noMark Nothing
598 guardedUnify orientation compVar var
602-- UNIFY ALIASES
605unifyAlias :: Context -> ModuleName.Canonical -> N.Name -> [(N.Name, Variable)] -> Variable -> Content -> Unify ()
606unifyAlias context home name args realVar otherContent =
607 case otherContent of
608 FlexVar _ ->
609 merge context (Alias home name args realVar)
611 FlexSuper _ _ ->
612 subUnify context realVar (_second context)
614 RigidVar _ ->
615 subUnify context realVar (_second context)
617 RigidSuper _ _ ->
618 subUnify context realVar (_second context)
620 Alias otherHome otherName otherArgs otherRealVar ->
621 if name == otherName && home == otherHome then
622 do zipWithM_ (subUnify context) (map snd args) (map snd otherArgs)
623 merge context otherContent
625 else
626 subUnify context realVar otherRealVar
628 Structure _ ->
629 subUnify context realVar (_second context)
631 Error _ ->
632 return ()
636-- UNIFY STRUCTURES
639unifyStructure :: Context -> FlatType -> Content -> Content -> Unify ()
640unifyStructure context flatType content otherContent =
641 case otherContent of
642 FlexVar _ ->
643 merge context content
645 FlexSuper super _ ->
646 unifyFlexSuperStructure (reorient context) super flatType
648 RigidVar name ->
649 mismatch context $ Just $ RigidVarTooGeneric name (flatTypeToSpecificThing flatType)
651 RigidSuper super name ->
652 mismatch context $ Just $ RigidSuperTooGeneric super name (flatTypeToSpecificThing flatType)
654 Alias _ _ _ realVar ->
655 subUnify context (_first context) realVar
657 Structure otherTerm ->
658 case (flatType, otherTerm) of
659 (App1 home name args, App1 otherHome otherName otherArgs) ->
660 if home == otherHome && name == otherName then
661 do zipWithM_ (subUnify context) args otherArgs
662 merge context otherContent
664 else if isIntFloat home name otherHome otherName then
665 mismatch context (Just IntFloat)
667 else
668 mismatch context Nothing
670 (Fun1 arg result, Fun1 otherArg otherResult) ->
671 do subUnify context arg otherArg
672 subUnify context result otherResult
673 merge context otherContent
675 (EmptyRecord1, EmptyRecord1) ->
676 merge context otherContent
678 (Record1 fields ext, EmptyRecord1) | Map.null fields ->
679 subUnify context ext (_second context)
681 (EmptyRecord1, Record1 fields ext) | Map.null fields ->
682 subUnify context (_first context) ext
684 (Record1 fields extension, Record1 otherFields otherExtension) ->
685 Unify $ \vars ok err ->
686 do firstStructure <- gatherFields context fields extension
687 secondStructure <- gatherFields context otherFields otherExtension
688 case unifyRecord context firstStructure secondStructure of
689 Unify k ->
690 k vars ok err
692 _ ->
693 mismatch context Nothing
695 Error _ ->
696 return ()
700isIntFloat :: ModuleName.Canonical -> N.Name -> ModuleName.Canonical -> N.Name -> Bool
701isIntFloat home name otherHome otherName =
702 otherHome == ModuleName.basics
703 && home == ModuleName.basics
704 && (
705 (name == N.int && otherName == N.float)
706 ||
707 (name == N.float && otherName == N.int)
708 )
712-- UNIFY RECORDS
715unifyRecord :: Context -> RecordStructure -> RecordStructure -> Unify ()
716unifyRecord context firstStructure secondStructure =
717 do let (RecordStructure expFields expVar expStruct) = firstStructure
718 let (RecordStructure actFields actVar actStruct) = secondStructure
720 let sharedFields = Map.intersectionWith (,) expFields actFields
722 -- call after unifying extension, make sure record shape matches before
723 -- looking into whether the particular field types match.
724 let unifySharedFields otherFields ext =
725 do unifySharedFieldsHelp context sharedFields
726 let allFields = Map.union (Map.map fst sharedFields) otherFields
727 merge context (Structure (Record1 allFields ext))
729 let uniqueExpFields = Map.difference expFields actFields
730 let uniqueActFields = Map.difference actFields expFields
732 case (expStruct, Map.null uniqueExpFields, actStruct, Map.null uniqueActFields) of
733 (_, True, _, True) ->
734 do subUnify context expVar actVar
735 unifySharedFields Map.empty expVar
737 (Empty, _, _, False) ->
738 mismatch context $ Just $
739 MessyFields (Map.keys sharedFields) (Map.keys uniqueExpFields) (Map.keys uniqueActFields)
741 (_, False, Empty, _) ->
742 mismatch context $ Just $
743 MessyFields (Map.keys sharedFields) (Map.keys uniqueExpFields) (Map.keys uniqueActFields)
745 (_, False, _, True) ->
746 do subRecord <- fresh context (Structure (Record1 uniqueExpFields expVar))
747 subUnify context subRecord actVar
748 unifySharedFields Map.empty subRecord
750 (_, True, _, False) ->
751 do subRecord <- fresh context (Structure (Record1 uniqueActFields actVar))
752 subUnify context expVar subRecord
753 unifySharedFields Map.empty subRecord
755 (Extension, False, Extension, False) ->
756 do let subFields = Map.union uniqueExpFields uniqueActFields
757 subExt <- fresh context Type.unnamedFlexVar
758 expRecord <- fresh context (Structure (Record1 uniqueActFields subExt))
759 actRecord <- fresh context (Structure (Record1 uniqueExpFields subExt))
760 subUnify context expVar expRecord
761 subUnify context actRecord actVar
762 unifySharedFields subFields subExt
766unifySharedFieldsHelp :: Context -> Map.Map N.Name (Variable, Variable) -> Unify ()
767unifySharedFieldsHelp context sharedFields =
768 do badFields <- Map.traverseMaybeWithKey (unifyField context) sharedFields
769 case Map.toList badFields of
770 [] ->
771 return ()
773 badFieldPairs ->
774 mismatch context (Just (BadFields badFieldPairs))
777unifyField :: Context -> N.Name -> (Variable, Variable) -> Unify (Maybe (Maybe Reason))
778unifyField context _ (actual, expected) =
779 Unify $ \vars ok _ ->
780 case subUnify context actual expected of
781 Unify k ->
782 k vars
783 (\vs () -> ok vs Nothing)
784 (\vs problem ->
785 ok vs $ Just $
786 case problem of
787 Reason _ reason ->
788 reason
790 Infinite ->
791 Nothing
792 )
796-- GATHER RECORD STRUCTURE
799data RecordStructure =
800 RecordStructure
801 { _fields :: Map.Map N.Name Variable
802 , _extVar :: Variable
803 , _extStruct :: ExtensionStructure
804 }
807data ExtensionStructure
808 = Empty
809 | Extension
812gatherFields :: Context -> Map.Map N.Name Variable -> Variable -> IO RecordStructure
813gatherFields context fields variable =
814 do (Descriptor content _ _ _) <- UF.get variable
815 case content of
816 Structure (Record1 subFields subExt) ->
817 gatherFields context (Map.union fields subFields) subExt
819 Structure EmptyRecord1 ->
820 return (RecordStructure fields variable Empty)
822 Alias _ _ _ var ->
823 -- TODO may be dropping useful alias info here
824 gatherFields context fields var
826 _ ->
827 return (RecordStructure fields variable Extension)