git.iko.soy/elk
on dcce951 help sign in
elk/src/Type/Unify.hs
725 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)
549 Alias otherName otherArgs otherRealVar ->
550 if name == otherName then
551 do zipWithM_ (subUnify context) (map snd args) (map snd otherArgs)
552 merge context otherContent
554 else
555 subUnify context realVar otherRealVar
557 Structure _ ->
558 subUnify context realVar (_second context)
562-- UNIFY STRUCTURES
565unifyStructure :: Context -> Term1 Variable -> Content -> Unify ()
566unifyStructure context term otherContent =
567 case otherContent of
568 Error ->
569 return ()
571 Var Flex Nothing _ ->
572 merge context (Structure term)
574 Var Flex (Just super) _ ->
575 unifySuper (reorient context) super (Structure term)
577 Var Rigid _ maybeName ->
578 mismatch context (Just (Error.flipReason (badRigid maybeName)))
580 Atom _ ->
581 mismatch context Nothing
583 Alias _ _ realVar ->
584 subUnify context (_first context) realVar
586 Structure otherTerm ->
587 case (term, otherTerm) of
588 (App1 func arg, App1 otherFunc otherArg) ->
589 do subUnify context func otherFunc
590 subUnify context arg otherArg
591 merge context otherContent
593 (Fun1 arg result, Fun1 otherArg otherResult) ->
594 do subUnify context arg otherArg
595 subUnify context result otherResult
596 merge context otherContent
598 (EmptyRecord1, EmptyRecord1) ->
599 merge context otherContent
601 (Record1 fields ext, EmptyRecord1) | Map.null fields ->
602 subUnify context ext (_second context)
604 (EmptyRecord1, Record1 fields ext) | Map.null fields ->
605 subUnify context (_first context) ext
607 (Record1 fields extension, Record1 otherFields otherExtension) ->
608 do firstStructure <- gatherFields context fields extension
609 secondStructure <- gatherFields context otherFields otherExtension
610 unifyRecord context firstStructure secondStructure
612 _ ->
613 mismatch context Nothing
617-- UNIFY RECORDS
620unifyRecord :: Context -> RecordStructure -> RecordStructure -> Unify ()
621unifyRecord context firstStructure secondStructure =
622 do let (RecordStructure expFields expVar expStruct) = firstStructure
623 let (RecordStructure actFields actVar actStruct) = secondStructure
625 let sharedFields = Map.intersectionWith (,) expFields actFields
627 -- call after unifying extension, make sure record shape matches before
628 -- looking into whether the particular field types match.
629 let unifySharedFields otherFields ext =
630 do unifySharedFieldsHelp context sharedFields
631 let allFields = Map.union (Map.map fst sharedFields) otherFields
632 merge context (Structure (Record1 allFields ext))
634 let uniqueExpFields = Map.difference expFields actFields
635 let uniqueActFields = Map.difference actFields expFields
637 case (expStruct, Map.null uniqueExpFields, actStruct, Map.null uniqueActFields) of
638 (_, True, _, True) ->
639 do subUnify context expVar actVar
640 unifySharedFields Map.empty expVar
642 (Empty, _, _, False) ->
643 mismatch context $ Just $
644 Error.MessyFields (Map.keys sharedFields) (Map.keys uniqueExpFields) (Map.keys uniqueActFields)
646 (_, False, Empty, _) ->
647 mismatch context $ Just $
648 Error.MessyFields (Map.keys sharedFields) (Map.keys uniqueExpFields) (Map.keys uniqueActFields)
650 (_, False, _, True) ->
651 do subRecord <- fresh context (Structure (Record1 uniqueExpFields expVar))
652 subUnify context subRecord actVar
653 unifySharedFields Map.empty subRecord
655 (_, True, _, False) ->
656 do subRecord <- fresh context (Structure (Record1 uniqueActFields actVar))
657 subUnify context expVar subRecord
658 unifySharedFields Map.empty subRecord
660 (Extension, False, Extension, False) ->
661 do let subFields = Map.union uniqueExpFields uniqueActFields
662 subExt <- fresh context (Var Flex Nothing Nothing)
663 expRecord <- fresh context (Structure (Record1 uniqueActFields subExt))
664 actRecord <- fresh context (Structure (Record1 uniqueExpFields subExt))
665 subUnify context expVar expRecord
666 subUnify context actRecord actVar
667 unifySharedFields subFields subExt
671unifySharedFieldsHelp :: Context -> Map.Map String (Variable, Variable) -> Unify ()
672unifySharedFieldsHelp context sharedFields =
673 do maybeBadFields <- traverse (unifyField context) (Map.toList sharedFields)
674 case Maybe.catMaybes maybeBadFields of
675 [] ->
676 return ()
678 badFields ->
679 mismatch context (Just (Error.BadFields (reverse badFields)))
682unifyField :: Context -> (String, (Variable, Variable)) -> Unify (Maybe (String, Maybe Error.Reason))
683unifyField context (field, (expected, actual)) =
684 do result <- lift $ runExceptT $ subUnify context expected actual
685 case result of
686 Right () ->
687 return $ Nothing
689 Left (Mismatch maybeReason) ->
690 return $ Just (field, maybeReason)
694-- GATHER RECORD STRUCTURE
697data RecordStructure = RecordStructure
698 { _fields :: Map.Map String Variable
699 , _extVar :: Variable
700 , _extStruct :: ExtensionStructure
701 }
704data ExtensionStructure
705 = Empty
706 | Extension
709gatherFields :: Context -> Map.Map String Variable -> Variable -> Unify RecordStructure
710gatherFields context fields variable =
711 do desc <- liftIO (UF.descriptor variable)
712 case _content desc of
713 Structure (Record1 subFields subExt) ->
714 gatherFields context (Map.union fields subFields) subExt
716 Structure EmptyRecord1 ->
717 return (RecordStructure fields variable Empty)
719 Alias _ _ var ->
720 -- TODO may be dropping useful alias info here
721 gatherFields context fields var
723 _ ->
724 return (RecordStructure fields variable Extension)