on f4401ac help sign in
elk/compiler/src/Type/Solve.hs
720 lines 21 kB history raw
1{-# OPTIONS_GHC -Wall #-}
2{-# LANGUAGE OverloadedStrings #-}
3module Type.Solve
4 ( run
5 )
6 where
9import Control.Monad
10import qualified Data.Map.Strict as Map
11import Data.Map.Strict ((!))
12import qualified Data.Name as Name
13import qualified Data.NonEmptyList as NE
14import qualified Data.Vector as Vector
15import qualified Data.Vector.Mutable as MVector
17import qualified AST.Canonical as Can
18import qualified Reporting.Annotation as A
19import qualified Reporting.Error.Type as Error
20import qualified Reporting.Render.Type as RT
21import qualified Reporting.Render.Type.Localizer as L
22import qualified Type.Occurs as Occurs
23import Type.Type as Type
24import qualified Type.Error as ET
25import qualified Type.Unify as Unify
26import qualified Type.UnionFind as UF
30-- RUN SOLVER
33run :: Constraint -> IO (Either (NE.List Error.Error) (Map.Map Name.Name Can.Annotation))
34run constraint =
35 do pools <- MVector.replicate 8 []
37 (State env _ errors) <-
38 solve Map.empty outermostRank pools emptyState constraint
40 case errors of
41 [] ->
42 Right <$> traverse Type.toAnnotation env
44 e:es ->
45 return $ Left (NE.List e es)
49{-# NOINLINE emptyState #-}
50emptyState :: State
51emptyState =
52 State Map.empty (nextMark noMark) []
56-- SOLVER
59type Env =
60 Map.Map Name.Name Variable
63type Pools =
64 MVector.IOVector [Variable]
67data State =
68 State
69 { _env :: Env
70 , _mark :: Mark
71 , _errors :: [Error.Error]
72 }
75solve :: Env -> Int -> Pools -> State -> Constraint -> IO State
76solve env rank pools state constraint =
77 case constraint of
78 CTrue ->
79 return state
81 CSaveTheEnvironment ->
82 return (state { _env = env })
84 CEqual region category tipe expectation ->
85 do actual <- typeToVariable rank pools tipe
86 expected <- expectedToVariable rank pools expectation
87 answer <- Unify.unify actual expected
88 case answer of
89 Unify.Ok vars ->
90 do introduce rank pools vars
91 return state
93 Unify.Err vars actualType expectedType ->
94 do introduce rank pools vars
95 return $ addError state $
96 Error.BadExpr region category actualType $
97 Error.typeReplace expectation expectedType
99 CLocal region name expectation ->
100 do actual <- makeCopy rank pools (env ! name)
101 expected <- expectedToVariable rank pools expectation
102 answer <- Unify.unify actual expected
103 case answer of
104 Unify.Ok vars ->
105 do introduce rank pools vars
106 return state
108 Unify.Err vars actualType expectedType ->
109 do introduce rank pools vars
110 return $ addError state $
111 Error.BadExpr region (Error.Local name) actualType $
112 Error.typeReplace expectation expectedType
114 CForeign region name (Can.Forall freeVars srcType) expectation ->
115 do actual <- srcTypeToVariable rank pools freeVars srcType
116 expected <- expectedToVariable rank pools expectation
117 answer <- Unify.unify actual expected
118 case answer of
119 Unify.Ok vars ->
120 do introduce rank pools vars
121 return state
123 Unify.Err vars actualType expectedType ->
124 do introduce rank pools vars
125 return $ addError state $
126 Error.BadExpr region (Error.Foreign name) actualType $
127 Error.typeReplace expectation expectedType
129 CPattern region category tipe expectation ->
130 do actual <- typeToVariable rank pools tipe
131 expected <- patternExpectationToVariable rank pools expectation
132 answer <- Unify.unify actual expected
133 case answer of
134 Unify.Ok vars ->
135 do introduce rank pools vars
136 return state
138 Unify.Err vars actualType expectedType ->
139 do introduce rank pools vars
140 return $ addError state $
141 Error.BadPattern region category actualType
142 (Error.ptypeReplace expectation expectedType)
144 CAnd constraints ->
145 foldM (solve env rank pools) state constraints
147 CLet [] flexs _ headerCon CTrue ->
148 do introduce rank pools flexs
149 solve env rank pools state headerCon
151 CLet [] [] header headerCon subCon ->
152 do state1 <- solve env rank pools state headerCon
153 locals <- traverse (A.traverse (typeToVariable rank pools)) header
154 let newEnv = Map.union env (Map.map A.toValue locals)
155 state2 <- solve newEnv rank pools state1 subCon
156 foldM occurs state2 $ Map.toList locals
158 CLet rigids flexs header headerCon subCon ->
159 do
160 -- work in the next pool to localize header
161 let nextRank = rank + 1
162 let poolsLength = MVector.length pools
163 nextPools <-
164 if nextRank < poolsLength
165 then return pools
166 else MVector.grow pools poolsLength
168 -- introduce variables
169 let vars = rigids ++ flexs
170 forM_ vars $ \var ->
171 UF.modify var $ \(Descriptor content _ mark copy) ->
172 Descriptor content nextRank mark copy
173 MVector.write nextPools nextRank vars
175 -- run solver in next pool
176 locals <- traverse (A.traverse (typeToVariable nextRank nextPools)) header
177 (State savedEnv mark errors) <-
178 solve env nextRank nextPools state headerCon
180 let youngMark = mark
181 let visitMark = nextMark youngMark
182 let finalMark = nextMark visitMark
184 -- pop pool
185 generalize youngMark visitMark nextRank nextPools
186 MVector.write nextPools nextRank []
188 -- check that things went well
189 mapM_ isGeneric rigids
191 let newEnv = Map.union env (Map.map A.toValue locals)
192 let tempState = State savedEnv finalMark errors
193 newState <- solve newEnv rank nextPools tempState subCon
195 foldM occurs newState (Map.toList locals)
198-- Check that a variable has rank == noRank, meaning that it can be generalized.
199isGeneric :: Variable -> IO ()
200isGeneric var =
201 do (Descriptor _ rank _ _) <- UF.get var
202 if rank == noRank
203 then return ()
204 else
205 do tipe <- Type.toErrorType var
206 error $
207 "You ran into a compiler bug. Here are some details for the developers:\n\n"
208 ++ " " ++ show (ET.toDoc L.empty RT.None tipe) ++ " [rank = " ++ show rank ++ "]\n\n"
209 ++
210 "Please create an <http://sscce.org/> and then report it\n\
211 \at <https://github.com/elm/compiler/issues>\n\n"
215-- EXPECTATIONS TO VARIABLE
218expectedToVariable :: Int -> Pools -> Error.Expected Type -> IO Variable
219expectedToVariable rank pools expectation =
220 typeToVariable rank pools $
221 case expectation of
222 Error.NoExpectation tipe ->
223 tipe
225 Error.FromContext _ _ tipe ->
226 tipe
228 Error.FromAnnotation _ _ _ tipe ->
229 tipe
232patternExpectationToVariable :: Int -> Pools -> Error.PExpected Type -> IO Variable
233patternExpectationToVariable rank pools expectation =
234 typeToVariable rank pools $
235 case expectation of
236 Error.PNoExpectation tipe ->
237 tipe
239 Error.PFromContext _ _ tipe ->
240 tipe
244-- ERROR HELPERS
247addError :: State -> Error.Error -> State
248addError (State savedEnv rank errors) err =
249 State savedEnv rank (err:errors)
253-- OCCURS CHECK
256occurs :: State -> (Name.Name, A.Located Variable) -> IO State
257occurs state (name, A.At region variable) =
258 do hasOccurred <- Occurs.occurs variable
259 if hasOccurred
260 then
261 do errorType <- Type.toErrorType variable
262 (Descriptor _ rank mark copy) <- UF.get variable
263 UF.set variable (Descriptor Error rank mark copy)
264 return $ addError state (Error.InfiniteType region name errorType)
265 else
266 return state
270-- GENERALIZE
273{-| Every variable has rank less than or equal to the maxRank of the pool.
274This sorts variables into the young and old pools accordingly.
275-}
276generalize :: Mark -> Mark -> Int -> Pools -> IO ()
277generalize youngMark visitMark youngRank pools =
278 do youngVars <- MVector.read pools youngRank
279 rankTable <- poolToRankTable youngMark youngRank youngVars
281 -- get the ranks right for each entry.
282 -- start at low ranks so that we only have to pass
283 -- over the information once.
284 Vector.imapM_
285 (\rank table -> mapM_ (adjustRank youngMark visitMark rank) table)
286 rankTable
288 -- For variables that have rank lowerer than youngRank, register them in
289 -- the appropriate old pool if they are not redundant.
290 Vector.forM_ (Vector.unsafeInit rankTable) $ \vars ->
291 forM_ vars $ \var ->
292 do isRedundant <- UF.redundant var
293 if isRedundant
294 then return ()
295 else
296 do (Descriptor _ rank _ _) <- UF.get var
297 MVector.modify pools (var:) rank
299 -- For variables with rank youngRank
300 -- If rank < youngRank: register in oldPool
301 -- otherwise generalize
302 forM_ (Vector.unsafeLast rankTable) $ \var ->
303 do isRedundant <- UF.redundant var
304 if isRedundant
305 then return ()
306 else
307 do (Descriptor content rank mark copy) <- UF.get var
308 if rank < youngRank
309 then MVector.modify pools (var:) rank
310 else UF.set var $ Descriptor content noRank mark copy
313poolToRankTable :: Mark -> Int -> [Variable] -> IO (Vector.Vector [Variable])
314poolToRankTable youngMark youngRank youngInhabitants =
315 do mutableTable <- MVector.replicate (youngRank + 1) []
317 -- Sort the youngPool variables into buckets by rank.
318 forM_ youngInhabitants $ \var ->
319 do (Descriptor content rank _ copy) <- UF.get var
320 UF.set var (Descriptor content rank youngMark copy)
321 MVector.modify mutableTable (var:) rank
323 Vector.unsafeFreeze mutableTable
327-- ADJUST RANK
329--
330-- Adjust variable ranks such that ranks never increase as you move deeper.
331-- This way the outermost rank is representative of the entire structure.
332--
333adjustRank :: Mark -> Mark -> Int -> Variable -> IO Int
334adjustRank youngMark visitMark groupRank var =
335 do (Descriptor content rank mark copy) <- UF.get var
336 if mark == youngMark then
337 do -- Set the variable as marked first because it may be cyclic.
338 UF.set var $ Descriptor content rank visitMark copy
339 maxRank <- adjustRankContent youngMark visitMark groupRank content
340 UF.set var $ Descriptor content maxRank visitMark copy
341 return maxRank
343 else if mark == visitMark then
344 return rank
346 else
347 do let minRank = min groupRank rank
348 -- TODO how can minRank ever be groupRank?
349 UF.set var $ Descriptor content minRank visitMark copy
350 return minRank
353adjustRankContent :: Mark -> Mark -> Int -> Content -> IO Int
354adjustRankContent youngMark visitMark groupRank content =
355 let
356 go = adjustRank youngMark visitMark groupRank
357 in
358 case content of
359 FlexVar _ ->
360 return groupRank
362 FlexSuper _ _ ->
363 return groupRank
365 RigidVar _ ->
366 return groupRank
368 RigidSuper _ _ ->
369 return groupRank
371 Structure flatType ->
372 case flatType of
373 App1 _ _ args ->
374 foldM (\rank arg -> max rank <$> go arg) outermostRank args
376 Fun1 arg result ->
377 max <$> go arg <*> go result
379 EmptyRecord1 ->
380 -- THEORY: an empty record never needs to get generalized
381 return outermostRank
383 Record1 fields extension ->
384 do extRank <- go extension
385 foldM (\rank field -> max rank <$> go field) extRank fields
387 Unit1 ->
388 -- THEORY: a unit never needs to get generalized
389 return outermostRank
391 Tuple1 a b maybeC ->
392 do ma <- go a
393 mb <- go b
394 case maybeC of
395 Nothing ->
396 return (max ma mb)
398 Just c ->
399 max (max ma mb) <$> go c
401 Alias _ _ args _ ->
402 -- THEORY: anything in the realVar would be outermostRank
403 foldM (\rank (_, argVar) -> max rank <$> go argVar) outermostRank args
405 Error ->
406 return groupRank
410-- REGISTER VARIABLES
413introduce :: Int -> Pools -> [Variable] -> IO ()
414introduce rank pools variables =
415 do MVector.modify pools (variables++) rank
416 forM_ variables $ \var ->
417 UF.modify var $ \(Descriptor content _ mark copy) ->
418 Descriptor content rank mark copy
422-- TYPE TO VARIABLE
425typeToVariable :: Int -> Pools -> Type -> IO Variable
426typeToVariable rank pools tipe =
427 typeToVar rank pools Map.empty tipe
430typeToVar :: Int -> Pools -> Map.Map Name.Name Variable -> Type -> IO Variable
431typeToVar rank pools aliasDict tipe =
432 let go = typeToVar rank pools aliasDict in
433 case tipe of
434 VarN v ->
435 return v
437 AppN home name args ->
438 do argVars <- traverse go args
439 register rank pools (Structure (App1 home name argVars))
441 FunN a b ->
442 do aVar <- go a
443 bVar <- go b
444 register rank pools (Structure (Fun1 aVar bVar))
446 AliasN home name args aliasType ->
447 do argVars <- traverse (traverse go) args
448 aliasVar <- typeToVar rank pools (Map.fromList argVars) aliasType
449 register rank pools (Alias home name argVars aliasVar)
451 PlaceHolder name ->
452 return (aliasDict ! name)
454 RecordN fields ext ->
455 do fieldVars <- traverse go fields
456 extVar <- go ext
457 register rank pools (Structure (Record1 fieldVars extVar))
459 EmptyRecordN ->
460 register rank pools emptyRecord1
462 UnitN ->
463 register rank pools unit1
465 TupleN a b c ->
466 do aVar <- go a
467 bVar <- go b
468 cVar <- traverse go c
469 register rank pools (Structure (Tuple1 aVar bVar cVar))
472register :: Int -> Pools -> Content -> IO Variable
473register rank pools content =
474 do var <- UF.fresh (Descriptor content rank noMark Nothing)
475 MVector.modify pools (var:) rank
476 return var
479{-# NOINLINE emptyRecord1 #-}
480emptyRecord1 :: Content
481emptyRecord1 =
482 Structure EmptyRecord1
485{-# NOINLINE unit1 #-}
486unit1 :: Content
487unit1 =
488 Structure Unit1
492-- SOURCE TYPE TO VARIABLE
495srcTypeToVariable :: Int -> Pools -> Map.Map Name.Name () -> Can.Type -> IO Variable
496srcTypeToVariable rank pools freeVars srcType =
497 let
498 nameToContent name
499 | Name.isNumberType name = FlexSuper Number (Just name)
500 | Name.isComparableType name = FlexSuper Comparable (Just name)
501 | Name.isAppendableType name = FlexSuper Appendable (Just name)
502 | Name.isCompappendType name = FlexSuper CompAppend (Just name)
503 | otherwise = FlexVar (Just name)
505 makeVar name _ =
506 UF.fresh (Descriptor (nameToContent name) rank noMark Nothing)
507 in
508 do flexVars <- Map.traverseWithKey makeVar freeVars
509 MVector.modify pools (Map.elems flexVars ++) rank
510 srcTypeToVar rank pools flexVars srcType
513srcTypeToVar :: Int -> Pools -> Map.Map Name.Name Variable -> Can.Type -> IO Variable
514srcTypeToVar rank pools flexVars srcType =
515 let go = srcTypeToVar rank pools flexVars in
516 case srcType of
517 Can.TLambda argument result ->
518 do argVar <- go argument
519 resultVar <- go result
520 register rank pools (Structure (Fun1 argVar resultVar))
522 Can.TVar name ->
523 return (flexVars ! name)
525 Can.TType home name args ->
526 do argVars <- traverse go args
527 register rank pools (Structure (App1 home name argVars))
529 Can.TRecord fields maybeExt ->
530 do fieldVars <- traverse (srcFieldTypeToVar rank pools flexVars) fields
531 extVar <-
532 case maybeExt of
533 Nothing -> register rank pools emptyRecord1
534 Just ext -> return (flexVars ! ext)
535 register rank pools (Structure (Record1 fieldVars extVar))
537 Can.TUnit ->
538 register rank pools unit1
540 Can.TTuple a b c ->
541 do aVar <- go a
542 bVar <- go b
543 cVar <- traverse go c
544 register rank pools (Structure (Tuple1 aVar bVar cVar))
546 Can.TAlias home name args aliasType ->
547 do argVars <- traverse (traverse go) args
548 aliasVar <-
549 case aliasType of
550 Can.Holey tipe ->
551 srcTypeToVar rank pools (Map.fromList argVars) tipe
553 Can.Filled tipe ->
554 go tipe
556 register rank pools (Alias home name argVars aliasVar)
559srcFieldTypeToVar :: Int -> Pools -> Map.Map Name.Name Variable -> Can.FieldType -> IO Variable
560srcFieldTypeToVar rank pools flexVars (Can.FieldType _ srcTipe) =
561 srcTypeToVar rank pools flexVars srcTipe
565-- COPY
568makeCopy :: Int -> Pools -> Variable -> IO Variable
569makeCopy rank pools var =
570 do copy <- makeCopyHelp rank pools var
571 restore var
572 return copy
575makeCopyHelp :: Int -> Pools -> Variable -> IO Variable
576makeCopyHelp maxRank pools variable =
577 do (Descriptor content rank _ maybeCopy) <- UF.get variable
579 case maybeCopy of
580 Just copy ->
581 return copy
583 Nothing ->
584 if rank /= noRank then
585 return variable
587 else
588 do let makeDescriptor c = Descriptor c maxRank noMark Nothing
589 copy <- UF.fresh $ makeDescriptor content
590 MVector.modify pools (copy:) maxRank
592 -- Link the original variable to the new variable. This lets us
593 -- avoid making multiple copies of the variable we are instantiating.
594 --
595 -- Need to do this before recursively copying to avoid looping.
596 UF.set variable $
597 Descriptor content rank noMark (Just copy)
599 -- Now we recursively copy the content of the variable.
600 -- We have already marked the variable as copied, so we
601 -- will not repeat this work or crawl this variable again.
602 case content of
603 Structure term ->
604 do newTerm <- traverseFlatType (makeCopyHelp maxRank pools) term
605 UF.set copy $ makeDescriptor (Structure newTerm)
606 return copy
608 FlexVar _ ->
609 return copy
611 FlexSuper _ _ ->
612 return copy
614 RigidVar name ->
615 do UF.set copy $ makeDescriptor $ FlexVar (Just name)
616 return copy
618 RigidSuper super name ->
619 do UF.set copy $ makeDescriptor $ FlexSuper super (Just name)
620 return copy
622 Alias home name args realType ->
623 do newArgs <- mapM (traverse (makeCopyHelp maxRank pools)) args
624 newRealType <- makeCopyHelp maxRank pools realType
625 UF.set copy $ makeDescriptor (Alias home name newArgs newRealType)
626 return copy
628 Error ->
629 return copy
633-- RESTORE
636restore :: Variable -> IO ()
637restore variable =
638 do (Descriptor content _ _ maybeCopy) <- UF.get variable
639 case maybeCopy of
640 Nothing ->
641 return ()
643 Just _ ->
644 do UF.set variable $ Descriptor content noRank noMark Nothing
645 restoreContent content
648restoreContent :: Content -> IO ()
649restoreContent content =
650 case content of
651 FlexVar _ ->
652 return ()
654 FlexSuper _ _ ->
655 return ()
657 RigidVar _ ->
658 return ()
660 RigidSuper _ _ ->
661 return ()
663 Structure term ->
664 case term of
665 App1 _ _ args ->
666 mapM_ restore args
668 Fun1 arg result ->
669 do restore arg
670 restore result
672 EmptyRecord1 ->
673 return ()
675 Record1 fields ext ->
676 do mapM_ restore fields
677 restore ext
679 Unit1 ->
680 return ()
682 Tuple1 a b maybeC ->
683 do restore a
684 restore b
685 case maybeC of
686 Nothing -> return ()
687 Just c -> restore c
689 Alias _ _ args var ->
690 do mapM_ (traverse restore) args
691 restore var
693 Error ->
694 return ()
698-- TRAVERSE FLAT TYPE
701traverseFlatType :: (Variable -> IO Variable) -> FlatType -> IO FlatType
702traverseFlatType f flatType =
703 case flatType of
704 App1 home name args ->
705 liftM (App1 home name) (traverse f args)
707 Fun1 a b ->
708 liftM2 Fun1 (f a) (f b)
710 EmptyRecord1 ->
711 pure EmptyRecord1
713 Record1 fields ext ->
714 liftM2 Record1 (traverse f fields) (f ext)
716 Unit1 ->
717 pure Unit1
719 Tuple1 a b cs ->
720 liftM3 Tuple1 (f a) (f b) (traverse f cs)