git.iko.soy/elk
on 99ef42e help sign in
elk/src/Type/Solve.hs
715 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.Vector as Vector
13import qualified Data.Vector.Mutable as MVector
15import qualified AST.Canonical as Can
16import qualified Elm.Name as N
17import qualified Reporting.Annotation as A
18import qualified Reporting.Error.Type as Error
19import qualified Type.Occurs as Occurs
20import Type.Constraint as Con
21import Type.Type as Type
22import qualified Type.Unify as Unify
23import qualified Type.UnionFind as UF
27-- RUN SOLVER
30run :: Constraint -> IO (Either [Error.Error] (Map.Map N.Name Can.Annotation))
31run constraint =
32 do pools <- MVector.replicate 8 []
34 (State env _ errors) <-
35 solve Map.empty outermostRank pools emptyState constraint
37 case errors of
38 [] ->
39 Right <$> traverse Type.toAnnotation env
41 _ ->
42 return $ Left errors
46{-# NOINLINE emptyState #-}
47emptyState :: State
48emptyState =
49 State Map.empty (nextMark noMark) []
53-- SOLVER
56type Env =
57 Map.Map N.Name Variable
60type Pools =
61 MVector.IOVector [Variable]
64data State =
65 State
66 { _env :: Env
67 , _mark :: Mark
68 , _errors :: [Error.Error]
69 }
72solve :: Env -> Int -> Pools -> State -> Constraint -> IO State
73solve env rank pools state constraint =
74 case constraint of
75 CTrue ->
76 return state
78 CSaveTheEnvironment ->
79 return (state { _env = env })
81 CEqual region category tipe expectation ->
82 do actual <- typeToVariable rank pools tipe
83 expected <- expectedToVariable rank pools expectation
84 answer <- Unify.unify actual expected
85 case answer of
86 Unify.Ok vars ->
87 do introduce rank pools vars
88 return state
90 Unify.Err vars actualType expectedType ->
91 do introduce rank pools vars
92 return $ addError state $
93 Error.Mismatch
94 (Error.BadExpr region category actualType)
95 (Con.typeReplace expectation expectedType)
97 CLocal region name expectation ->
98 do actual <- makeCopy rank pools (env ! name)
99 expected <- expectedToVariable rank pools expectation
100 answer <- Unify.unify actual expected
101 case answer of
102 Unify.Ok vars ->
103 do introduce rank pools vars
104 return state
106 Unify.Err vars actualType expectedType ->
107 do introduce rank pools vars
108 return $ addError state $
109 Error.Mismatch
110 (Error.BadLocal region name actualType)
111 (Con.typeReplace expectation expectedType)
113 CForeign region name (Can.Forall freeVars srcType) expectation ->
114 do actual <- srcTypeToVariable rank pools freeVars srcType
115 expected <- expectedToVariable rank pools expectation
116 answer <- Unify.unify actual expected
117 case answer of
118 Unify.Ok vars ->
119 do introduce rank pools vars
120 return state
122 Unify.Err vars actualType expectedType ->
123 do introduce rank pools vars
124 return $ addError state $
125 Error.Mismatch
126 (Error.BadForeign region name actualType)
127 (Con.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 (Con.ptypeReplace expectation expectedType)
144 CAnd constraints ->
145 foldM (solve env rank pools) state constraints
147 CBranch a b eqCon makeNotEqCon ->
148 do aVar <- typeToVariable rank pools a
149 bVar <- typeToVariable rank pools b
150 answer <- Unify.unify aVar bVar
151 case answer of
152 Unify.Ok vars ->
153 do introduce rank pools vars
154 solve env rank pools state eqCon
156 Unify.Err vars _ _ ->
157 do introduce rank pools vars
158 solve env rank pools state =<< makeNotEqCon
160 CLet [] flexs _ headerCon CTrue ->
161 do introduce rank pools flexs
162 solve env rank pools state headerCon
164 CLet [] [] header headerCon subCon ->
165 do state1 <- solve env rank pools state headerCon
166 locals <- traverse (A.traverse (typeToVariable rank pools)) header
167 let newEnv = Map.union env (Map.map A.toValue locals)
168 state2 <- solve newEnv rank pools state1 subCon
169 foldM occurs state2 $ Map.toList locals
171 CLet rigids flexs header headerCon subCon ->
172 do
173 -- work in the next pool to localize header
174 let nextRank = rank + 1
175 let poolsLength = MVector.length pools
176 nextPools <-
177 if nextRank < poolsLength
178 then return pools
179 else MVector.grow pools poolsLength
181 -- introduce variables
182 let vars = rigids ++ flexs
183 forM_ vars $ \var ->
184 UF.modify var $ \(Descriptor content _ mark copy) ->
185 Descriptor content nextRank mark copy
186 MVector.write nextPools nextRank vars
188 -- run solver in next pool
189 locals <- traverse (A.traverse (typeToVariable nextRank nextPools)) header
190 (State savedEnv mark errors) <-
191 solve env nextRank nextPools state headerCon
193 let youngMark = mark
194 let visitMark = nextMark youngMark
195 let finalMark = nextMark visitMark
197 -- pop pool
198 generalize youngMark visitMark nextRank nextPools
199 MVector.write nextPools nextRank []
201 -- check that things went well
202 mapM_ isGeneric rigids
204 let newEnv = Map.union env (Map.map A.toValue locals)
205 let tempState = State savedEnv finalMark errors
206 newState <- solve newEnv rank nextPools tempState subCon
208 foldM occurs newState (Map.toList locals)
211-- Check that a variable has rank == noRank, meaning that it can be generalized.
212isGeneric :: Variable -> IO ()
213isGeneric var =
214 do (Descriptor _ rank _ _) <- UF.get var
215 if rank == noRank
216 then return ()
217 else
218 error
219 "You ran into a compiler bug!\n\n\
220 \I was unable to generalize a type variable during type inference. It was ranked.\n\n\
221 \Please create an <http://sscce.org/> and report it at <https://github.com/elm-lang/elm-compiler/issues>\n\n"
225-- EXPECTATIONS TO VARIABLE
228expectedToVariable :: Int -> Pools -> Expected Type -> IO Variable
229expectedToVariable rank pools expectation =
230 typeToVariable rank pools $
231 case expectation of
232 NoExpectation tipe ->
233 tipe
235 FromContext _ _ tipe ->
236 tipe
238 FromAnnotation _ _ _ tipe ->
239 tipe
242patternExpectationToVariable :: Int -> Pools -> PExpected Type -> IO Variable
243patternExpectationToVariable rank pools expectation =
244 typeToVariable rank pools $
245 case expectation of
246 PNoExpectation tipe ->
247 tipe
249 PFromContext _ _ tipe ->
250 tipe
254-- ERROR HELPERS
257addError :: State -> Error.Error -> State
258addError (State savedEnv rank errors) err =
259 State savedEnv rank (err:errors)
263-- OCCURS CHECK
266occurs :: State -> (N.Name, A.Located Variable) -> IO State
267occurs state (_name, A.At _region variable) =
268 do hasOccurred <- Occurs.occurs variable
269 if hasOccurred
270 then
271 do overallType <- Type.toSrcType variable
272 (Descriptor _ rank mark copy) <- UF.get variable
273 UF.set variable (Descriptor (Error "∞") rank mark copy)
274 return $ state { _errors = Error.InfiniteType overallType : _errors state }
275 else
276 return state
280-- GENERALIZE
283{-| Every variable has rank less than or equal to the maxRank of the pool.
284This sorts variables into the young and old pools accordingly.
285-}
286generalize :: Mark -> Mark -> Int -> Pools -> IO ()
287generalize youngMark visitMark youngRank pools =
288 do youngVars <- MVector.read pools youngRank
289 rankTable <- poolToRankTable youngMark youngRank youngVars
291 -- get the ranks right for each entry.
292 -- start at low ranks so that we only have to pass
293 -- over the information once.
294 Vector.imapM_
295 (\rank table -> mapM_ (adjustRank youngMark visitMark rank) table)
296 rankTable
298 -- For variables that have rank lowerer than youngRank, register them in
299 -- the appropriate old pool if they are not redundant.
300 Vector.forM_ (Vector.unsafeInit rankTable) $ \vars ->
301 forM_ vars $ \var ->
302 do isRedundant <- UF.redundant var
303 if isRedundant
304 then return ()
305 else
306 do (Descriptor _ rank _ _) <- UF.get var
307 MVector.modify pools (var:) rank
309 -- For variables with rank youngRank
310 -- If rank < youngRank: register in oldPool
311 -- otherwise generalize
312 forM_ (Vector.unsafeLast rankTable) $ \var ->
313 do isRedundant <- UF.redundant var
314 if isRedundant
315 then return ()
316 else
317 do (Descriptor content rank mark copy) <- UF.get var
318 if rank < youngRank
319 then MVector.modify pools (var:) rank
320 else UF.set var $ Descriptor content noRank mark copy
323poolToRankTable :: Mark -> Int -> [Variable] -> IO (Vector.Vector [Variable])
324poolToRankTable youngMark youngRank youngInhabitants =
325 do mutableTable <- MVector.replicate (youngRank + 1) []
327 -- Sort the youngPool variables into buckets by rank.
328 forM_ youngInhabitants $ \var ->
329 do (Descriptor content rank _ copy) <- UF.get var
330 UF.set var (Descriptor content rank youngMark copy)
331 MVector.modify mutableTable (var:) rank
333 Vector.unsafeFreeze mutableTable
337-- ADJUST RANK
339--
340-- Adjust variable ranks such that ranks never increase as you move deeper.
341-- This way the outermost rank is representative of the entire structure.
342--
343adjustRank :: Mark -> Mark -> Int -> Variable -> IO Int
344adjustRank youngMark visitMark groupRank var =
345 do (Descriptor content rank mark copy) <- UF.get var
346 if mark == youngMark then
347 do -- Set the variable as marked first because it may be cyclic.
348 UF.set var $ Descriptor content rank visitMark copy
349 maxRank <- adjustRankContent youngMark visitMark groupRank content
350 UF.set var $ Descriptor content maxRank visitMark copy
351 return maxRank
353 else if mark == visitMark then
354 return rank
356 else
357 do let minRank = min groupRank rank
358 -- TODO how can minRank ever be groupRank?
359 UF.set var $ Descriptor content minRank visitMark copy
360 return minRank
363adjustRankContent :: Mark -> Mark -> Int -> Content -> IO Int
364adjustRankContent youngMark visitMark groupRank content =
365 let
366 go = adjustRank youngMark visitMark groupRank
367 in
368 case content of
369 FlexVar _ ->
370 return groupRank
372 FlexSuper _ _ ->
373 return groupRank
375 RigidVar _ ->
376 return groupRank
378 RigidSuper _ _ ->
379 return groupRank
381 Structure flatType ->
382 case flatType of
383 App1 _ _ args ->
384 foldM (\rank arg -> max rank <$> go arg) outermostRank args
386 Fun1 arg result ->
387 max <$> go arg <*> go result
389 EmptyRecord1 ->
390 -- THEORY: an empty record never needs to get generalized
391 return outermostRank
393 Record1 fields extension ->
394 do extRank <- go extension
395 foldM (\rank field -> max rank <$> go field) extRank fields
397 Unit1 ->
398 -- THEORY: a unit never needs to get generalized
399 return outermostRank
401 Tuple1 a b maybeC ->
402 do ma <- go a
403 mb <- go b
404 case maybeC of
405 Nothing ->
406 return (max ma mb)
408 Just c ->
409 max (max ma mb) <$> go c
411 Alias _ _ args _ ->
412 -- THEORY: anything in the realVar would be outermostRank
413 foldM (\rank (_, argVar) -> max rank <$> go argVar) outermostRank args
415 Error _ ->
416 return groupRank
420-- REGISTER VARIABLES
423introduce :: Int -> Pools -> [Variable] -> IO ()
424introduce rank pools variables =
425 do MVector.modify pools (variables++) rank
426 forM_ variables $ \var ->
427 UF.modify var $ \(Descriptor content _ mark copy) ->
428 Descriptor content rank mark copy
432-- TYPE TO VARIABLE
435typeToVariable :: Int -> Pools -> Type -> IO Variable
436typeToVariable rank pools tipe =
437 typeToVar rank pools Map.empty tipe
440typeToVar :: Int -> Pools -> Map.Map N.Name Variable -> Type -> IO Variable
441typeToVar rank pools aliasDict tipe =
442 let go = typeToVar rank pools aliasDict in
443 case tipe of
444 VarN v ->
445 return v
447 AppN home name args ->
448 do argVars <- traverse go args
449 register rank pools (Structure (App1 home name argVars))
451 FunN a b ->
452 do aVar <- go a
453 bVar <- go b
454 register rank pools (Structure (Fun1 aVar bVar))
456 AliasN home name args aliasType ->
457 do argVars <- traverse (traverse go) args
458 aliasVar <- typeToVar rank pools (Map.fromList argVars) aliasType
459 register rank pools (Alias home name argVars aliasVar)
461 PlaceHolder name ->
462 return (aliasDict ! name)
464 RecordN fields ext ->
465 do fieldVars <- traverse go fields
466 extVar <- go ext
467 register rank pools (Structure (Record1 fieldVars extVar))
469 EmptyRecordN ->
470 register rank pools emptyRecord1
472 UnitN ->
473 register rank pools unit1
475 TupleN a b c ->
476 do aVar <- go a
477 bVar <- go b
478 cVar <- traverse go c
479 register rank pools (Structure (Tuple1 aVar bVar cVar))
482register :: Int -> Pools -> Content -> IO Variable
483register rank pools content =
484 do var <- UF.fresh (Descriptor content rank noMark Nothing)
485 MVector.modify pools (var:) rank
486 return var
489{-# NOINLINE emptyRecord1 #-}
490emptyRecord1 :: Content
491emptyRecord1 =
492 Structure EmptyRecord1
495{-# NOINLINE unit1 #-}
496unit1 :: Content
497unit1 =
498 Structure Unit1
502-- SOURCE TYPE TO VARIABLE
505srcTypeToVariable :: Int -> Pools -> Map.Map N.Name () -> Can.Type -> IO Variable
506srcTypeToVariable rank pools freeVars srcType =
507 let
508 makeVar name _ =
509 UF.fresh (Descriptor (FlexVar (Just name)) rank noMark Nothing)
510 in
511 do flexVars <- Map.traverseWithKey makeVar freeVars
512 MVector.modify pools (Map.elems flexVars ++) rank
513 srcTypeToVar rank pools flexVars srcType
516srcTypeToVar :: Int -> Pools -> Map.Map N.Name Variable -> Can.Type -> IO Variable
517srcTypeToVar rank pools flexVars srcType =
518 let go = srcTypeToVar rank pools flexVars in
519 case srcType of
520 Can.TLambda argument result ->
521 do argVar <- go argument
522 resultVar <- go result
523 register rank pools (Structure (Fun1 argVar resultVar))
525 Can.TVar name ->
526 return (flexVars ! name)
528 Can.TType home name args ->
529 do argVars <- traverse go args
530 register rank pools (Structure (App1 home name argVars))
532 Can.TRecord fields maybeExt ->
533 do fieldVars <- traverse go fields
534 extVar <- maybe (register rank pools emptyRecord1) go maybeExt
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)
560-- COPY
563makeCopy :: Int -> Pools -> Variable -> IO Variable
564makeCopy rank pools var =
565 do copy <- makeCopyHelp rank pools var
566 restore var
567 return copy
570makeCopyHelp :: Int -> Pools -> Variable -> IO Variable
571makeCopyHelp maxRank pools variable =
572 do (Descriptor content rank _ maybeCopy) <- UF.get variable
574 case maybeCopy of
575 Just copy ->
576 return copy
578 Nothing ->
579 if rank /= noRank then
580 return variable
582 else
583 do let makeDescriptor c = Descriptor c maxRank noMark Nothing
584 copy <- UF.fresh $ makeDescriptor content
585 MVector.modify pools (copy:) maxRank
587 -- Link the original variable to the new variable. This lets us
588 -- avoid making multiple copies of the variable we are instantiating.
589 --
590 -- Need to do this before recursively copying to avoid looping.
591 UF.set variable $
592 Descriptor content rank noMark (Just copy)
594 -- Now we recursively copy the content of the variable.
595 -- We have already marked the variable as copied, so we
596 -- will not repeat this work or crawl this variable again.
597 case content of
598 Structure term ->
599 do newTerm <- traverseFlatType (makeCopyHelp maxRank pools) term
600 UF.set copy $ makeDescriptor (Structure newTerm)
601 return copy
603 FlexVar _ ->
604 return copy
606 FlexSuper _ _ ->
607 return copy
609 RigidVar name ->
610 do UF.set copy $ makeDescriptor $ FlexVar (Just name)
611 return copy
613 RigidSuper super name ->
614 do UF.set copy $ makeDescriptor $ FlexSuper super (Just name)
615 return copy
617 Alias home name args realType ->
618 do newArgs <- mapM (traverse (makeCopyHelp maxRank pools)) args
619 newRealType <- makeCopyHelp maxRank pools realType
620 UF.set copy $ makeDescriptor (Alias home name newArgs newRealType)
621 return copy
623 Error _ ->
624 return copy
628-- RESTORE
631restore :: Variable -> IO ()
632restore variable =
633 do (Descriptor content _ _ maybeCopy) <- UF.get variable
634 case maybeCopy of
635 Nothing ->
636 return ()
638 Just _ ->
639 do UF.set variable $ Descriptor content noRank noMark Nothing
640 restoreContent content
643restoreContent :: Content -> IO ()
644restoreContent content =
645 case content of
646 FlexVar _ ->
647 return ()
649 FlexSuper _ _ ->
650 return ()
652 RigidVar _ ->
653 return ()
655 RigidSuper _ _ ->
656 return ()
658 Structure term ->
659 case term of
660 App1 _ _ args ->
661 mapM_ restore args
663 Fun1 arg result ->
664 do restore arg
665 restore result
667 EmptyRecord1 ->
668 return ()
670 Record1 fields ext ->
671 do mapM_ restore fields
672 restore ext
674 Unit1 ->
675 return ()
677 Tuple1 a b maybeC ->
678 do restore a
679 restore b
680 case maybeC of
681 Nothing -> return ()
682 Just c -> restore c
684 Alias _ _ args var ->
685 do mapM_ (traverse restore) args
686 restore var
688 Error _ ->
689 return ()
693-- TRAVERSE FLAT TYPE
696traverseFlatType :: (Variable -> IO Variable) -> FlatType -> IO FlatType
697traverseFlatType f flatType =
698 case flatType of
699 App1 home name args ->
700 liftM (App1 home name) (traverse f args)
702 Fun1 a b ->
703 liftM2 Fun1 (f a) (f b)
705 EmptyRecord1 ->
706 pure EmptyRecord1
708 Record1 fields ext ->
709 liftM2 Record1 (traverse f fields) (f ext)
711 Unit1 ->
712 pure Unit1
714 Tuple1 a b cs ->
715 liftM3 Tuple1 (f a) (f b) (traverse f cs)