on fe7bbbd help sign in
elk/src/Type/Unify.hs
727 lines 20 kB history raw
1{-# OPTIONS_GHC -Wall #-}
2{-# LANGUAGE OverloadedStrings #-}
3module Type.Unify (unify) where
5import Control.Monad (zipWithM_)
6import Control.Monad.Except (ExceptT, lift, liftIO, throwError, runExceptT)
7import qualified Data.Map as Map
8import qualified Data.Maybe as Maybe
9import Data.Text (Text)
10import qualified Data.UnionFind.IO as UF
12import qualified AST.Variable as Var
13import qualified Reporting.Region as R
14import qualified Reporting.Error.Type as Error
15import qualified Type.State as TS
16import Type.Type as Type
20-- KICK OFF UNIFICATION
23unify :: Error.Hint -> R.Region -> Variable -> Variable -> TS.Solver ()
24unify hint region expected actual =
25 do result <- runExceptT (guardedUnify ExpectedActual expected actual)
26 case result of
27 Right () ->
28 return ()
30 Left (Mismatch maybeReason) ->
31 let
32 mkError =
33 do expectedSrcType <- Type.toSrcType expected
34 actualSrcType <- Type.toSrcType actual
35 mergeHelp expected actual Error
36 let info = Error.MismatchInfo hint expectedSrcType actualSrcType maybeReason
37 return (Error.Mismatch info)
38 in
39 TS.addError region =<< liftIO mkError
43-- UNIFICATION HELPERS
46type Unify =
47 ExceptT Mismatch TS.Solver
50data Context = Context
51 { _orientation :: Orientation
52 , _first :: Variable
53 , _firstDesc :: Descriptor
54 , _second :: Variable
55 , _secondDesc :: Descriptor
56 }
59data Orientation = ExpectedActual | ActualExpected
62reorient :: Context -> Context
63reorient (Context orientation var1 desc1 var2 desc2) =
64 let
65 otherOrientation =
66 case orientation of
67 ExpectedActual -> ActualExpected
68 ActualExpected -> ExpectedActual
69 in
70 Context otherOrientation var2 desc2 var1 desc1
74-- ERROR MESSAGES
77newtype Mismatch =
78 Mismatch (Maybe Error.Reason)
81mismatch :: Context -> Maybe Error.Reason -> Unify a
82mismatch context@(Context orientation var1 _ var2 _) maybeReason =
83 do args1 <- liftIO $ collectArgs var1
84 args2 <- liftIO $ collectArgs var2
86 let numArgs1 = length args1
87 let numArgs2 = length args2
89 if numArgs1 == numArgs2
90 then
91 mismatchHelp orientation maybeReason
92 else
93 do zipWithM_ (\arg1 arg2 -> lift $ runExceptT $ subUnify context arg1 arg2) args1 args2
94 mismatchHelp orientation $ Just $ Error.MissingArgs $ abs (numArgs2 - numArgs1)
97mismatchHelp :: Orientation -> Maybe Error.Reason -> Unify a
98mismatchHelp orientation maybeReason =
99 throwError $ Mismatch $
100 case orientation of
101 ExpectedActual ->
102 maybeReason
104 ActualExpected ->
105 Error.flipReason <$> maybeReason
108badRigid :: Maybe Text -> Error.Reason
109badRigid maybeName =
110 Error.BadVar (Just (Error.Rigid maybeName)) Nothing
113badSuper :: Super -> Error.Reason
114badSuper super =
115 Error.BadVar (Just (errorSuper super)) Nothing
118doubleBad :: Error.VarType -> Error.VarType -> Error.Reason
119doubleBad vt1 vt2 =
120 Error.BadVar (Just vt1) (Just vt2)
123errorSuper :: Super -> Error.VarType
124errorSuper super =
125 case super of
126 Number ->
127 Error.Number
129 Comparable ->
130 Error.Comparable
132 Appendable ->
133 Error.Appendable
135 CompAppend ->
136 Error.CompAppend
140-- MERGE
143merge :: Context -> Content -> Unify ()
144merge (Context _ first _ second _) content =
145 liftIO $ mergeHelp first second content
148mergeHelp :: Variable -> Variable -> Content -> IO ()
149mergeHelp first second content =
150 UF.union' first second $ \desc1 desc2 ->
151 return $
152 Descriptor
153 { _content = content
154 , _rank = min (_rank desc1) (_rank desc2)
155 , _mark = noMark
156 , _copy = Nothing
157 }
160fresh :: Context -> Content -> Unify Variable
161fresh (Context _ _ desc1 _ desc2) content =
162 do freshVariable <-
163 liftIO $ UF.fresh $
164 Descriptor
165 { _content = content
166 , _rank = min (_rank desc1) (_rank desc2)
167 , _mark = noMark
168 , _copy = Nothing
169 }
170 lift (TS.register freshVariable)
174-- ACTUALLY UNIFY THINGS
177guardedUnify :: Orientation -> Variable -> Variable -> Unify ()
178guardedUnify orientation left right =
179 do equivalent <- liftIO $ UF.equivalent left right
180 if equivalent
181 then return ()
182 else
183 do leftDesc <- liftIO $ UF.descriptor left
184 rightDesc <- liftIO $ UF.descriptor right
185 actuallyUnify (Context orientation left leftDesc right rightDesc)
188subUnify :: Context -> Variable -> Variable -> Unify ()
189subUnify context var1 var2 =
190 guardedUnify (_orientation context) var1 var2
193actuallyUnify :: Context -> Unify ()
194actuallyUnify context@(Context _ _ firstDesc _ secondDesc) =
195 let
196 secondContent = _content secondDesc
197 in
198 case _content firstDesc of
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 return ()
204 Var Flex Nothing _ ->
205 unifyFlex context secondContent
207 Var Flex (Just super) _ ->
208 unifySuper context super secondContent
210 Var Rigid maybeSuper maybeName ->
211 unifyRigid context maybeSuper maybeName secondContent
213 Atom name ->
214 unifyAtom context name secondContent
216 Alias name args realVar ->
217 unifyAlias context name args realVar secondContent
219 Structure term ->
220 unifyStructure context term secondContent
224-- UNIFY FLEXIBLE VARIABLES
227unifyFlex :: Context -> Content -> Unify ()
228unifyFlex context otherContent =
229 case otherContent of
230 Error ->
231 return ()
233 Var Flex _ _ ->
234 merge context otherContent
236 Var Rigid _ _ ->
237 merge context otherContent
239 Atom _ ->
240 merge context otherContent
242 Alias _ _ _ ->
243 merge context otherContent
245 Structure _ ->
246 merge context otherContent
250-- UNIFY RIGID VARIABLES
253unifyRigid :: Context -> Maybe Super -> Maybe Text -> Content -> Unify ()
254unifyRigid context maybeSuper maybeName otherContent =
255 case otherContent of
256 Error ->
257 return ()
259 Var Flex otherMaybeSuper _ ->
260 case (maybeSuper, otherMaybeSuper) of
261 (_, Nothing) ->
262 merge context (Var Rigid maybeSuper maybeName)
264 (Nothing, Just _) ->
265 mismatch context (Just (badRigid maybeName))
267 (Just super, Just otherSuper) ->
268 case combineSupers super otherSuper of
269 Right newSuper | newSuper == otherSuper ->
270 merge context otherContent
272 _ ->
273 mismatch context (Just (badRigid maybeName))
275 Var Rigid _ otherMaybeName ->
276 mismatch context $ Just $
277 doubleBad (Error.Rigid maybeName) (Error.Rigid otherMaybeName)
279 Atom _ ->
280 mismatch context (Just (badRigid maybeName))
282 Alias _ _ _ ->
283 mismatch context (Just (badRigid maybeName))
285 Structure _ ->
286 mismatch context (Just (badRigid maybeName))
290-- UNIFY SUPER VARIABLES
293unifySuper :: Context -> Super -> Content -> Unify ()
294unifySuper context super otherContent =
295 case otherContent of
296 Structure term ->
297 unifySuperStructure context super term
299 Atom name ->
300 if atomMatchesSuper super name then
301 merge context otherContent
302 else
303 mismatch context (Just (badSuper super))
305 Var Rigid Nothing maybeName ->
306 mismatch context (Just (doubleBad (errorSuper super) (Error.Rigid maybeName)))
308 Var Rigid (Just otherSuper) maybeName ->
309 case combineSupers super otherSuper of
310 Right newSuper | newSuper == super ->
311 merge context otherContent
313 _ ->
314 mismatch context $ Just $
315 doubleBad (errorSuper super) (Error.Rigid maybeName)
317 Var Flex Nothing _ ->
318 merge context (Var Flex (Just super) Nothing)
320 Var Flex (Just otherSuper) _ ->
321 case combineSupers super otherSuper of
322 Left reason ->
323 mismatch context (Just reason)
325 Right newSuper ->
326 merge context (Var Flex (Just newSuper) Nothing)
328 Alias _ _ realVar ->
329 subUnify context (_first context) realVar
331 Error ->
332 return ()
335combineSupers :: Super -> Super -> Either Error.Reason Super
336combineSupers firstSuper secondSuper =
337 case (firstSuper, secondSuper) of
338 (Number , Number ) -> Right Number
339 (Comparable, Number ) -> Right Number
340 (Number , Comparable) -> Right Number
342 (Comparable, Comparable) -> Right Comparable
343 (Appendable, Appendable) -> Right Appendable
345 (Appendable, Comparable) -> Right CompAppend
346 (Comparable, Appendable) -> Right CompAppend
348 (CompAppend, CompAppend) -> Right CompAppend
349 (CompAppend, Comparable) -> Right CompAppend
350 (Comparable, CompAppend) -> Right CompAppend
351 (CompAppend, Appendable) -> Right CompAppend
352 (Appendable, CompAppend) -> Right CompAppend
354 (_ , _ ) ->
355 Left $ doubleBad (errorSuper firstSuper) (errorSuper secondSuper)
358isPrimitiveFrom :: [Text] -> Var.Canonical -> Bool
359isPrimitiveFrom prims var =
360 any (\p -> Var.isPrim p var) prims
363atomMatchesSuper :: Super -> Var.Canonical -> Bool
364atomMatchesSuper super name =
365 case super of
366 Number ->
367 isPrimitiveFrom ["Int", "Float"] name
369 Comparable ->
370 isPrimitiveFrom ["Int", "Float", "Char", "String"] name
372 Appendable ->
373 Var.isPrim "String" name
375 CompAppend ->
376 Var.isPrim "String" name
379unifySuperStructure :: Context -> Super -> Term1 Variable -> Unify ()
380unifySuperStructure context super term =
381 do appStructure <- liftIO (collectApps (Structure term))
382 case appStructure of
383 Other ->
384 mismatch context (Just (badSuper super))
386 List variable ->
387 case super of
388 Number ->
389 mismatch context (Just (badSuper super))
391 Appendable ->
392 merge context (Structure term)
394 Comparable ->
395 do merge context (Structure term)
396 unifyComparableRecursive (_orientation context) variable
398 CompAppend ->
399 do merge context (Structure term)
400 unifyComparableRecursive (_orientation context) variable
402 Tuple entries ->
403 case super of
404 Number ->
405 mismatch context (Just (badSuper super))
407 Appendable ->
408 mismatch context (Just (badSuper super))
410 Comparable ->
411 if length entries > 6 then
412 mismatch context (Just (Error.TooLongComparableTuple (length entries)))
414 else
415 do merge context (Structure term)
416 mapM_ (unifyComparableRecursive (_orientation context)) entries
418 CompAppend ->
419 mismatch context (Just (badSuper super))
422unifyComparableRecursive :: Orientation -> Variable -> Unify ()
423unifyComparableRecursive orientation var =
424 do compVar <-
425 liftIO $
426 do desc <- UF.descriptor var
427 UF.fresh $
428 Descriptor
429 { _content = Var Flex (Just Comparable) Nothing
430 , _rank = _rank desc
431 , _mark = noMark
432 , _copy = Nothing
433 }
435 guardedUnify orientation compVar var
438data AppStructure
439 = List Variable
440 | Tuple [Variable]
441 | Other
444collectApps :: Content -> IO AppStructure
445collectApps content =
446 collectAppsHelp [] content
449collectAppsHelp :: [Variable] -> Content -> IO AppStructure
450collectAppsHelp args content =
451 case (content, args) of
452 (Structure (App1 func arg), _) ->
453 collectAppsHelp (args ++ [arg]) =<< getContent func
455 (Atom name, [arg]) | Var.isList name ->
456 return (List arg)
458 (Atom name, _) | Var.isTuple name ->
459 return (Tuple args)
461 _ ->
462 return Other
465collectArgs :: Variable -> IO [Variable]
466collectArgs variable =
467 collectArgsHelp [] variable
470collectArgsHelp :: [Variable] -> Variable -> IO [Variable]
471collectArgsHelp revArgs variable =
472 do content <- getContent variable
473 case content of
474 Structure (Fun1 arg returnType) ->
475 collectArgsHelp (arg : revArgs) returnType
477 _ ->
478 return $ variable : revArgs
481getContent :: Variable -> IO Content
482getContent variable =
483 _content <$> UF.descriptor variable
487-- UNIFY ATOMS
490unifyAtom :: Context -> Var.Canonical -> Content -> Unify ()
491unifyAtom context name otherContent =
492 case otherContent of
493 Error ->
494 return ()
496 Var Flex Nothing _ ->
497 merge context (Atom name)
499 Var Flex (Just super) _ ->
500 if atomMatchesSuper super name then
501 merge context (Atom name)
503 else
504 mismatch context (Just ((Error.flipReason (badSuper super))))
506 Var Rigid _ maybeName ->
507 mismatch context (Just (Error.flipReason (badRigid maybeName)))
509 Atom otherName ->
510 if name == otherName then
511 merge context otherContent
513 else
514 mismatch context $
515 if isIntFloat name otherName || isIntFloat otherName name then
516 Just Error.IntFloat
517 else
518 Nothing
520 Alias _ _ realVar ->
521 subUnify context (_first context) realVar
523 Structure _ ->
524 mismatch context Nothing
527isIntFloat :: Var.Canonical -> Var.Canonical -> Bool
528isIntFloat name otherName =
529 Var.isPrim "Int" name && Var.isPrim "Float" otherName
533-- UNIFY ALIASES
536unifyAlias :: Context -> Var.Canonical -> [(Text, Variable)] -> Variable -> Content -> Unify ()
537unifyAlias context name args realVar otherContent =
538 case otherContent of
539 Error ->
540 return ()
542 Var Flex Nothing _ ->
543 merge context (Alias name args realVar)
545 Var _ _ _ ->
546 subUnify context realVar (_second context)
548 Atom _ ->
549 subUnify context realVar (_second context)
551 Alias otherName otherArgs otherRealVar ->
552 if name == otherName then
553 do zipWithM_ (subUnify context) (map snd args) (map snd otherArgs)
554 merge context otherContent
556 else
557 subUnify context realVar otherRealVar
559 Structure _ ->
560 subUnify context realVar (_second context)
564-- UNIFY STRUCTURES
567unifyStructure :: Context -> Term1 Variable -> Content -> Unify ()
568unifyStructure context term otherContent =
569 case otherContent of
570 Error ->
571 return ()
573 Var Flex Nothing _ ->
574 merge context (Structure term)
576 Var Flex (Just super) _ ->
577 unifySuper (reorient context) super (Structure term)
579 Var Rigid _ maybeName ->
580 mismatch context (Just (Error.flipReason (badRigid maybeName)))
582 Atom _ ->
583 mismatch context Nothing
585 Alias _ _ realVar ->
586 subUnify context (_first context) realVar
588 Structure otherTerm ->
589 case (term, otherTerm) of
590 (App1 func arg, App1 otherFunc otherArg) ->
591 do subUnify context func otherFunc
592 subUnify context arg otherArg
593 merge context otherContent
595 (Fun1 arg result, Fun1 otherArg otherResult) ->
596 do subUnify context arg otherArg
597 subUnify context result otherResult
598 merge context otherContent
600 (EmptyRecord1, EmptyRecord1) ->
601 merge context otherContent
603 (Record1 fields ext, EmptyRecord1) | Map.null fields ->
604 subUnify context ext (_second context)
606 (EmptyRecord1, Record1 fields ext) | Map.null fields ->
607 subUnify context (_first context) ext
609 (Record1 fields extension, Record1 otherFields otherExtension) ->
610 do firstStructure <- gatherFields context fields extension
611 secondStructure <- gatherFields context otherFields otherExtension
612 unifyRecord context firstStructure secondStructure
614 _ ->
615 mismatch context Nothing
619-- UNIFY RECORDS
622unifyRecord :: Context -> RecordStructure -> RecordStructure -> Unify ()
623unifyRecord context firstStructure secondStructure =
624 do let (RecordStructure expFields expVar expStruct) = firstStructure
625 let (RecordStructure actFields actVar actStruct) = secondStructure
627 let sharedFields = Map.intersectionWith (,) expFields actFields
629 -- call after unifying extension, make sure record shape matches before
630 -- looking into whether the particular field types match.
631 let unifySharedFields otherFields ext =
632 do unifySharedFieldsHelp context sharedFields
633 let allFields = Map.union (Map.map fst sharedFields) otherFields
634 merge context (Structure (Record1 allFields ext))
636 let uniqueExpFields = Map.difference expFields actFields
637 let uniqueActFields = Map.difference actFields expFields
639 case (expStruct, Map.null uniqueExpFields, actStruct, Map.null uniqueActFields) of
640 (_, True, _, True) ->
641 do subUnify context expVar actVar
642 unifySharedFields Map.empty expVar
644 (Empty, _, _, False) ->
645 mismatch context $ Just $
646 Error.MessyFields (Map.keys sharedFields) (Map.keys uniqueExpFields) (Map.keys uniqueActFields)
648 (_, False, Empty, _) ->
649 mismatch context $ Just $
650 Error.MessyFields (Map.keys sharedFields) (Map.keys uniqueExpFields) (Map.keys uniqueActFields)
652 (_, False, _, True) ->
653 do subRecord <- fresh context (Structure (Record1 uniqueExpFields expVar))
654 subUnify context subRecord actVar
655 unifySharedFields Map.empty subRecord
657 (_, True, _, False) ->
658 do subRecord <- fresh context (Structure (Record1 uniqueActFields actVar))
659 subUnify context expVar subRecord
660 unifySharedFields Map.empty subRecord
662 (Extension, False, Extension, False) ->
663 do let subFields = Map.union uniqueExpFields uniqueActFields
664 subExt <- fresh context (Var Flex Nothing Nothing)
665 expRecord <- fresh context (Structure (Record1 uniqueActFields subExt))
666 actRecord <- fresh context (Structure (Record1 uniqueExpFields subExt))
667 subUnify context expVar expRecord
668 subUnify context actRecord actVar
669 unifySharedFields subFields subExt
673unifySharedFieldsHelp :: Context -> Map.Map Text (Variable, Variable) -> Unify ()
674unifySharedFieldsHelp context sharedFields =
675 do maybeBadFields <- traverse (unifyField context) (Map.toList sharedFields)
676 case Maybe.catMaybes maybeBadFields of
677 [] ->
678 return ()
680 badFields ->
681 mismatch context (Just (Error.BadFields (reverse badFields)))
684unifyField :: Context -> (Text, (Variable, Variable)) -> Unify (Maybe (Text, Maybe Error.Reason))
685unifyField context (field, (expected, actual)) =
686 do result <- lift $ runExceptT $ subUnify context expected actual
687 case result of
688 Right () ->
689 return $ Nothing
691 Left (Mismatch maybeReason) ->
692 return $ Just (field, maybeReason)
696-- GATHER RECORD STRUCTURE
699data RecordStructure = RecordStructure
700 { _fields :: Map.Map Text Variable
701 , _extVar :: Variable
702 , _extStruct :: ExtensionStructure
703 }
706data ExtensionStructure
707 = Empty
708 | Extension
711gatherFields :: Context -> Map.Map Text Variable -> Variable -> Unify RecordStructure
712gatherFields context fields variable =
713 do desc <- liftIO (UF.descriptor variable)
714 case _content desc of
715 Structure (Record1 subFields subExt) ->
716 gatherFields context (Map.union fields subFields) subExt
718 Structure EmptyRecord1 ->
719 return (RecordStructure fields variable Empty)
721 Alias _ _ var ->
722 -- TODO may be dropping useful alias info here
723 gatherFields context fields var
725 _ ->
726 return (RecordStructure fields variable Extension)