on b09bb00 help sign in
elk/src/Type/Unify.hs
728 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 qualified Data.Text as Text
10import Data.Text (Text)
11import qualified Data.UnionFind.IO as UF
13import qualified AST.Variable as Var
14import qualified Reporting.Region as R
15import qualified Reporting.Error.Type as Error
16import qualified Type.State as TS
17import Type.Type as Type
21-- KICK OFF UNIFICATION
24unify :: Error.Hint -> R.Region -> Variable -> Variable -> TS.Solver ()
25unify hint region expected actual =
26 do result <- runExceptT (guardedUnify ExpectedActual expected actual)
27 case result of
28 Right () ->
29 return ()
31 Left (Mismatch maybeReason) ->
32 let
33 mkError =
34 do expectedSrcType <- Type.toSrcType expected
35 actualSrcType <- Type.toSrcType actual
36 mergeHelp expected actual Error
37 let info = Error.MismatchInfo hint expectedSrcType actualSrcType maybeReason
38 return (Error.Mismatch info)
39 in
40 TS.addError region =<< liftIO mkError
44-- UNIFICATION HELPERS
47type Unify =
48 ExceptT Mismatch TS.Solver
51data Context = Context
52 { _orientation :: Orientation
53 , _first :: Variable
54 , _firstDesc :: Descriptor
55 , _second :: Variable
56 , _secondDesc :: Descriptor
57 }
60data Orientation = ExpectedActual | ActualExpected
63reorient :: Context -> Context
64reorient (Context orientation var1 desc1 var2 desc2) =
65 let
66 otherOrientation =
67 case orientation of
68 ExpectedActual -> ActualExpected
69 ActualExpected -> ExpectedActual
70 in
71 Context otherOrientation var2 desc2 var1 desc1
75-- ERROR MESSAGES
78newtype Mismatch =
79 Mismatch (Maybe Error.Reason)
82mismatch :: Context -> Maybe Error.Reason -> Unify a
83mismatch context@(Context orientation var1 _ var2 _) maybeReason =
84 do args1 <- liftIO $ collectArgs var1
85 args2 <- liftIO $ collectArgs var2
87 let numArgs1 = length args1
88 let numArgs2 = length args2
90 if numArgs1 == numArgs2
91 then
92 mismatchHelp orientation maybeReason
93 else
94 do zipWithM_ (\arg1 arg2 -> lift $ runExceptT $ subUnify context arg1 arg2) args1 args2
95 mismatchHelp orientation $ Just $ Error.MissingArgs $ abs (numArgs2 - numArgs1)
98mismatchHelp :: Orientation -> Maybe Error.Reason -> Unify a
99mismatchHelp orientation maybeReason =
100 throwError $ Mismatch $
101 case orientation of
102 ExpectedActual ->
103 maybeReason
105 ActualExpected ->
106 Error.flipReason <$> maybeReason
109badRigid :: Maybe Text -> Error.Reason
110badRigid maybeName =
111 Error.BadVar (Just (Error.Rigid maybeName)) Nothing
114badSuper :: Super -> Error.Reason
115badSuper super =
116 Error.BadVar (Just (errorSuper super)) Nothing
119doubleBad :: Error.VarType -> Error.VarType -> Error.Reason
120doubleBad vt1 vt2 =
121 Error.BadVar (Just vt1) (Just vt2)
124errorSuper :: Super -> Error.VarType
125errorSuper super =
126 case super of
127 Number ->
128 Error.Number
130 Comparable ->
131 Error.Comparable
133 Appendable ->
134 Error.Appendable
136 CompAppend ->
137 Error.CompAppend
141-- MERGE
144merge :: Context -> Content -> Unify ()
145merge (Context _ first _ second _) content =
146 liftIO $ mergeHelp first second content
149mergeHelp :: Variable -> Variable -> Content -> IO ()
150mergeHelp first second content =
151 UF.union' first second $ \desc1 desc2 ->
152 return $
153 Descriptor
154 { _content = content
155 , _rank = min (_rank desc1) (_rank desc2)
156 , _mark = noMark
157 , _copy = Nothing
158 }
161fresh :: Context -> Content -> Unify Variable
162fresh (Context _ _ desc1 _ desc2) content =
163 do freshVariable <-
164 liftIO $ UF.fresh $
165 Descriptor
166 { _content = content
167 , _rank = min (_rank desc1) (_rank desc2)
168 , _mark = noMark
169 , _copy = Nothing
170 }
171 lift (TS.register freshVariable)
175-- ACTUALLY UNIFY THINGS
178guardedUnify :: Orientation -> Variable -> Variable -> Unify ()
179guardedUnify orientation left right =
180 do equivalent <- liftIO $ UF.equivalent left right
181 if equivalent
182 then return ()
183 else
184 do leftDesc <- liftIO $ UF.descriptor left
185 rightDesc <- liftIO $ UF.descriptor right
186 actuallyUnify (Context orientation left leftDesc right rightDesc)
189subUnify :: Context -> Variable -> Variable -> Unify ()
190subUnify context var1 var2 =
191 guardedUnify (_orientation context) var1 var2
194actuallyUnify :: Context -> Unify ()
195actuallyUnify context@(Context _ _ firstDesc _ secondDesc) =
196 let
197 secondContent = _content secondDesc
198 in
199 case _content firstDesc of
200 Error ->
201 -- If there was an error, just pretend it is okay. This lets us avoid
202 -- "cascading" errors where one problem manifests as multiple message.
203 return ()
205 Var Flex Nothing _ ->
206 unifyFlex context secondContent
208 Var Flex (Just super) _ ->
209 unifySuper context super secondContent
211 Var Rigid maybeSuper maybeName ->
212 unifyRigid context maybeSuper maybeName secondContent
214 Atom name ->
215 unifyAtom context name secondContent
217 Alias name args realVar ->
218 unifyAlias context name args realVar secondContent
220 Structure term ->
221 unifyStructure context term secondContent
225-- UNIFY FLEXIBLE VARIABLES
228unifyFlex :: Context -> Content -> Unify ()
229unifyFlex context otherContent =
230 case otherContent of
231 Error ->
232 return ()
234 Var Flex _ _ ->
235 merge context otherContent
237 Var Rigid _ _ ->
238 merge context otherContent
240 Atom _ ->
241 merge context otherContent
243 Alias _ _ _ ->
244 merge context otherContent
246 Structure _ ->
247 merge context otherContent
251-- UNIFY RIGID VARIABLES
254unifyRigid :: Context -> Maybe Super -> Maybe Text -> Content -> Unify ()
255unifyRigid context maybeSuper maybeName otherContent =
256 case otherContent of
257 Error ->
258 return ()
260 Var Flex otherMaybeSuper _ ->
261 case (maybeSuper, otherMaybeSuper) of
262 (_, Nothing) ->
263 merge context (Var Rigid maybeSuper maybeName)
265 (Nothing, Just _) ->
266 mismatch context (Just (badRigid maybeName))
268 (Just super, Just otherSuper) ->
269 case combineSupers super otherSuper of
270 Right newSuper | newSuper == otherSuper ->
271 merge context otherContent
273 _ ->
274 mismatch context (Just (badRigid maybeName))
276 Var Rigid _ otherMaybeName ->
277 mismatch context $ Just $
278 doubleBad (Error.Rigid maybeName) (Error.Rigid otherMaybeName)
280 Atom _ ->
281 mismatch context (Just (badRigid maybeName))
283 Alias _ _ _ ->
284 mismatch context (Just (badRigid maybeName))
286 Structure _ ->
287 mismatch context (Just (badRigid maybeName))
291-- UNIFY SUPER VARIABLES
294unifySuper :: Context -> Super -> Content -> Unify ()
295unifySuper context super otherContent =
296 case otherContent of
297 Structure term ->
298 unifySuperStructure context super term
300 Atom name ->
301 if atomMatchesSuper super name then
302 merge context otherContent
303 else
304 mismatch context (Just (badSuper super))
306 Var Rigid Nothing maybeName ->
307 mismatch context (Just (doubleBad (errorSuper super) (Error.Rigid maybeName)))
309 Var Rigid (Just otherSuper) maybeName ->
310 case combineSupers super otherSuper of
311 Right newSuper | newSuper == super ->
312 merge context otherContent
314 _ ->
315 mismatch context $ Just $
316 doubleBad (errorSuper super) (Error.Rigid maybeName)
318 Var Flex Nothing _ ->
319 merge context (Var Flex (Just super) Nothing)
321 Var Flex (Just otherSuper) _ ->
322 case combineSupers super otherSuper of
323 Left reason ->
324 mismatch context (Just reason)
326 Right newSuper ->
327 merge context (Var Flex (Just newSuper) Nothing)
329 Alias _ _ realVar ->
330 subUnify context (_first context) realVar
332 Error ->
333 return ()
336combineSupers :: Super -> Super -> Either Error.Reason Super
337combineSupers firstSuper secondSuper =
338 case (firstSuper, secondSuper) of
339 (Number , Number ) -> Right Number
340 (Comparable, Number ) -> Right Number
341 (Number , Comparable) -> Right Number
343 (Comparable, Comparable) -> Right Comparable
344 (Appendable, Appendable) -> Right Appendable
346 (Appendable, Comparable) -> Right CompAppend
347 (Comparable, Appendable) -> Right CompAppend
349 (CompAppend, CompAppend) -> Right CompAppend
350 (CompAppend, Comparable) -> Right CompAppend
351 (Comparable, CompAppend) -> Right CompAppend
352 (CompAppend, Appendable) -> Right CompAppend
353 (Appendable, CompAppend) -> Right CompAppend
355 (_ , _ ) ->
356 Left $ doubleBad (errorSuper firstSuper) (errorSuper secondSuper)
359isPrimitiveFrom :: [Text] -> Var.Canonical -> Bool
360isPrimitiveFrom prims var =
361 any (\p -> Var.isPrim p var) prims
364atomMatchesSuper :: Super -> Var.Canonical -> Bool
365atomMatchesSuper super name =
366 case super of
367 Number ->
368 isPrimitiveFrom ["Int", "Float"] name
370 Comparable ->
371 isPrimitiveFrom ["Int", "Float", "Char", "String"] name
373 Appendable ->
374 Var.isPrim "String" name
376 CompAppend ->
377 Var.isPrim "String" name
380unifySuperStructure :: Context -> Super -> Term1 Variable -> Unify ()
381unifySuperStructure context super term =
382 do appStructure <- liftIO (collectApps (Structure term))
383 case appStructure of
384 Other ->
385 mismatch context (Just (badSuper super))
387 List variable ->
388 case super of
389 Number ->
390 mismatch context (Just (badSuper super))
392 Appendable ->
393 merge context (Structure term)
395 Comparable ->
396 do merge context (Structure term)
397 unifyComparableRecursive (_orientation context) variable
399 CompAppend ->
400 do merge context (Structure term)
401 unifyComparableRecursive (_orientation context) variable
403 Tuple entries ->
404 case super of
405 Number ->
406 mismatch context (Just (badSuper super))
408 Appendable ->
409 mismatch context (Just (badSuper super))
411 Comparable ->
412 if length entries > 6 then
413 mismatch context (Just (Error.TooLongComparableTuple (length entries)))
415 else
416 do merge context (Structure term)
417 mapM_ (unifyComparableRecursive (_orientation context)) entries
419 CompAppend ->
420 mismatch context (Just (badSuper super))
423unifyComparableRecursive :: Orientation -> Variable -> Unify ()
424unifyComparableRecursive orientation var =
425 do compVar <-
426 liftIO $
427 do desc <- UF.descriptor var
428 UF.fresh $
429 Descriptor
430 { _content = Var Flex (Just Comparable) Nothing
431 , _rank = _rank desc
432 , _mark = noMark
433 , _copy = Nothing
434 }
436 guardedUnify orientation compVar var
439data AppStructure
440 = List Variable
441 | Tuple [Variable]
442 | Other
445collectApps :: Content -> IO AppStructure
446collectApps content =
447 collectAppsHelp [] content
450collectAppsHelp :: [Variable] -> Content -> IO AppStructure
451collectAppsHelp args content =
452 case (content, args) of
453 (Structure (App1 func arg), _) ->
454 collectAppsHelp (args ++ [arg]) =<< getContent func
456 (Atom name, [arg]) | Var.isList name ->
457 return (List arg)
459 (Atom name, _) | Var.isTuple name ->
460 return (Tuple args)
462 _ ->
463 return Other
466collectArgs :: Variable -> IO [Variable]
467collectArgs variable =
468 collectArgsHelp [] variable
471collectArgsHelp :: [Variable] -> Variable -> IO [Variable]
472collectArgsHelp revArgs variable =
473 do content <- getContent variable
474 case content of
475 Structure (Fun1 arg returnType) ->
476 collectArgsHelp (arg : revArgs) returnType
478 _ ->
479 return $ variable : revArgs
482getContent :: Variable -> IO Content
483getContent variable =
484 _content <$> UF.descriptor variable
488-- UNIFY ATOMS
491unifyAtom :: Context -> Var.Canonical -> Content -> Unify ()
492unifyAtom context name otherContent =
493 case otherContent of
494 Error ->
495 return ()
497 Var Flex Nothing _ ->
498 merge context (Atom name)
500 Var Flex (Just super) _ ->
501 if atomMatchesSuper super name then
502 merge context (Atom name)
504 else
505 mismatch context (Just ((Error.flipReason (badSuper super))))
507 Var Rigid _ maybeName ->
508 mismatch context (Just (Error.flipReason (badRigid maybeName)))
510 Atom otherName ->
511 if name == otherName then
512 merge context otherContent
514 else
515 mismatch context $
516 if isIntFloat name otherName || isIntFloat otherName name then
517 Just Error.IntFloat
518 else
519 Nothing
521 Alias _ _ realVar ->
522 subUnify context (_first context) realVar
524 Structure _ ->
525 mismatch context Nothing
528isIntFloat :: Var.Canonical -> Var.Canonical -> Bool
529isIntFloat name otherName =
530 Var.isPrim "Int" name && Var.isPrim "Float" otherName
534-- UNIFY ALIASES
537unifyAlias :: Context -> Var.Canonical -> [(Text, Variable)] -> Variable -> Content -> Unify ()
538unifyAlias context name args realVar otherContent =
539 case otherContent of
540 Error ->
541 return ()
543 Var Flex Nothing _ ->
544 merge context (Alias name args realVar)
546 Var _ _ _ ->
547 subUnify context realVar (_second context)
549 Atom _ ->
550 subUnify context realVar (_second context)
552 Alias otherName otherArgs otherRealVar ->
553 if name == otherName then
554 do zipWithM_ (subUnify context) (map snd args) (map snd otherArgs)
555 merge context otherContent
557 else
558 subUnify context realVar otherRealVar
560 Structure _ ->
561 subUnify context realVar (_second context)
565-- UNIFY STRUCTURES
568unifyStructure :: Context -> Term1 Variable -> Content -> Unify ()
569unifyStructure context term otherContent =
570 case otherContent of
571 Error ->
572 return ()
574 Var Flex Nothing _ ->
575 merge context (Structure term)
577 Var Flex (Just super) _ ->
578 unifySuper (reorient context) super (Structure term)
580 Var Rigid _ maybeName ->
581 mismatch context (Just (Error.flipReason (badRigid maybeName)))
583 Atom _ ->
584 mismatch context Nothing
586 Alias _ _ realVar ->
587 subUnify context (_first context) realVar
589 Structure otherTerm ->
590 case (term, otherTerm) of
591 (App1 func arg, App1 otherFunc otherArg) ->
592 do subUnify context func otherFunc
593 subUnify context arg otherArg
594 merge context otherContent
596 (Fun1 arg result, Fun1 otherArg otherResult) ->
597 do subUnify context arg otherArg
598 subUnify context result otherResult
599 merge context otherContent
601 (EmptyRecord1, EmptyRecord1) ->
602 merge context otherContent
604 (Record1 fields ext, EmptyRecord1) | Map.null fields ->
605 subUnify context ext (_second context)
607 (EmptyRecord1, Record1 fields ext) | Map.null fields ->
608 subUnify context (_first context) ext
610 (Record1 fields extension, Record1 otherFields otherExtension) ->
611 do firstStructure <- gatherFields context fields extension
612 secondStructure <- gatherFields context otherFields otherExtension
613 unifyRecord context firstStructure secondStructure
615 _ ->
616 mismatch context Nothing
620-- UNIFY RECORDS
623unifyRecord :: Context -> RecordStructure -> RecordStructure -> Unify ()
624unifyRecord context firstStructure secondStructure =
625 do let (RecordStructure expFields expVar expStruct) = firstStructure
626 let (RecordStructure actFields actVar actStruct) = secondStructure
628 let sharedFields = Map.intersectionWith (,) expFields actFields
630 -- call after unifying extension, make sure record shape matches before
631 -- looking into whether the particular field types match.
632 let unifySharedFields otherFields ext =
633 do unifySharedFieldsHelp context sharedFields
634 let allFields = Map.union (Map.map fst sharedFields) otherFields
635 merge context (Structure (Record1 allFields ext))
637 let uniqueExpFields = Map.difference expFields actFields
638 let uniqueActFields = Map.difference actFields expFields
640 case (expStruct, Map.null uniqueExpFields, actStruct, Map.null uniqueActFields) of
641 (_, True, _, True) ->
642 do subUnify context expVar actVar
643 unifySharedFields Map.empty expVar
645 (Empty, _, _, False) ->
646 mismatch context $ Just $
647 Error.MessyFields (Map.keys sharedFields) (Map.keys uniqueExpFields) (Map.keys uniqueActFields)
649 (_, False, Empty, _) ->
650 mismatch context $ Just $
651 Error.MessyFields (Map.keys sharedFields) (Map.keys uniqueExpFields) (Map.keys uniqueActFields)
653 (_, False, _, True) ->
654 do subRecord <- fresh context (Structure (Record1 uniqueExpFields expVar))
655 subUnify context subRecord actVar
656 unifySharedFields Map.empty subRecord
658 (_, True, _, False) ->
659 do subRecord <- fresh context (Structure (Record1 uniqueActFields actVar))
660 subUnify context expVar subRecord
661 unifySharedFields Map.empty subRecord
663 (Extension, False, Extension, False) ->
664 do let subFields = Map.union uniqueExpFields uniqueActFields
665 subExt <- fresh context (Var Flex Nothing Nothing)
666 expRecord <- fresh context (Structure (Record1 uniqueActFields subExt))
667 actRecord <- fresh context (Structure (Record1 uniqueExpFields subExt))
668 subUnify context expVar expRecord
669 subUnify context actRecord actVar
670 unifySharedFields subFields subExt
674unifySharedFieldsHelp :: Context -> Map.Map Text (Variable, Variable) -> Unify ()
675unifySharedFieldsHelp context sharedFields =
676 do maybeBadFields <- traverse (unifyField context) (Map.toList sharedFields)
677 case Maybe.catMaybes maybeBadFields of
678 [] ->
679 return ()
681 badFields ->
682 mismatch context (Just (Error.BadFields (reverse badFields)))
685unifyField :: Context -> (Text, (Variable, Variable)) -> Unify (Maybe (String, Maybe Error.Reason))
686unifyField context (field, (expected, actual)) =
687 do result <- lift $ runExceptT $ subUnify context expected actual
688 case result of
689 Right () ->
690 return $ Nothing
692 Left (Mismatch maybeReason) ->
693 return $ Just (Text.unpack field, maybeReason)
697-- GATHER RECORD STRUCTURE
700data RecordStructure = RecordStructure
701 { _fields :: Map.Map Text Variable
702 , _extVar :: Variable
703 , _extStruct :: ExtensionStructure
704 }
707data ExtensionStructure
708 = Empty
709 | Extension
712gatherFields :: Context -> Map.Map Text Variable -> Variable -> Unify RecordStructure
713gatherFields context fields variable =
714 do desc <- liftIO (UF.descriptor variable)
715 case _content desc of
716 Structure (Record1 subFields subExt) ->
717 gatherFields context (Map.union fields subFields) subExt
719 Structure EmptyRecord1 ->
720 return (RecordStructure fields variable Empty)
722 Alias _ _ var ->
723 -- TODO may be dropping useful alias info here
724 gatherFields context fields var
726 _ ->
727 return (RecordStructure fields variable Extension)