git.iko.soy/elk
on 2de786d help sign in
elk/src/Type/Unify.hs
726 lines 20 kB history raw
1{-# OPTIONS_GHC -Wall #-}
2module Type.Unify (unify) where
4import Control.Monad (zipWithM_)
5import Control.Monad.Except (ExceptT, lift, liftIO, throwError, runExceptT)
6import qualified Data.Map as Map
7import qualified Data.Maybe as Maybe
8import qualified Data.UnionFind.IO as UF
10import qualified AST.Variable as Var
11import qualified Reporting.Region as R
12import qualified Reporting.Error.Type as Error
13import qualified Type.State as TS
14import Type.Type as Type
18-- KICK OFF UNIFICATION
21unify :: Error.Hint -> R.Region -> Variable -> Variable -> TS.Solver ()
22unify hint region expected actual =
23 do result <- runExceptT (guardedUnify ExpectedActual expected actual)
24 case result of
25 Right () ->
26 return ()
28 Left (Mismatch maybeReason) ->
29 let
30 mkError =
31 do expectedSrcType <- Type.toSrcType expected
32 actualSrcType <- Type.toSrcType actual
33 mergeHelp expected actual Error
34 let info = Error.MismatchInfo hint expectedSrcType actualSrcType maybeReason
35 return (Error.Mismatch info)
36 in
37 TS.addError region =<< liftIO mkError
41-- UNIFICATION HELPERS
44type Unify =
45 ExceptT Mismatch TS.Solver
48data Context = Context
49 { _orientation :: Orientation
50 , _first :: Variable
51 , _firstDesc :: Descriptor
52 , _second :: Variable
53 , _secondDesc :: Descriptor
54 }
57data Orientation = ExpectedActual | ActualExpected
60reorient :: Context -> Context
61reorient (Context orientation var1 desc1 var2 desc2) =
62 let
63 otherOrientation =
64 case orientation of
65 ExpectedActual -> ActualExpected
66 ActualExpected -> ExpectedActual
67 in
68 Context otherOrientation var2 desc2 var1 desc1
72-- ERROR MESSAGES
75newtype Mismatch =
76 Mismatch (Maybe Error.Reason)
79mismatch :: Context -> Maybe Error.Reason -> Unify a
80mismatch context@(Context orientation var1 _ var2 _) maybeReason =
81 do args1 <- liftIO $ collectArgs var1
82 args2 <- liftIO $ collectArgs var2
84 let numArgs1 = length args1
85 let numArgs2 = length args2
87 if numArgs1 == numArgs2
88 then
89 mismatchHelp orientation maybeReason
90 else
91 do zipWithM_ (\arg1 arg2 -> lift $ runExceptT $ subUnify context arg1 arg2) args1 args2
92 mismatchHelp orientation $ Just $ Error.MissingArgs $ abs (numArgs2 - numArgs1)
95mismatchHelp :: Orientation -> Maybe Error.Reason -> Unify a
96mismatchHelp orientation maybeReason =
97 throwError $ Mismatch $
98 case orientation of
99 ExpectedActual ->
100 maybeReason
102 ActualExpected ->
103 Error.flipReason <$> maybeReason
106badRigid :: Maybe String -> Error.Reason
107badRigid maybeName =
108 Error.BadVar (Just (Error.Rigid maybeName)) Nothing
111badSuper :: Super -> Error.Reason
112badSuper super =
113 Error.BadVar (Just (errorSuper super)) Nothing
116doubleBad :: Error.VarType -> Error.VarType -> Error.Reason
117doubleBad vt1 vt2 =
118 Error.BadVar (Just vt1) (Just vt2)
121errorSuper :: Super -> Error.VarType
122errorSuper super =
123 case super of
124 Number ->
125 Error.Number
127 Comparable ->
128 Error.Comparable
130 Appendable ->
131 Error.Appendable
133 CompAppend ->
134 Error.CompAppend
138-- MERGE
141merge :: Context -> Content -> Unify ()
142merge (Context _ first _ second _) content =
143 liftIO $ mergeHelp first second content
146mergeHelp :: Variable -> Variable -> Content -> IO ()
147mergeHelp first second content =
148 UF.union' first second $ \desc1 desc2 ->
149 return $
150 Descriptor
151 { _content = content
152 , _rank = min (_rank desc1) (_rank desc2)
153 , _mark = noMark
154 , _copy = Nothing
155 }
158fresh :: Context -> Content -> Unify Variable
159fresh (Context _ _ desc1 _ desc2) content =
160 do freshVariable <-
161 liftIO $ UF.fresh $
162 Descriptor
163 { _content = content
164 , _rank = min (_rank desc1) (_rank desc2)
165 , _mark = noMark
166 , _copy = Nothing
167 }
168 lift (TS.register freshVariable)
172-- ACTUALLY UNIFY THINGS
175guardedUnify :: Orientation -> Variable -> Variable -> Unify ()
176guardedUnify orientation left right =
177 do equivalent <- liftIO $ UF.equivalent left right
178 if equivalent
179 then return ()
180 else
181 do leftDesc <- liftIO $ UF.descriptor left
182 rightDesc <- liftIO $ UF.descriptor right
183 actuallyUnify (Context orientation left leftDesc right rightDesc)
186subUnify :: Context -> Variable -> Variable -> Unify ()
187subUnify context var1 var2 =
188 guardedUnify (_orientation context) var1 var2
191actuallyUnify :: Context -> Unify ()
192actuallyUnify context@(Context _ _ firstDesc _ secondDesc) =
193 let
194 secondContent = _content secondDesc
195 in
196 case _content firstDesc of
197 Error ->
198 -- If there was an error, just pretend it is okay. This lets us avoid
199 -- "cascading" errors where one problem manifests as multiple message.
200 return ()
202 Var Flex Nothing _ ->
203 unifyFlex context secondContent
205 Var Flex (Just super) _ ->
206 unifySuper context super secondContent
208 Var Rigid maybeSuper maybeName ->
209 unifyRigid context maybeSuper maybeName secondContent
211 Atom name ->
212 unifyAtom context name secondContent
214 Alias name args realVar ->
215 unifyAlias context name args realVar secondContent
217 Structure term ->
218 unifyStructure context term secondContent
222-- UNIFY FLEXIBLE VARIABLES
225unifyFlex :: Context -> Content -> Unify ()
226unifyFlex context otherContent =
227 case otherContent of
228 Error ->
229 return ()
231 Var Flex _ _ ->
232 merge context otherContent
234 Var Rigid _ _ ->
235 merge context otherContent
237 Atom _ ->
238 merge context otherContent
240 Alias _ _ _ ->
241 merge context otherContent
243 Structure _ ->
244 merge context otherContent
248-- UNIFY RIGID VARIABLES
251unifyRigid :: Context -> Maybe Super -> Maybe String -> Content -> Unify ()
252unifyRigid context maybeSuper maybeName otherContent =
253 case otherContent of
254 Error ->
255 return ()
257 Var Flex otherMaybeSuper _ ->
258 case (maybeSuper, otherMaybeSuper) of
259 (_, Nothing) ->
260 merge context (Var Rigid maybeSuper maybeName)
262 (Nothing, Just _) ->
263 mismatch context (Just (badRigid maybeName))
265 (Just super, Just otherSuper) ->
266 case combineSupers super otherSuper of
267 Right newSuper | newSuper == otherSuper ->
268 merge context otherContent
270 _ ->
271 mismatch context (Just (badRigid maybeName))
273 Var Rigid _ otherMaybeName ->
274 mismatch context $ Just $
275 doubleBad (Error.Rigid maybeName) (Error.Rigid otherMaybeName)
277 Atom _ ->
278 mismatch context (Just (badRigid maybeName))
280 Alias _ _ _ ->
281 mismatch context (Just (badRigid maybeName))
283 Structure _ ->
284 mismatch context (Just (badRigid maybeName))
288-- UNIFY SUPER VARIABLES
291unifySuper :: Context -> Super -> Content -> Unify ()
292unifySuper context super otherContent =
293 case otherContent of
294 Structure term ->
295 unifySuperStructure context super term
297 Atom name ->
298 if atomMatchesSuper super name then
299 merge context otherContent
300 else
301 mismatch context (Just (badSuper super))
303 Var Rigid Nothing maybeName ->
304 mismatch context (Just (doubleBad (errorSuper super) (Error.Rigid maybeName)))
306 Var Rigid (Just otherSuper) maybeName ->
307 case combineSupers super otherSuper of
308 Right newSuper | newSuper == super ->
309 merge context otherContent
311 _ ->
312 mismatch context $ Just $
313 doubleBad (errorSuper super) (Error.Rigid maybeName)
315 Var Flex Nothing _ ->
316 merge context (Var Flex (Just super) Nothing)
318 Var Flex (Just otherSuper) _ ->
319 case combineSupers super otherSuper of
320 Left reason ->
321 mismatch context (Just reason)
323 Right newSuper ->
324 merge context (Var Flex (Just newSuper) Nothing)
326 Alias _ _ realVar ->
327 subUnify context (_first context) realVar
329 Error ->
330 return ()
333combineSupers :: Super -> Super -> Either Error.Reason Super
334combineSupers firstSuper secondSuper =
335 case (firstSuper, secondSuper) of
336 (Number , Number ) -> Right Number
337 (Comparable, Number ) -> Right Number
338 (Number , Comparable) -> Right Number
340 (Comparable, Comparable) -> Right Comparable
341 (Appendable, Appendable) -> Right Appendable
343 (Appendable, Comparable) -> Right CompAppend
344 (Comparable, Appendable) -> Right CompAppend
346 (CompAppend, CompAppend) -> Right CompAppend
347 (CompAppend, Comparable) -> Right CompAppend
348 (Comparable, CompAppend) -> Right CompAppend
349 (CompAppend, Appendable) -> Right CompAppend
350 (Appendable, CompAppend) -> Right CompAppend
352 (_ , _ ) ->
353 Left $ doubleBad (errorSuper firstSuper) (errorSuper secondSuper)
356isPrimitiveFrom :: [String] -> Var.Canonical -> Bool
357isPrimitiveFrom prims var =
358 any (\p -> Var.isPrim p var) prims
361atomMatchesSuper :: Super -> Var.Canonical -> Bool
362atomMatchesSuper super name =
363 case super of
364 Number ->
365 isPrimitiveFrom ["Int", "Float"] name
367 Comparable ->
368 isPrimitiveFrom ["Int", "Float", "Char", "String"] name
370 Appendable ->
371 Var.isPrim "String" name
373 CompAppend ->
374 Var.isPrim "String" name
377unifySuperStructure :: Context -> Super -> Term1 Variable -> Unify ()
378unifySuperStructure context super term =
379 do appStructure <- liftIO (collectApps (Structure term))
380 case appStructure of
381 Other ->
382 mismatch context (Just (badSuper super))
384 List variable ->
385 case super of
386 Number ->
387 mismatch context (Just (badSuper super))
389 Appendable ->
390 merge context (Structure term)
392 Comparable ->
393 do merge context (Structure term)
394 unifyComparableRecursive (_orientation context) variable
396 CompAppend ->
397 do merge context (Structure term)
398 unifyComparableRecursive (_orientation context) variable
400 Tuple entries ->
401 case super of
402 Number ->
403 mismatch context (Just (badSuper super))
405 Appendable ->
406 mismatch context (Just (badSuper super))
408 Comparable ->
409 if length entries > 6 then
410 mismatch context (Just (Error.TooLongComparableTuple (length entries)))
412 else
413 do merge context (Structure term)
414 mapM_ (unifyComparableRecursive (_orientation context)) entries
416 CompAppend ->
417 mismatch context (Just (badSuper super))
420unifyComparableRecursive :: Orientation -> Variable -> Unify ()
421unifyComparableRecursive orientation var =
422 do compVar <-
423 liftIO $
424 do desc <- UF.descriptor var
425 UF.fresh $
426 Descriptor
427 { _content = Var Flex (Just Comparable) Nothing
428 , _rank = _rank desc
429 , _mark = noMark
430 , _copy = Nothing
431 }
433 guardedUnify orientation compVar var
436data AppStructure
437 = List Variable
438 | Tuple [Variable]
439 | Other
442collectApps :: Content -> IO AppStructure
443collectApps content =
444 collectAppsHelp [] content
447collectAppsHelp :: [Variable] -> Content -> IO AppStructure
448collectAppsHelp args content =
449 case (content, args) of
450 (Structure (App1 func arg), _) ->
451 collectAppsHelp (args ++ [arg]) =<< getContent func
453 (Atom name, [arg]) | Var.isList name ->
454 return (List arg)
456 (Atom name, _) | Var.isTuple name ->
457 return (Tuple args)
459 _ ->
460 return Other
463collectArgs :: Variable -> IO [Variable]
464collectArgs variable =
465 collectArgsHelp [] variable
468collectArgsHelp :: [Variable] -> Variable -> IO [Variable]
469collectArgsHelp revArgs variable =
470 do content <- getContent variable
471 case content of
472 Structure (Fun1 arg returnType) ->
473 collectArgsHelp (arg : revArgs) returnType
475 _ ->
476 return $ variable : revArgs
479getContent :: Variable -> IO Content
480getContent variable =
481 _content <$> UF.descriptor variable
485-- UNIFY ATOMS
488unifyAtom :: Context -> Var.Canonical -> Content -> Unify ()
489unifyAtom context name otherContent =
490 case otherContent of
491 Error ->
492 return ()
494 Var Flex Nothing _ ->
495 merge context (Atom name)
497 Var Flex (Just super) _ ->
498 if atomMatchesSuper super name then
499 merge context (Atom name)
501 else
502 mismatch context (Just ((Error.flipReason (badSuper super))))
504 Var Rigid _ maybeName ->
505 mismatch context (Just (Error.flipReason (badRigid maybeName)))
507 Atom otherName ->
508 if name == otherName then
509 merge context otherContent
511 else
512 mismatch context $
513 if isIntFloat name otherName || isIntFloat otherName name then
514 Just Error.IntFloat
515 else
516 Nothing
518 Alias _ _ realVar ->
519 subUnify context (_first context) realVar
521 Structure _ ->
522 mismatch context Nothing
525isIntFloat :: Var.Canonical -> Var.Canonical -> Bool
526isIntFloat name otherName =
527 Var.isPrim "Int" name && Var.isPrim "Float" otherName
531-- UNIFY ALIASES
534unifyAlias :: Context -> Var.Canonical -> [(String, Variable)] -> Variable -> Content -> Unify ()
535unifyAlias context name args realVar otherContent =
536 case otherContent of
537 Error ->
538 return ()
540 Var Flex Nothing _ ->
541 merge context (Alias name args realVar)
543 Var _ _ _ ->
544 subUnify context realVar (_second context)
546 Atom _ ->
547 subUnify context realVar (_second context)
550 Alias otherName otherArgs otherRealVar ->
551 if name == otherName then
552 do zipWithM_ (subUnify context) (map snd args) (map snd otherArgs)
553 merge context otherContent
555 else
556 subUnify context realVar otherRealVar
558 Structure _ ->
559 subUnify context realVar (_second context)
563-- UNIFY STRUCTURES
566unifyStructure :: Context -> Term1 Variable -> Content -> Unify ()
567unifyStructure context term otherContent =
568 case otherContent of
569 Error ->
570 return ()
572 Var Flex Nothing _ ->
573 merge context (Structure term)
575 Var Flex (Just super) _ ->
576 unifySuper (reorient context) super (Structure term)
578 Var Rigid _ maybeName ->
579 mismatch context (Just (Error.flipReason (badRigid maybeName)))
581 Atom _ ->
582 mismatch context Nothing
584 Alias _ _ realVar ->
585 subUnify context (_first context) realVar
587 Structure otherTerm ->
588 case (term, otherTerm) of
589 (App1 func arg, App1 otherFunc otherArg) ->
590 do subUnify context func otherFunc
591 subUnify context arg otherArg
592 merge context otherContent
594 (Fun1 arg result, Fun1 otherArg otherResult) ->
595 do subUnify context arg otherArg
596 subUnify context result otherResult
597 merge context otherContent
599 (EmptyRecord1, EmptyRecord1) ->
600 merge context otherContent
602 (Record1 fields ext, EmptyRecord1) | Map.null fields ->
603 subUnify context ext (_second context)
605 (EmptyRecord1, Record1 fields ext) | Map.null fields ->
606 subUnify context (_first context) ext
608 (Record1 fields extension, Record1 otherFields otherExtension) ->
609 do firstStructure <- gatherFields context fields extension
610 secondStructure <- gatherFields context otherFields otherExtension
611 unifyRecord context firstStructure secondStructure
613 _ ->
614 mismatch context Nothing
618-- UNIFY RECORDS
621unifyRecord :: Context -> RecordStructure -> RecordStructure -> Unify ()
622unifyRecord context firstStructure secondStructure =
623 do let (RecordStructure expFields expVar expStruct) = firstStructure
624 let (RecordStructure actFields actVar actStruct) = secondStructure
626 let sharedFields = Map.intersectionWith (,) expFields actFields
628 -- call after unifying extension, make sure record shape matches before
629 -- looking into whether the particular field types match.
630 let unifySharedFields otherFields ext =
631 do unifySharedFieldsHelp context sharedFields
632 let allFields = Map.union (Map.map fst sharedFields) otherFields
633 merge context (Structure (Record1 allFields ext))
635 let uniqueExpFields = Map.difference expFields actFields
636 let uniqueActFields = Map.difference actFields expFields
638 case (expStruct, Map.null uniqueExpFields, actStruct, Map.null uniqueActFields) of
639 (_, True, _, True) ->
640 do subUnify context expVar actVar
641 unifySharedFields Map.empty expVar
643 (Empty, _, _, False) ->
644 mismatch context $ Just $
645 Error.MessyFields (Map.keys sharedFields) (Map.keys uniqueExpFields) (Map.keys uniqueActFields)
647 (_, False, Empty, _) ->
648 mismatch context $ Just $
649 Error.MessyFields (Map.keys sharedFields) (Map.keys uniqueExpFields) (Map.keys uniqueActFields)
651 (_, False, _, True) ->
652 do subRecord <- fresh context (Structure (Record1 uniqueExpFields expVar))
653 subUnify context subRecord actVar
654 unifySharedFields Map.empty subRecord
656 (_, True, _, False) ->
657 do subRecord <- fresh context (Structure (Record1 uniqueActFields actVar))
658 subUnify context expVar subRecord
659 unifySharedFields Map.empty subRecord
661 (Extension, False, Extension, False) ->
662 do let subFields = Map.union uniqueExpFields uniqueActFields
663 subExt <- fresh context (Var Flex Nothing Nothing)
664 expRecord <- fresh context (Structure (Record1 uniqueActFields subExt))
665 actRecord <- fresh context (Structure (Record1 uniqueExpFields subExt))
666 subUnify context expVar expRecord
667 subUnify context actRecord actVar
668 unifySharedFields subFields subExt
672unifySharedFieldsHelp :: Context -> Map.Map String (Variable, Variable) -> Unify ()
673unifySharedFieldsHelp context sharedFields =
674 do maybeBadFields <- traverse (unifyField context) (Map.toList sharedFields)
675 case Maybe.catMaybes maybeBadFields of
676 [] ->
677 return ()
679 badFields ->
680 mismatch context (Just (Error.BadFields (reverse badFields)))
683unifyField :: Context -> (String, (Variable, Variable)) -> Unify (Maybe (String, Maybe Error.Reason))
684unifyField context (field, (expected, actual)) =
685 do result <- lift $ runExceptT $ subUnify context expected actual
686 case result of
687 Right () ->
688 return $ Nothing
690 Left (Mismatch maybeReason) ->
691 return $ Just (field, maybeReason)
695-- GATHER RECORD STRUCTURE
698data RecordStructure = RecordStructure
699 { _fields :: Map.Map String Variable
700 , _extVar :: Variable
701 , _extStruct :: ExtensionStructure
702 }
705data ExtensionStructure
706 = Empty
707 | Extension
710gatherFields :: Context -> Map.Map String Variable -> Variable -> Unify RecordStructure
711gatherFields context fields variable =
712 do desc <- liftIO (UF.descriptor variable)
713 case _content desc of
714 Structure (Record1 subFields subExt) ->
715 gatherFields context (Map.union fields subFields) subExt
717 Structure EmptyRecord1 ->
718 return (RecordStructure fields variable Empty)
720 Alias _ _ var ->
721 -- TODO may be dropping useful alias info here
722 gatherFields context fields var
724 _ ->
725 return (RecordStructure fields variable Extension)