git.iko.soy/elk
on dc356df help sign in
elk/src/Type/Solve.hs
716 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 {-# SCC elm_compiler_type_adjust #-}
346 do (Descriptor content rank mark copy) <- UF.get var
347 if mark == youngMark then
348 do -- Set the variable as marked first because it may be cyclic.
349 UF.set var $ Descriptor content rank visitMark copy
350 maxRank <- adjustRankContent youngMark visitMark groupRank content
351 UF.set var $ Descriptor content maxRank visitMark copy
352 return maxRank
354 else if mark == visitMark then
355 return rank
357 else
358 do let minRank = min groupRank rank
359 -- TODO how can minRank ever be groupRank?
360 UF.set var $ Descriptor content minRank visitMark copy
361 return minRank
364adjustRankContent :: Mark -> Mark -> Int -> Content -> IO Int
365adjustRankContent youngMark visitMark groupRank content =
366 let
367 go = adjustRank youngMark visitMark groupRank
368 in
369 case content of
370 FlexVar _ ->
371 return groupRank
373 FlexSuper _ _ ->
374 return groupRank
376 RigidVar _ ->
377 return groupRank
379 RigidSuper _ _ ->
380 return groupRank
382 Structure flatType ->
383 case flatType of
384 App1 _ _ args ->
385 foldM (\rank arg -> max rank <$> go arg) outermostRank args
387 Fun1 arg result ->
388 max <$> go arg <*> go result
390 EmptyRecord1 ->
391 -- THEORY: an empty record never needs to get generalized
392 return outermostRank
394 Record1 fields extension ->
395 do extRank <- go extension
396 foldM (\rank field -> max rank <$> go field) extRank fields
398 Unit1 ->
399 -- THEORY: a unit never needs to get generalized
400 return outermostRank
402 Tuple1 a b maybeC ->
403 do ma <- go a
404 mb <- go b
405 case maybeC of
406 Nothing ->
407 return (max ma mb)
409 Just c ->
410 max (max ma mb) <$> go c
412 Alias _ _ args _ ->
413 -- THEORY: anything in the realVar would be outermostRank
414 foldM (\rank (_, argVar) -> max rank <$> go argVar) outermostRank args
416 Error _ ->
417 return groupRank
421-- REGISTER VARIABLES
424introduce :: Int -> Pools -> [Variable] -> IO ()
425introduce rank pools variables =
426 do MVector.modify pools (variables++) rank
427 forM_ variables $ \var ->
428 UF.modify var $ \(Descriptor content _ mark copy) ->
429 Descriptor content rank mark copy
433-- TYPE TO VARIABLE
436typeToVariable :: Int -> Pools -> Type -> IO Variable
437typeToVariable rank pools tipe =
438 typeToVar rank pools Map.empty tipe
441typeToVar :: Int -> Pools -> Map.Map N.Name Variable -> Type -> IO Variable
442typeToVar rank pools aliasDict tipe =
443 let go = typeToVar rank pools aliasDict in
444 case tipe of
445 VarN v ->
446 return v
448 AppN home name args ->
449 do argVars <- traverse go args
450 register rank pools (Structure (App1 home name argVars))
452 FunN a b ->
453 do aVar <- go a
454 bVar <- go b
455 register rank pools (Structure (Fun1 aVar bVar))
457 AliasN home name args aliasType ->
458 do argVars <- traverse (traverse go) args
459 aliasVar <- typeToVar rank pools (Map.fromList argVars) aliasType
460 register rank pools (Alias home name argVars aliasVar)
462 PlaceHolder name ->
463 return (aliasDict ! name)
465 RecordN fields ext ->
466 do fieldVars <- traverse go fields
467 extVar <- go ext
468 register rank pools (Structure (Record1 fieldVars extVar))
470 EmptyRecordN ->
471 register rank pools emptyRecord1
473 UnitN ->
474 register rank pools unit1
476 TupleN a b c ->
477 do aVar <- go a
478 bVar <- go b
479 cVar <- traverse go c
480 register rank pools (Structure (Tuple1 aVar bVar cVar))
483register :: Int -> Pools -> Content -> IO Variable
484register rank pools content =
485 do var <- UF.fresh (Descriptor content rank noMark Nothing)
486 MVector.modify pools (var:) rank
487 return var
490{-# NOINLINE emptyRecord1 #-}
491emptyRecord1 :: Content
492emptyRecord1 =
493 Structure EmptyRecord1
496{-# NOINLINE unit1 #-}
497unit1 :: Content
498unit1 =
499 Structure Unit1
503-- SOURCE TYPE TO VARIABLE
506srcTypeToVariable :: Int -> Pools -> Map.Map N.Name () -> Can.Type -> IO Variable
507srcTypeToVariable rank pools freeVars srcType =
508 let
509 makeVar name _ =
510 UF.fresh (Descriptor (FlexVar (Just name)) rank noMark Nothing)
511 in
512 do flexVars <- Map.traverseWithKey makeVar freeVars
513 MVector.modify pools (Map.elems flexVars ++) rank
514 srcTypeToVar rank pools flexVars srcType
517srcTypeToVar :: Int -> Pools -> Map.Map N.Name Variable -> Can.Type -> IO Variable
518srcTypeToVar rank pools flexVars srcType =
519 let go = srcTypeToVar rank pools flexVars in
520 case srcType of
521 Can.TLambda argument result ->
522 do argVar <- go argument
523 resultVar <- go result
524 register rank pools (Structure (Fun1 argVar resultVar))
526 Can.TVar name ->
527 return (flexVars ! name)
529 Can.TType home name args ->
530 do argVars <- traverse go args
531 register rank pools (Structure (App1 home name argVars))
533 Can.TRecord fields maybeExt ->
534 do fieldVars <- traverse go fields
535 extVar <- maybe (register rank pools emptyRecord1) go maybeExt
536 register rank pools (Structure (Record1 fieldVars extVar))
538 Can.TUnit ->
539 register rank pools unit1
541 Can.TTuple a b c ->
542 do aVar <- go a
543 bVar <- go b
544 cVar <- traverse go c
545 register rank pools (Structure (Tuple1 aVar bVar cVar))
547 Can.TAlias home name args aliasType ->
548 do argVars <- traverse (traverse go) args
549 aliasVar <-
550 case aliasType of
551 Can.Holey tipe ->
552 srcTypeToVar rank pools (Map.fromList argVars) tipe
554 Can.Filled tipe ->
555 go tipe
557 register rank pools (Alias home name argVars aliasVar)
561-- COPY
564makeCopy :: Int -> Pools -> Variable -> IO Variable
565makeCopy rank pools var =
566 do copy <- makeCopyHelp rank pools var
567 restore var
568 return copy
571makeCopyHelp :: Int -> Pools -> Variable -> IO Variable
572makeCopyHelp maxRank pools variable =
573 do (Descriptor content rank _ maybeCopy) <- UF.get variable
575 case maybeCopy of
576 Just copy ->
577 return copy
579 Nothing ->
580 if rank /= noRank then
581 return variable
583 else
584 do let makeDescriptor c = Descriptor c maxRank noMark Nothing
585 copy <- UF.fresh $ makeDescriptor content
586 MVector.modify pools (copy:) maxRank
588 -- Link the original variable to the new variable. This lets us
589 -- avoid making multiple copies of the variable we are instantiating.
590 --
591 -- Need to do this before recursively copying to avoid looping.
592 UF.set variable $
593 Descriptor content rank noMark (Just copy)
595 -- Now we recursively copy the content of the variable.
596 -- We have already marked the variable as copied, so we
597 -- will not repeat this work or crawl this variable again.
598 case content of
599 Structure term ->
600 do newTerm <- traverseFlatType (makeCopyHelp maxRank pools) term
601 UF.set copy $ makeDescriptor (Structure newTerm)
602 return copy
604 FlexVar _ ->
605 return copy
607 FlexSuper _ _ ->
608 return copy
610 RigidVar name ->
611 do UF.set copy $ makeDescriptor $ FlexVar (Just name)
612 return copy
614 RigidSuper super name ->
615 do UF.set copy $ makeDescriptor $ FlexSuper super (Just name)
616 return copy
618 Alias home name args realType ->
619 do newArgs <- mapM (traverse (makeCopyHelp maxRank pools)) args
620 newRealType <- makeCopyHelp maxRank pools realType
621 UF.set copy $ makeDescriptor (Alias home name newArgs newRealType)
622 return copy
624 Error _ ->
625 return copy
629-- RESTORE
632restore :: Variable -> IO ()
633restore variable =
634 do (Descriptor content _ _ maybeCopy) <- UF.get variable
635 case maybeCopy of
636 Nothing ->
637 return ()
639 Just _ ->
640 do UF.set variable $ Descriptor content noRank noMark Nothing
641 restoreContent content
644restoreContent :: Content -> IO ()
645restoreContent content =
646 case content of
647 FlexVar _ ->
648 return ()
650 FlexSuper _ _ ->
651 return ()
653 RigidVar _ ->
654 return ()
656 RigidSuper _ _ ->
657 return ()
659 Structure term ->
660 case term of
661 App1 _ _ args ->
662 mapM_ restore args
664 Fun1 arg result ->
665 do restore arg
666 restore result
668 EmptyRecord1 ->
669 return ()
671 Record1 fields ext ->
672 do mapM_ restore fields
673 restore ext
675 Unit1 ->
676 return ()
678 Tuple1 a b maybeC ->
679 do restore a
680 restore b
681 case maybeC of
682 Nothing -> return ()
683 Just c -> restore c
685 Alias _ _ args var ->
686 do mapM_ (traverse restore) args
687 restore var
689 Error _ ->
690 return ()
694-- TRAVERSE FLAT TYPE
697traverseFlatType :: (Variable -> IO Variable) -> FlatType -> IO FlatType
698traverseFlatType f flatType =
699 case flatType of
700 App1 home name args ->
701 liftM (App1 home name) (traverse f args)
703 Fun1 a b ->
704 liftM2 Fun1 (f a) (f b)
706 EmptyRecord1 ->
707 pure EmptyRecord1
709 Record1 fields ext ->
710 liftM2 Record1 (traverse f fields) (f ext)
712 Unit1 ->
713 pure Unit1
715 Tuple1 a b cs ->
716 liftM3 Tuple1 (f a) (f b) (traverse f cs)