on 3e23ef2 help sign in
elk/src/Type/Unify.hs
664 lines 20 kB history raw
1{-# OPTIONS_GHC -Wall #-}
2{-# LANGUAGE OverloadedStrings #-}
3module Type.Unify (unify) where
5import Control.Monad (liftM2, when, 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)
11import qualified AST.Variable as Var
12import qualified Reporting.Region as R
13import qualified Reporting.Error.Type as Error
14import qualified Type.Occurs as Occurs
15import qualified Type.State as TS
16import Type.Type as Type
17import qualified Type.UnionFind as UF
21-- KICK OFF UNIFICATION
24unify :: Error.Hint -> R.Region -> Variable -> Variable -> TS.Solver ()
25unify hint region expected actual =
26 {-# SCC elm_compiler_type_unify #-}
27 do result <- runExceptT (guardedUnify ExpectedActual expected actual)
28 case result of
29 Right () ->
30 return ()
32 Left problem ->
33 do expectedSrcType <- liftIO $ Type.toSrcType expected
34 actualSrcType <- liftIO $ Type.toSrcType actual
35 liftIO $ mergeHelp expected actual (Error "?") noRank
36 TS.addError region $
37 case problem of
38 Typical ->
39 Error.Mismatch $
40 Error.MismatchInfo hint expectedSrcType actualSrcType Nothing
42 Special reason ->
43 Error.Mismatch $
44 Error.MismatchInfo hint expectedSrcType actualSrcType (Just reason)
46 Infinite ->
47 Error.InfiniteType (Left hint) expectedSrcType
51-- UNIFICATION HELPERS
54type Unify =
55 ExceptT Problem TS.Solver
58data Context =
59 Context
60 { _orientation :: Orientation
61 , _first :: Variable
62 , _firstDesc :: Descriptor
63 , _second :: Variable
64 , _secondDesc :: Descriptor
65 }
68data Orientation = ExpectedActual | ActualExpected
71reorient :: Context -> Context
72reorient (Context orientation var1 desc1 var2 desc2) =
73 let
74 otherOrientation =
75 case orientation of
76 ExpectedActual -> ActualExpected
77 ActualExpected -> ExpectedActual
78 in
79 Context otherOrientation var2 desc2 var1 desc1
83-- ERROR MESSAGES
86data Problem
87 = Typical
88 | Special Error.Reason
89 | Infinite
92mismatch :: Context -> Maybe Error.Reason -> Unify a
93mismatch context@(Context orientation var1 _ var2 _) maybeReason =
94 do anyInfinite <- liftIO $ liftM2 (||) (Occurs.occurs var1) (Occurs.occurs var2)
95 when anyInfinite $ throwError Infinite
97 args1 <- liftIO $ collectArgs var1
98 args2 <- liftIO $ collectArgs var2
100 let numArgs1 = length args1
101 let numArgs2 = length args2
103 if numArgs1 == numArgs2
104 then
105 throwError $ reasonToProblem orientation maybeReason
106 else
107 do lift $ zipWithM_ (\a1 a2 -> runExceptT $ subUnify context a1 a2) args1 args2
108 throwError $ reasonToProblem orientation $ Just $
109 Error.MissingArgs $ abs (numArgs2 - numArgs1)
112reasonToProblem :: Orientation -> Maybe Error.Reason -> Problem
113reasonToProblem orientation maybeReason =
114 case maybeReason of
115 Nothing ->
116 Typical
118 Just reason ->
119 case orientation of
120 ExpectedActual ->
121 Special reason
123 ActualExpected ->
124 Special (Error.flipReason reason)
127badRigid :: Maybe Text -> Error.Reason
128badRigid maybeName =
129 Error.BadVar (Just (Error.Rigid maybeName)) Nothing
132badSuper :: Super -> Error.Reason
133badSuper super =
134 Error.BadVar (Just (errorSuper super)) Nothing
137badSupers :: Super -> Super -> Error.Reason
138badSupers super1 super2 =
139 Error.BadVar (Just (errorSuper super1)) (Just (errorSuper super2))
142doubleBad :: Error.VarType -> Error.VarType -> Error.Reason
143doubleBad vt1 vt2 =
144 Error.BadVar (Just vt1) (Just vt2)
147errorSuper :: Super -> Error.VarType
148errorSuper super =
149 case super of
150 Number ->
151 Error.Number
153 Comparable ->
154 Error.Comparable
156 Appendable ->
157 Error.Appendable
159 CompAppend ->
160 Error.CompAppend
164-- MERGE
167merge :: Context -> Content -> Unify ()
168merge (Context _ var1 (Descriptor _ rank1 _ _) var2 (Descriptor _ rank2 _ _)) content =
169 liftIO $ mergeHelp var1 var2 content (min rank1 rank2)
172mergeHelp :: Variable -> Variable -> Content -> Int -> IO ()
173mergeHelp var1 var2 newContent newRank =
174 UF.union var1 var2 $
175 Descriptor newContent newRank noMark Nothing
178fresh :: Context -> Content -> Unify Variable
179fresh (Context _ _ (Descriptor _ rank1 _ _) _ (Descriptor _ rank2 _ _)) content =
180 do freshVariable <-
181 liftIO $ UF.fresh $
182 Descriptor content (min rank1 rank2) noMark Nothing
183 lift (TS.register freshVariable)
187-- ACTUALLY UNIFY THINGS
190guardedUnify :: Orientation -> Variable -> Variable -> Unify ()
191guardedUnify orientation left right =
192 do equivalent <- liftIO $ UF.equivalent left right
193 if equivalent
194 then return ()
195 else
196 do leftDesc <- liftIO $ UF.descriptor left
197 rightDesc <- liftIO $ UF.descriptor right
198 actuallyUnify (Context orientation left leftDesc right rightDesc)
201subUnify :: Context -> Variable -> Variable -> Unify ()
202subUnify context var1 var2 =
203 guardedUnify (_orientation context) var1 var2
206actuallyUnify :: Context -> Unify ()
207actuallyUnify context@(Context _ _ (Descriptor firstContent _ _ _) _ (Descriptor secondContent _ _ _)) =
208 case firstContent of
209 Error _ ->
210 -- If there was an error, just pretend it is okay. This lets us avoid
211 -- "cascading" errors where one problem manifests as multiple message.
212 return ()
214 Var Flex Nothing _ ->
215 unifyFlex context secondContent
217 Var Flex (Just super) _ ->
218 unifyFlexSuper context super firstContent secondContent
220 Var Rigid maybeSuper maybeName ->
221 unifyRigid context maybeSuper maybeName firstContent secondContent
223 Alias name args realVar ->
224 unifyAlias context name args realVar secondContent
226 Structure term ->
227 unifyStructure context term firstContent secondContent
231-- UNIFY FLEXIBLE VARIABLES
234unifyFlex :: Context -> Content -> Unify ()
235unifyFlex context otherContent =
236 case otherContent of
237 Error _ ->
238 return ()
240 Var Flex _ _ ->
241 merge context otherContent
243 Var Rigid _ _ ->
244 merge context otherContent
246 Alias _ _ _ ->
247 merge context otherContent
249 Structure _ ->
250 merge context otherContent
254-- UNIFY RIGID VARIABLES
257unifyRigid :: Context -> Maybe Super -> Maybe Text -> Content -> Content -> Unify ()
258unifyRigid context maybeSuper maybeName content otherContent =
259 case otherContent of
260 Error _ ->
261 return ()
263 Var Flex otherMaybeSuper _ ->
264 case (maybeSuper, otherMaybeSuper) of
265 (_, Nothing) ->
266 merge context content
268 (Nothing, Just _) ->
269 mismatch context (Just (badRigid maybeName))
271 (Just super, Just otherSuper) ->
272 if combineRigidSupers super otherSuper then
273 merge context content
274 else
275 mismatch context (Just (badRigid maybeName))
277 Var Rigid _ otherMaybeName ->
278 mismatch context $ Just $
279 doubleBad (Error.Rigid maybeName) (Error.Rigid otherMaybeName)
281 Alias _ _ _ ->
282 mismatch context (Just (badRigid maybeName))
284 Structure _ ->
285 mismatch context (Just (badRigid maybeName))
289-- UNIFY SUPER VARIABLES
292unifyFlexSuper :: Context -> Super -> Content -> Content -> Unify ()
293unifyFlexSuper context super content otherContent =
294 case otherContent of
295 Structure term ->
296 unifyFlexSuperStructure context super term
298 Var Rigid Nothing maybeName ->
299 mismatch context (Just (doubleBad (errorSuper super) (Error.Rigid maybeName)))
301 Var Rigid (Just otherSuper) maybeName ->
302 if combineRigidSupers otherSuper super then
303 merge context otherContent
304 else
305 mismatch context $ Just $ badRigid maybeName
307 Var Flex Nothing _ ->
308 merge context content
310 Var Flex (Just otherSuper) _ ->
311 case super of
312 Number ->
313 case otherSuper of
314 Number -> merge context content
315 Comparable -> merge context content
316 _ -> mismatch context $ Just $ badSupers super otherSuper
318 Comparable ->
319 case otherSuper of
320 Comparable -> merge context otherContent
321 Number -> merge context otherContent
322 Appendable -> merge context (Var Flex (Just CompAppend) Nothing)
323 CompAppend -> merge context otherContent
325 Appendable ->
326 case otherSuper of
327 Appendable -> merge context otherContent
328 Comparable -> merge context (Var Flex (Just CompAppend) Nothing)
329 CompAppend -> merge context otherContent
330 Number -> mismatch context $ Just $ badSupers super otherSuper
332 CompAppend ->
333 case otherSuper of
334 Comparable -> merge context content
335 Appendable -> merge context content
336 CompAppend -> merge context content
337 Number -> mismatch context $ Just $ badSupers super otherSuper
339 Alias _ _ realVar ->
340 subUnify context (_first context) realVar
342 Error _ ->
343 return ()
346combineRigidSupers :: Super -> Super -> Bool
347combineRigidSupers rigid flex =
348 rigid == flex
349 || (rigid == Number && flex == Comparable)
350 || (rigid == CompAppend && (flex == Comparable || flex == Appendable))
353atomMatchesSuper :: Super -> Var.Canonical -> Bool
354atomMatchesSuper super name =
355 case super of
356 Number ->
357 elem name [ Var.int, Var.float ]
359 Comparable ->
360 elem name [ Var.string, Var.int, Var.float, Var.char]
362 Appendable ->
363 name == Var.string
365 CompAppend ->
366 name == Var.string
369unifyFlexSuperStructure :: Context -> Super -> FlatType -> Unify ()
370unifyFlexSuperStructure context super term =
371 do case term of
372 App1 name [] ->
373 if atomMatchesSuper super name then
374 merge context (Structure term)
375 else
376 mismatch context (Just (badSuper super))
378 App1 name [variable] | name == Var.list ->
379 case super of
380 Number ->
381 mismatch context (Just (badSuper super))
383 Appendable ->
384 merge context (Structure term)
386 Comparable ->
387 do comparableOccursCheck context
388 merge context (Structure term)
389 unifyComparableRecursive (_orientation context) variable
391 CompAppend ->
392 do comparableOccursCheck context
393 merge context (Structure term)
394 unifyComparableRecursive (_orientation context) variable
396 App1 name args | Var.isTuple name ->
397 case super of
398 Number ->
399 mismatch context (Just (badSuper super))
401 Appendable ->
402 mismatch context (Just (badSuper super))
404 Comparable ->
405 if length args > 6 then
406 mismatch context (Just (Error.TooLongComparableTuple (length args)))
408 else
409 do comparableOccursCheck context
410 merge context (Structure term)
411 mapM_ (unifyComparableRecursive (_orientation context)) args
413 CompAppend ->
414 mismatch context (Just (badSuper super))
416 _ ->
417 mismatch context (Just (badSuper super))
420-- TODO: is there some way to avoid doing this?
421-- Do type classes require occurs checks?
422comparableOccursCheck :: Context -> Unify ()
423comparableOccursCheck (Context _ _ _ var _) =
424 do hasOccurred <- liftIO $ Occurs.occurs var
425 if hasOccurred
426 then throwError Infinite
427 else return ()
430unifyComparableRecursive :: Orientation -> Variable -> Unify ()
431unifyComparableRecursive orientation var =
432 do compVar <- liftIO $
433 do (Descriptor _ rank _ _) <- UF.descriptor var
434 UF.fresh $ Descriptor (Var Flex (Just Comparable) Nothing) rank noMark Nothing
436 guardedUnify orientation compVar var
439collectArgs :: Variable -> IO [Variable]
440collectArgs variable =
441 collectArgsHelp [] variable
444collectArgsHelp :: [Variable] -> Variable -> IO [Variable]
445collectArgsHelp revArgs variable =
446 do (Descriptor content _ _ _) <- UF.descriptor variable
447 case content of
448 Structure (Fun1 arg returnType) ->
449 collectArgsHelp (arg : revArgs) returnType
451 _ ->
452 return $ variable : revArgs
456-- UNIFY ALIASES
459unifyAlias :: Context -> Var.Canonical -> [(Text, Variable)] -> Variable -> Content -> Unify ()
460unifyAlias context name args realVar otherContent =
461 case otherContent of
462 Error _ ->
463 return ()
465 Var Flex Nothing _ ->
466 merge context (Alias name args realVar)
468 Var _ _ _ ->
469 subUnify context realVar (_second context)
471 Alias otherName otherArgs otherRealVar ->
472 if name == otherName then
473 do zipWithM_ (subUnify context) (map snd args) (map snd otherArgs)
474 merge context otherContent
476 else
477 subUnify context realVar otherRealVar
479 Structure _ ->
480 subUnify context realVar (_second context)
484-- UNIFY STRUCTURES
487unifyStructure :: Context -> FlatType -> Content -> Content -> Unify ()
488unifyStructure context term content otherContent =
489 case otherContent of
490 Error _ ->
491 return ()
493 Var Flex Nothing _ ->
494 merge context content
496 Var Flex (Just super) _ ->
497 unifyFlexSuperStructure (reorient context) super term
499 Var Rigid _ maybeName ->
500 mismatch context (Just (Error.flipReason (badRigid maybeName)))
502 Alias _ _ realVar ->
503 subUnify context (_first context) realVar
505 Structure otherTerm ->
506 case (term, otherTerm) of
507 (App1 name args, App1 otherName otherArgs) ->
508 if name == otherName then
509 do zipWithM_ (subUnify context) args otherArgs
510 merge context otherContent
512 else if isIntFloat name otherName || isIntFloat otherName name then
513 mismatch context (Just Error.IntFloat)
515 else
516 mismatch context Nothing
518 (Fun1 arg result, Fun1 otherArg otherResult) ->
519 do subUnify context arg otherArg
520 subUnify context result otherResult
521 merge context otherContent
523 (EmptyRecord1, EmptyRecord1) ->
524 merge context otherContent
526 (Record1 fields ext, EmptyRecord1) | Map.null fields ->
527 subUnify context ext (_second context)
529 (EmptyRecord1, Record1 fields ext) | Map.null fields ->
530 subUnify context (_first context) ext
532 (Record1 fields extension, Record1 otherFields otherExtension) ->
533 do firstStructure <- liftIO $ gatherFields context fields extension
534 secondStructure <- liftIO $ gatherFields context otherFields otherExtension
535 unifyRecord context firstStructure secondStructure
537 _ ->
538 mismatch context Nothing
541isIntFloat :: Var.Canonical -> Var.Canonical -> Bool
542isIntFloat name otherName =
543 Var.isPrim "Int" name && Var.isPrim "Float" otherName
547-- UNIFY RECORDS
550unifyRecord :: Context -> RecordStructure -> RecordStructure -> Unify ()
551unifyRecord context firstStructure secondStructure =
552 do let (RecordStructure expFields expVar expStruct) = firstStructure
553 let (RecordStructure actFields actVar actStruct) = secondStructure
555 let sharedFields = Map.intersectionWith (,) expFields actFields
557 -- call after unifying extension, make sure record shape matches before
558 -- looking into whether the particular field types match.
559 let unifySharedFields otherFields ext =
560 do unifySharedFieldsHelp context sharedFields
561 let allFields = Map.union (Map.map fst sharedFields) otherFields
562 merge context (Structure (Record1 allFields ext))
564 let uniqueExpFields = Map.difference expFields actFields
565 let uniqueActFields = Map.difference actFields expFields
567 case (expStruct, Map.null uniqueExpFields, actStruct, Map.null uniqueActFields) of
568 (_, True, _, True) ->
569 do subUnify context expVar actVar
570 unifySharedFields Map.empty expVar
572 (Empty, _, _, False) ->
573 mismatch context $ Just $
574 Error.MessyFields (Map.keys sharedFields) (Map.keys uniqueExpFields) (Map.keys uniqueActFields)
576 (_, False, Empty, _) ->
577 mismatch context $ Just $
578 Error.MessyFields (Map.keys sharedFields) (Map.keys uniqueExpFields) (Map.keys uniqueActFields)
580 (_, False, _, True) ->
581 do subRecord <- fresh context (Structure (Record1 uniqueExpFields expVar))
582 subUnify context subRecord actVar
583 unifySharedFields Map.empty subRecord
585 (_, True, _, False) ->
586 do subRecord <- fresh context (Structure (Record1 uniqueActFields actVar))
587 subUnify context expVar subRecord
588 unifySharedFields Map.empty subRecord
590 (Extension, False, Extension, False) ->
591 do let subFields = Map.union uniqueExpFields uniqueActFields
592 subExt <- fresh context (Var Flex Nothing Nothing)
593 expRecord <- fresh context (Structure (Record1 uniqueActFields subExt))
594 actRecord <- fresh context (Structure (Record1 uniqueExpFields subExt))
595 subUnify context expVar expRecord
596 subUnify context actRecord actVar
597 unifySharedFields subFields subExt
601unifySharedFieldsHelp :: Context -> Map.Map Text (Variable, Variable) -> Unify ()
602unifySharedFieldsHelp context sharedFields =
603 do maybeBadFields <- traverse (unifyField context) (Map.toList sharedFields)
604 case Maybe.catMaybes maybeBadFields of
605 [] ->
606 return ()
608 badFields ->
609 mismatch context (Just (Error.BadFields (reverse badFields)))
612unifyField :: Context -> (Text, (Variable, Variable)) -> Unify (Maybe (Text, Maybe Error.Reason))
613unifyField context (field, (expected, actual)) =
614 do result <- lift $ runExceptT $ subUnify context expected actual
615 case result of
616 Right () ->
617 return $ Nothing
619 Left problem ->
620 return $ Just $ (,) field $
621 case problem of
622 Typical ->
623 Nothing
625 Special reason ->
626 Just reason
628 Infinite ->
629 Nothing
633-- GATHER RECORD STRUCTURE
636data RecordStructure = RecordStructure
637 { _fields :: Map.Map Text Variable
638 , _extVar :: Variable
639 , _extStruct :: ExtensionStructure
640 }
643data ExtensionStructure
644 = Empty
645 | Extension
648gatherFields :: Context -> Map.Map Text Variable -> Variable -> IO RecordStructure
649gatherFields context fields variable =
650 do (Descriptor content _ _ _) <- UF.descriptor variable
651 case content of
652 Structure (Record1 subFields subExt) ->
653 gatherFields context (Map.union fields subFields) subExt
655 Structure EmptyRecord1 ->
656 return (RecordStructure fields variable Empty)
658 Alias _ _ var ->
659 -- TODO may be dropping useful alias info here
660 gatherFields context fields var
662 _ ->
663 return (RecordStructure fields variable Extension)