git.iko.soy/elk
on 2deedfb help sign in
elk/src/Type/Unify.hs
848 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)
42onSuccess :: [Variable] -> () -> IO Answer
43onSuccess vars () =
44 return (Ok vars)
47{-# NOINLINE errorDescriptor #-}
48errorDescriptor :: Descriptor
49errorDescriptor =
50 Descriptor (Error "?") noRank noMark Nothing
54-- PROBLEM
57data Reason
58 = BadFields [(N.Name, Maybe Reason)]
59 | MessyFields [N.Name] [N.Name] [N.Name]
60 | IntFloat
61 | MissingArgs Int
62 | RigidClash N.Name N.Name
63 | NotPartOfSuper Type.SuperType
64 | RigidVarTooGeneric N.Name SpecificThing
65 | RigidSuperTooGeneric Type.SuperType N.Name SpecificThing
68data SpecificThing
69 = SpecificSuper Type.SuperType
70 | SpecificType N.Name
71 | SpecificFunction
72 | SpecificRecord
73 | SpecificUnit
74 | SpecificTuple
77flipReason :: Reason -> Reason
78flipReason reason =
79 case reason of
80 BadFields fields ->
81 BadFields (map (fmap (fmap flipReason)) fields)
83 MessyFields both left right ->
84 MessyFields both right left
86 IntFloat ->
87 IntFloat
89 MissingArgs num ->
90 MissingArgs num
92 RigidClash a b ->
93 RigidClash b a
95 NotPartOfSuper super ->
96 NotPartOfSuper super
98 RigidVarTooGeneric name specific ->
99 RigidVarTooGeneric name specific
101 RigidSuperTooGeneric super name specific ->
102 RigidSuperTooGeneric super name specific
106-- CPS UNIFIER
109newtype Unify a =
110 Unify (forall r.
111 [Variable]
112 -> ([Variable] -> a -> IO r)
113 -> ([Variable] -> Problem -> IO r)
114 -> IO r
115 )
118-- TODO experiment with INLINE on the Unify instances
120instance Functor Unify where
121 fmap func (Unify kv) =
122 Unify $ \vars ok err ->
123 let
124 ok1 vars1 value =
125 ok vars1 (func value)
126 in
127 kv vars ok1 err
130instance Applicative Unify where
131 pure a =
132 Unify $ \vars ok _ ->
133 ok vars a
135 (<*>) (Unify kf) (Unify kv) =
136 Unify $ \vars ok err ->
137 let
138 ok1 vars1 func =
139 let
140 ok2 vars2 value =
141 ok vars2 (func value)
142 in
143 kv vars1 ok2 err
144 in
145 kf vars ok1 err
148instance Monad Unify where
149 return a =
150 Unify $ \vars ok _ ->
151 ok vars a
153 (>>=) (Unify ka) callback =
154 Unify $ \vars ok err ->
155 let
156 ok1 vars1 a =
157 case callback a of
158 Unify kb -> kb vars1 ok err
159 in
160 ka vars ok1 err
163register :: IO Variable -> Unify Variable
164register mkVar =
165 Unify $ \vars ok _ ->
166 do var <- mkVar
167 ok (var:vars) var
171-- UNIFICATION HELPERS
174data Context =
175 Context
176 { _orientation :: Orientation
177 , _first :: Variable
178 , _firstDesc :: Descriptor
179 , _second :: Variable
180 , _secondDesc :: Descriptor
181 }
184data Orientation
185 = ExpectedActual
186 | ActualExpected
189reorient :: Context -> Context
190reorient (Context orientation var1 desc1 var2 desc2) =
191 let
192 otherOrientation =
193 case orientation of
194 ExpectedActual -> ActualExpected
195 ActualExpected -> ExpectedActual
196 in
197 Context otherOrientation var2 desc2 var1 desc1
201-- ERROR MESSAGES
204data Problem
205 = Reason Bool (Maybe Reason)
206 | Infinite
209mismatch :: Context -> Maybe Reason -> Unify a
210mismatch context@(Context orientation var1 _ var2 _) maybeReason =
211 Unify $ \vars _ err ->
212 do anyInfinite <- liftM2 (||) (Occurs.occurs var1) (Occurs.occurs var2)
213 if anyInfinite
214 then err vars Infinite
215 else
216 do args1 <- collectArgs [] var1
217 args2 <- collectArgs [] var2
219 hasDecoder <-
220 or <$> traverse detectDecoder (args1 ++ args2)
222 if length args1 /= length args2
223 then
224 do newVars <- foldM (subUnifyAnyway context) vars (zip args1 args2)
225 err newVars $ Reason hasDecoder $ Just $
226 MissingArgs (abs (length args2 - length args1))
227 else
228 err vars $ Reason hasDecoder $
229 case orientation of
230 ExpectedActual ->
231 maybeReason
233 ActualExpected ->
234 fmap flipReason maybeReason
237subUnifyAnyway :: Context -> [Variable] -> (Variable, Variable) -> IO [Variable]
238subUnifyAnyway context vars (arg1, arg2) =
239 case subUnify context arg1 arg2 of
240 Unify k ->
241 k vars (\vs _ -> return vs) (\vs _ -> return vs)
244collectArgs :: [Variable] -> Variable -> IO [Variable]
245collectArgs revArgs variable =
246 do (Descriptor content _ _ _) <- UF.get variable
247 case content of
248 Structure (Fun1 arg returnType) ->
249 collectArgs (arg : revArgs) returnType
251 _ ->
252 return $ variable : revArgs
255detectDecoder :: Variable -> IO Bool
256detectDecoder variable =
257 do (Descriptor content _ _ _) <- UF.get variable
258 case content of
259 Structure (App1 home name [_]) ->
260 return (home == ModuleName.jsonDecode && name == "Decoder")
262 _ ->
263 return False
267-- MERGE
270merge :: Context -> Content -> Unify ()
271merge (Context _ var1 (Descriptor _ rank1 _ _) var2 (Descriptor _ rank2 _ _)) content =
272 Unify $ \vars ok _ ->
273 ok vars =<<
274 UF.union var1 var2 (Descriptor content (min rank1 rank2) noMark Nothing)
277fresh :: Context -> Content -> Unify Variable
278fresh (Context _ _ (Descriptor _ rank1 _ _) _ (Descriptor _ rank2 _ _)) content =
279 register $ UF.fresh $
280 Descriptor content (min rank1 rank2) noMark Nothing
284-- ACTUALLY UNIFY THINGS
287guardedUnify :: Orientation -> Variable -> Variable -> Unify ()
288guardedUnify orientation left right =
289 Unify $ \vars ok err ->
290 do equivalent <- UF.equivalent left right
291 if equivalent
292 then ok vars ()
293 else
294 do leftDesc <- UF.get left
295 rightDesc <- UF.get right
296 putStrLn (toString leftDesc ++ " vs " ++ toString rightDesc)
297 case actuallyUnify (Context orientation left leftDesc right rightDesc) of
298 Unify k ->
299 k vars ok err
302toString :: Descriptor -> String
303toString (Descriptor content _ _ _) =
304 case content of
305 FlexVar _ -> "FlexVar"
306 FlexSuper _ _ -> "FlexSuper"
307 RigidVar _ -> "RigidVar"
308 RigidSuper _ _ -> "RigidSuper"
309 Alias _ _ _ _ -> "Alias"
310 Structure _ -> "Structure"
311 Error _ -> "Error"
314subUnify :: Context -> Variable -> Variable -> Unify ()
315subUnify context var1 var2 =
316 guardedUnify (_orientation context) var1 var2
319actuallyUnify :: Context -> Unify ()
320actuallyUnify context@(Context _ _ (Descriptor firstContent _ _ _) _ (Descriptor secondContent _ _ _)) =
321 case firstContent of
322 FlexVar _ ->
323 unifyFlex context firstContent secondContent
325 FlexSuper super _ ->
326 unifyFlexSuper context super firstContent secondContent
328 RigidVar name ->
329 unifyRigid context Nothing name firstContent secondContent
331 RigidSuper super name ->
332 unifyRigid context (Just super) name firstContent secondContent
334 Alias home name args realVar ->
335 unifyAlias context home name args realVar secondContent
337 Structure flatType ->
338 unifyStructure context flatType firstContent secondContent
340 Error _ ->
341 -- If there was an error, just pretend it is okay. This lets us avoid
342 -- "cascading" errors where one problem manifests as multiple message.
343 return ()
347-- UNIFY FLEXIBLE VARIABLES
350unifyFlex :: Context -> Content -> Content -> Unify ()
351unifyFlex context content otherContent =
352 case otherContent of
353 Error _ ->
354 return ()
356 -- TODO see if wildcarding makes a noticable perf difference
358 FlexVar maybeName ->
359 merge context $
360 case maybeName of
361 Nothing ->
362 content
364 Just _ ->
365 otherContent
367 FlexSuper _ _ ->
368 merge context otherContent
370 RigidVar _ ->
371 merge context otherContent
373 RigidSuper _ _ ->
374 merge context otherContent
376 Alias _ _ _ _ ->
377 merge context otherContent
379 Structure _ ->
380 merge context otherContent
384-- UNIFY RIGID VARIABLES
387unifyRigid :: Context -> Maybe SuperType -> N.Name -> Content -> Content -> Unify ()
388unifyRigid context maybeSuper name content otherContent =
389 case otherContent of
390 FlexVar _ ->
391 merge context content
393 FlexSuper otherSuper _ ->
394 case maybeSuper of
395 Just super ->
396 if combineRigidSupers super otherSuper then
397 merge context content
398 else
399 mismatch context $ Just $
400 RigidSuperTooGeneric super name $ SpecificSuper otherSuper
402 Nothing ->
403 mismatch context $ Just $
404 RigidVarTooGeneric name $ SpecificSuper otherSuper
406 RigidVar otherName ->
407 mismatch context $ Just $
408 RigidClash name otherName
410 RigidSuper _ otherName ->
411 mismatch context $ Just $
412 RigidClash name otherName
414 Alias _ otherName _ _ ->
415 mismatch context $ Just $
416 maybe RigidVarTooGeneric RigidSuperTooGeneric maybeSuper name $
417 SpecificType otherName
419 Structure flatType ->
420 mismatch context $ Just $
421 maybe RigidVarTooGeneric RigidSuperTooGeneric maybeSuper name $
422 flatTypeToSpecificThing flatType
424 Error _ ->
425 return ()
428flatTypeToSpecificThing :: FlatType -> SpecificThing
429flatTypeToSpecificThing flatType =
430 case flatType of
431 App1 _ name _ ->
432 SpecificType name
434 Fun1 _ _ ->
435 SpecificFunction
437 EmptyRecord1 ->
438 SpecificRecord
440 Record1 _ _ ->
441 SpecificRecord
443 Unit1 ->
444 SpecificUnit
446 Tuple1 _ _ _ ->
447 SpecificTuple
451-- UNIFY SUPER VARIABLES
454unifyFlexSuper :: Context -> SuperType -> Content -> Content -> Unify ()
455unifyFlexSuper context super content otherContent =
456 case otherContent of
457 Structure flatType ->
458 unifyFlexSuperStructure context super flatType
460 RigidVar name ->
461 mismatch context $ Just $
462 RigidVarTooGeneric name (SpecificSuper super)
464 RigidSuper otherSuper name ->
465 if combineRigidSupers otherSuper super then
466 merge context otherContent
467 else
468 mismatch context $ Just $
469 RigidSuperTooGeneric otherSuper name (SpecificSuper super)
471 FlexVar _ ->
472 merge context content
474 FlexSuper otherSuper _ ->
475 case super of
476 Number ->
477 case otherSuper of
478 Number -> merge context content
479 Comparable -> merge context content
480 _ -> mismatch context Nothing -- NumberAppendableClash
482 Comparable ->
483 case otherSuper of
484 Comparable -> merge context otherContent
485 Number -> merge context otherContent
486 Appendable -> merge context (Type.unnamedFlexSuper CompAppend)
487 CompAppend -> merge context otherContent
489 Appendable ->
490 case otherSuper of
491 Appendable -> merge context otherContent
492 Comparable -> merge context (Type.unnamedFlexSuper CompAppend)
493 CompAppend -> merge context otherContent
494 Number -> mismatch context Nothing -- NumberAppendableClash
496 CompAppend ->
497 case otherSuper of
498 Comparable -> merge context content
499 Appendable -> merge context content
500 CompAppend -> merge context content
501 Number -> mismatch context Nothing -- NumberAppendableClash
503 Alias _ _ _ realVar ->
504 subUnify context (_first context) realVar
506 Error _ ->
507 return ()
510combineRigidSupers :: SuperType -> SuperType -> Bool
511combineRigidSupers rigid flex =
512 rigid == flex
513 || (rigid == Number && flex == Comparable)
514 || (rigid == CompAppend && (flex == Comparable || flex == Appendable))
517atomMatchesSuper :: SuperType -> ModuleName.Canonical -> N.Name -> Bool
518atomMatchesSuper super home name =
519 home == ModuleName.basics
520 &&
521 case super of
522 Number ->
523 name == N.int
524 || name == N.float
526 Comparable ->
527 name == N.int
528 || name == N.float
529 || name == N.string
530 || name == N.char
532 Appendable ->
533 name == N.string
535 CompAppend ->
536 name == N.string
539unifyFlexSuperStructure :: Context -> SuperType -> FlatType -> Unify ()
540unifyFlexSuperStructure context super flatType =
541 case flatType of
542 App1 home name [] ->
543 if atomMatchesSuper super home name then
544 merge context (Structure flatType)
545 else
546 mismatch context $ Just $ NotPartOfSuper super
548 App1 home name [variable] | home == ModuleName.list && name == N.list ->
549 case super of
550 Number ->
551 mismatch context $ Just $ NotPartOfSuper super
553 Appendable ->
554 merge context (Structure flatType)
556 Comparable ->
557 do comparableOccursCheck context
558 merge context (Structure flatType)
559 unifyComparableRecursive (_orientation context) variable
561 CompAppend ->
562 do comparableOccursCheck context
563 merge context (Structure flatType)
564 unifyComparableRecursive (_orientation context) variable
566 Tuple1 a b maybeC ->
567 case super of
568 Number ->
569 mismatch context $ Just $ NotPartOfSuper super
571 Appendable ->
572 mismatch context $ Just $ NotPartOfSuper super
574 Comparable ->
575 do comparableOccursCheck context
576 merge context (Structure flatType)
577 let orientation = _orientation context
578 unifyComparableRecursive orientation a
579 unifyComparableRecursive orientation b
580 case maybeC of
581 Nothing ->
582 return ()
584 Just c ->
585 unifyComparableRecursive orientation c
587 CompAppend ->
588 mismatch context $ Just $ NotPartOfSuper super
590 _ ->
591 mismatch context $ Just $ NotPartOfSuper super
594-- TODO: is there some way to avoid doing this?
595-- Do type classes require occurs checks?
596comparableOccursCheck :: Context -> Unify ()
597comparableOccursCheck (Context _ _ _ var _) =
598 Unify $ \vars ok err ->
599 do hasOccurred <- Occurs.occurs var
600 if hasOccurred
601 then err vars Infinite
602 else ok vars ()
605unifyComparableRecursive :: Orientation -> Variable -> Unify ()
606unifyComparableRecursive orientation var =
607 do compVar <- register $
608 do (Descriptor _ rank _ _) <- UF.get var
609 UF.fresh $ Descriptor (Type.unnamedFlexSuper Comparable) rank noMark Nothing
610 guardedUnify orientation compVar var
614-- UNIFY ALIASES
617unifyAlias :: Context -> ModuleName.Canonical -> N.Name -> [(N.Name, Variable)] -> Variable -> Content -> Unify ()
618unifyAlias context home name args realVar otherContent =
619 case otherContent of
620 FlexVar _ ->
621 merge context (Alias home name args realVar)
623 FlexSuper _ _ ->
624 subUnify context realVar (_second context)
626 RigidVar _ ->
627 subUnify context realVar (_second context)
629 RigidSuper _ _ ->
630 subUnify context realVar (_second context)
632 Alias otherHome otherName otherArgs otherRealVar ->
633 if name == otherName && home == otherHome then
634 do zipWithM_ (subUnify context) (map snd args) (map snd otherArgs)
635 merge context otherContent
637 else
638 subUnify context realVar otherRealVar
640 Structure _ ->
641 subUnify context realVar (_second context)
643 Error _ ->
644 return ()
648-- UNIFY STRUCTURES
651unifyStructure :: Context -> FlatType -> Content -> Content -> Unify ()
652unifyStructure context flatType content otherContent =
653 case otherContent of
654 FlexVar _ ->
655 merge context content
657 FlexSuper super _ ->
658 unifyFlexSuperStructure (reorient context) super flatType
660 RigidVar name ->
661 mismatch context $ Just $ RigidVarTooGeneric name (flatTypeToSpecificThing flatType)
663 RigidSuper super name ->
664 mismatch context $ Just $ RigidSuperTooGeneric super name (flatTypeToSpecificThing flatType)
666 Alias _ _ _ realVar ->
667 subUnify context (_first context) realVar
669 Structure otherFlatType ->
670 case (flatType, otherFlatType) of
671 (App1 home name args, App1 otherHome otherName otherArgs) ->
672 if home == otherHome && name == otherName then
673 do zipWithM_ (subUnify context) args otherArgs
674 merge context otherContent
676 else if isIntFloat home name otherHome otherName then
677 mismatch context (Just IntFloat)
679 else
680 mismatch context Nothing
682 (Fun1 arg result, Fun1 otherArg otherResult) ->
683 do subUnify context arg otherArg
684 subUnify context result otherResult
685 merge context otherContent
687 (EmptyRecord1, EmptyRecord1) ->
688 merge context otherContent
690 (Record1 fields ext, EmptyRecord1) | Map.null fields ->
691 subUnify context ext (_second context)
693 (EmptyRecord1, Record1 fields ext) | Map.null fields ->
694 subUnify context (_first context) ext
696 (Record1 fields extension, Record1 otherFields otherExtension) ->
697 Unify $ \vars ok err ->
698 do firstStructure <- gatherFields context fields extension
699 secondStructure <- gatherFields context otherFields otherExtension
700 case unifyRecord context firstStructure secondStructure of
701 Unify k ->
702 k vars ok err
704 (Tuple1 a b Nothing, Tuple1 x y Nothing) ->
705 do subUnify context a x
706 subUnify context b y
708 (Tuple1 a b (Just c), Tuple1 x y (Just z)) ->
709 do subUnify context a x
710 subUnify context b y
711 subUnify context c z
713 _ ->
714 mismatch context Nothing
716 Error _ ->
717 return ()
720isIntFloat :: ModuleName.Canonical -> N.Name -> ModuleName.Canonical -> N.Name -> Bool
721isIntFloat home name otherHome otherName =
722 otherHome == ModuleName.basics
723 && home == ModuleName.basics
724 && (
725 (name == N.int && otherName == N.float)
726 ||
727 (name == N.float && otherName == N.int)
728 )
732-- UNIFY RECORDS
735unifyRecord :: Context -> RecordStructure -> RecordStructure -> Unify ()
736unifyRecord context firstStructure secondStructure =
737 do let (RecordStructure expFields expVar expStruct) = firstStructure
738 let (RecordStructure actFields actVar actStruct) = secondStructure
740 let sharedFields = Map.intersectionWith (,) expFields actFields
742 -- call after unifying extension, make sure record shape matches before
743 -- looking into whether the particular field types match.
744 let unifySharedFields otherFields ext =
745 do unifySharedFieldsHelp context sharedFields
746 let allFields = Map.union (Map.map fst sharedFields) otherFields
747 merge context (Structure (Record1 allFields ext))
749 let uniqueExpFields = Map.difference expFields actFields
750 let uniqueActFields = Map.difference actFields expFields
752 case (expStruct, Map.null uniqueExpFields, actStruct, Map.null uniqueActFields) of
753 (_, True, _, True) ->
754 do subUnify context expVar actVar
755 unifySharedFields Map.empty expVar
757 (Empty, _, _, False) ->
758 mismatch context $ Just $
759 MessyFields (Map.keys sharedFields) (Map.keys uniqueExpFields) (Map.keys uniqueActFields)
761 (_, False, Empty, _) ->
762 mismatch context $ Just $
763 MessyFields (Map.keys sharedFields) (Map.keys uniqueExpFields) (Map.keys uniqueActFields)
765 (_, False, _, True) ->
766 do subRecord <- fresh context (Structure (Record1 uniqueExpFields expVar))
767 subUnify context subRecord actVar
768 unifySharedFields Map.empty subRecord
770 (_, True, _, False) ->
771 do subRecord <- fresh context (Structure (Record1 uniqueActFields actVar))
772 subUnify context expVar subRecord
773 unifySharedFields Map.empty subRecord
775 (Extension, False, Extension, False) ->
776 do let subFields = Map.union uniqueExpFields uniqueActFields
777 subExt <- fresh context Type.unnamedFlexVar
778 expRecord <- fresh context (Structure (Record1 uniqueActFields subExt))
779 actRecord <- fresh context (Structure (Record1 uniqueExpFields subExt))
780 subUnify context expVar expRecord
781 subUnify context actRecord actVar
782 unifySharedFields subFields subExt
786unifySharedFieldsHelp :: Context -> Map.Map N.Name (Variable, Variable) -> Unify ()
787unifySharedFieldsHelp context sharedFields =
788 do badFields <- Map.traverseMaybeWithKey (unifyField context) sharedFields
789 case Map.toList badFields of
790 [] ->
791 return ()
793 badFieldPairs ->
794 mismatch context (Just (BadFields badFieldPairs))
797unifyField :: Context -> N.Name -> (Variable, Variable) -> Unify (Maybe (Maybe Reason))
798unifyField context _ (actual, expected) =
799 Unify $ \vars ok _ ->
800 case subUnify context actual expected of
801 Unify k ->
802 k vars
803 (\vs () -> ok vs Nothing)
804 (\vs problem ->
805 ok vs $ Just $
806 case problem of
807 Reason _ reason ->
808 reason
810 Infinite ->
811 Nothing
812 )
816-- GATHER RECORD STRUCTURE
819data RecordStructure =
820 RecordStructure
821 { _fields :: Map.Map N.Name Variable
822 , _extVar :: Variable
823 , _extStruct :: ExtensionStructure
824 }
827data ExtensionStructure
828 = Empty
829 | Extension
832gatherFields :: Context -> Map.Map N.Name Variable -> Variable -> IO RecordStructure
833gatherFields context fields variable =
834 do (Descriptor content _ _ _) <- UF.get variable
835 case content of
836 Structure (Record1 subFields subExt) ->
837 gatherFields context (Map.union fields subFields) subExt
839 Structure EmptyRecord1 ->
840 return (RecordStructure fields variable Empty)
842 Alias _ _ _ var ->
843 -- TODO may be dropping useful alias info here
844 gatherFields context fields var
846 _ ->
847 return (RecordStructure fields variable Extension)