git.iko.soy/elk
on bd2ab82 help sign in
elk/src/Type/Solve.hs
721 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.Type as Type
21import qualified Type.Unify as Unify
22import qualified Type.UnionFind as UF
26-- RUN SOLVER
29run :: Constraint -> IO (Either [Error.Error] (Map.Map N.Name Can.Annotation))
30run constraint =
31 do pools <- MVector.replicate 8 []
33 (State env _ errors) <-
34 solve Map.empty outermostRank pools emptyState constraint
36 case errors of
37 [] ->
38 Right <$> traverse Type.toAnnotation env
40 _ ->
41 return $ Left errors
45{-# NOINLINE emptyState #-}
46emptyState :: State
47emptyState =
48 State Map.empty (nextMark noMark) []
52-- SOLVER
55type Env =
56 Map.Map N.Name Variable
59type Pools =
60 MVector.IOVector [Variable]
63data State =
64 State
65 { _env :: Env
66 , _mark :: Mark
67 , _errors :: [Error.Error]
68 }
71solve :: Env -> Int -> Pools -> State -> Constraint -> IO State
72solve env rank pools state constraint =
73 case constraint of
74 CTrue ->
75 return state
77 CSaveTheEnvironment ->
78 return (state { _env = env })
80 CEqual region category tipe expectation ->
81 do actual <- typeToVariable rank pools tipe
82 expected <- expectedToVariable rank pools expectation
83 answer <- Unify.unify actual expected
84 case answer of
85 Unify.Ok vars ->
86 do introduce rank pools vars
87 return state
89 Unify.Err vars actualType expectedType ->
90 do introduce rank pools vars
91 return $ addError state $
92 Error.BadExpr region category actualType $
93 Error.typeReplace expectation expectedType
95 CLocal region name expectation ->
96 do actual <- makeCopy rank pools (env ! name)
97 expected <- expectedToVariable rank pools expectation
98 answer <- Unify.unify actual expected
99 case answer of
100 Unify.Ok vars ->
101 do introduce rank pools vars
102 return state
104 Unify.Err vars actualType expectedType ->
105 do introduce rank pools vars
106 return $ addError state $
107 Error.BadExpr region (Error.Local name) actualType $
108 Error.typeReplace expectation expectedType
110 CForeign region name (Can.Forall freeVars srcType) expectation ->
111 do actual <- srcTypeToVariable rank pools freeVars srcType
112 expected <- expectedToVariable rank pools expectation
113 answer <- Unify.unify actual expected
114 case answer of
115 Unify.Ok vars ->
116 do introduce rank pools vars
117 return state
119 Unify.Err vars actualType expectedType ->
120 do introduce rank pools vars
121 return $ addError state $
122 Error.BadExpr region (Error.Foreign name) actualType $
123 Error.typeReplace expectation expectedType
125 CPattern region category tipe expectation ->
126 do actual <- typeToVariable rank pools tipe
127 expected <- patternExpectationToVariable rank pools expectation
128 answer <- Unify.unify actual expected
129 case answer of
130 Unify.Ok vars ->
131 do introduce rank pools vars
132 return state
134 Unify.Err vars actualType expectedType ->
135 do introduce rank pools vars
136 return $ addError state $
137 Error.BadPattern region category actualType
138 (Error.ptypeReplace expectation expectedType)
140 CAnd constraints ->
141 foldM (solve env rank pools) state constraints
143 CBranch a b eqCon makeNotEqCon ->
144 do aVar <- typeToVariable rank pools a
145 bVar <- typeToVariable rank pools b
146 answer <- Unify.unify aVar bVar
147 case answer of
148 Unify.Ok vars ->
149 do introduce rank pools vars
150 solve env rank pools state eqCon
152 Unify.Err vars _ _ ->
153 do introduce rank pools vars
154 solve env rank pools state =<< makeNotEqCon
156 CLet [] flexs _ headerCon CTrue ->
157 do introduce rank pools flexs
158 solve env rank pools state headerCon
160 CLet [] [] header headerCon subCon ->
161 do state1 <- solve env rank pools state headerCon
162 locals <- traverse (A.traverse (typeToVariable rank pools)) header
163 let newEnv = Map.union env (Map.map A.toValue locals)
164 state2 <- solve newEnv rank pools state1 subCon
165 foldM occurs state2 $ Map.toList locals
167 CLet rigids flexs header headerCon subCon ->
168 do
169 -- work in the next pool to localize header
170 let nextRank = rank + 1
171 let poolsLength = MVector.length pools
172 nextPools <-
173 if nextRank < poolsLength
174 then return pools
175 else MVector.grow pools poolsLength
177 -- introduce variables
178 let vars = rigids ++ flexs
179 forM_ vars $ \var ->
180 UF.modify var $ \(Descriptor content _ mark copy) ->
181 Descriptor content nextRank mark copy
182 MVector.write nextPools nextRank vars
184 -- run solver in next pool
185 locals <- traverse (A.traverse (typeToVariable nextRank nextPools)) header
186 (State savedEnv mark errors) <-
187 solve env nextRank nextPools state headerCon
189 let youngMark = mark
190 let visitMark = nextMark youngMark
191 let finalMark = nextMark visitMark
193 -- pop pool
194 generalize youngMark visitMark nextRank nextPools
195 MVector.write nextPools nextRank []
197 -- check that things went well
198 mapM_ isGeneric rigids
200 let newEnv = Map.union env (Map.map A.toValue locals)
201 let tempState = State savedEnv finalMark errors
202 newState <- solve newEnv rank nextPools tempState subCon
204 foldM occurs newState (Map.toList locals)
207-- Check that a variable has rank == noRank, meaning that it can be generalized.
208isGeneric :: Variable -> IO ()
209isGeneric var =
210 do (Descriptor _ rank _ _) <- UF.get var
211 if rank == noRank
212 then return ()
213 else
214 error
215 "You ran into a compiler bug!\n\n\
216 \I was unable to generalize a type variable during type inference. It was ranked.\n\n\
217 \Please create an <http://sscce.org/> and report it at <https://github.com/elm-lang/elm-compiler/issues>\n\n"
221-- EXPECTATIONS TO VARIABLE
224expectedToVariable :: Int -> Pools -> Error.Expected Type -> IO Variable
225expectedToVariable rank pools expectation =
226 typeToVariable rank pools $
227 case expectation of
228 Error.NoExpectation tipe ->
229 tipe
231 Error.FromContext _ _ tipe ->
232 tipe
234 Error.FromAnnotation _ _ _ tipe ->
235 tipe
238patternExpectationToVariable :: Int -> Pools -> Error.PExpected Type -> IO Variable
239patternExpectationToVariable rank pools expectation =
240 typeToVariable rank pools $
241 case expectation of
242 Error.PNoExpectation tipe ->
243 tipe
245 Error.PFromContext _ _ tipe ->
246 tipe
250-- ERROR HELPERS
253addError :: State -> Error.Error -> State
254addError (State savedEnv rank errors) err =
255 State savedEnv rank (err:errors)
259-- OCCURS CHECK
262occurs :: State -> (N.Name, A.Located Variable) -> IO State
263occurs state (name, A.At region variable) =
264 do hasOccurred <- Occurs.occurs variable
265 if hasOccurred
266 then
267 do errorType <- Type.toErrorType variable
268 (Descriptor _ rank mark copy) <- UF.get variable
269 UF.set variable (Descriptor Error rank mark copy)
270 return $ state { _errors = Error.InfiniteType region name errorType : _errors state }
271 else
272 return state
276-- GENERALIZE
279{-| Every variable has rank less than or equal to the maxRank of the pool.
280This sorts variables into the young and old pools accordingly.
281-}
282generalize :: Mark -> Mark -> Int -> Pools -> IO ()
283generalize youngMark visitMark youngRank pools =
284 do youngVars <- MVector.read pools youngRank
285 rankTable <- poolToRankTable youngMark youngRank youngVars
287 -- get the ranks right for each entry.
288 -- start at low ranks so that we only have to pass
289 -- over the information once.
290 Vector.imapM_
291 (\rank table -> mapM_ (adjustRank youngMark visitMark rank) table)
292 rankTable
294 -- For variables that have rank lowerer than youngRank, register them in
295 -- the appropriate old pool if they are not redundant.
296 Vector.forM_ (Vector.unsafeInit rankTable) $ \vars ->
297 forM_ vars $ \var ->
298 do isRedundant <- UF.redundant var
299 if isRedundant
300 then return ()
301 else
302 do (Descriptor _ rank _ _) <- UF.get var
303 MVector.modify pools (var:) rank
305 -- For variables with rank youngRank
306 -- If rank < youngRank: register in oldPool
307 -- otherwise generalize
308 forM_ (Vector.unsafeLast rankTable) $ \var ->
309 do isRedundant <- UF.redundant var
310 if isRedundant
311 then return ()
312 else
313 do (Descriptor content rank mark copy) <- UF.get var
314 if rank < youngRank
315 then MVector.modify pools (var:) rank
316 else UF.set var $ Descriptor content noRank mark copy
319poolToRankTable :: Mark -> Int -> [Variable] -> IO (Vector.Vector [Variable])
320poolToRankTable youngMark youngRank youngInhabitants =
321 do mutableTable <- MVector.replicate (youngRank + 1) []
323 -- Sort the youngPool variables into buckets by rank.
324 forM_ youngInhabitants $ \var ->
325 do (Descriptor content rank _ copy) <- UF.get var
326 UF.set var (Descriptor content rank youngMark copy)
327 MVector.modify mutableTable (var:) rank
329 Vector.unsafeFreeze mutableTable
333-- ADJUST RANK
335--
336-- Adjust variable ranks such that ranks never increase as you move deeper.
337-- This way the outermost rank is representative of the entire structure.
338--
339adjustRank :: Mark -> Mark -> Int -> Variable -> IO Int
340adjustRank youngMark visitMark groupRank var =
341 do (Descriptor content rank mark copy) <- UF.get var
342 if mark == youngMark then
343 do -- Set the variable as marked first because it may be cyclic.
344 UF.set var $ Descriptor content rank visitMark copy
345 maxRank <- adjustRankContent youngMark visitMark groupRank content
346 UF.set var $ Descriptor content maxRank visitMark copy
347 return maxRank
349 else if mark == visitMark then
350 return rank
352 else
353 do let minRank = min groupRank rank
354 -- TODO how can minRank ever be groupRank?
355 UF.set var $ Descriptor content minRank visitMark copy
356 return minRank
359adjustRankContent :: Mark -> Mark -> Int -> Content -> IO Int
360adjustRankContent youngMark visitMark groupRank content =
361 let
362 go = adjustRank youngMark visitMark groupRank
363 in
364 case content of
365 FlexVar _ ->
366 return groupRank
368 FlexSuper _ _ ->
369 return groupRank
371 RigidVar _ ->
372 return groupRank
374 RigidSuper _ _ ->
375 return groupRank
377 Structure flatType ->
378 case flatType of
379 App1 _ _ args ->
380 foldM (\rank arg -> max rank <$> go arg) outermostRank args
382 Fun1 arg result ->
383 max <$> go arg <*> go result
385 EmptyRecord1 ->
386 -- THEORY: an empty record never needs to get generalized
387 return outermostRank
389 Record1 fields extension ->
390 do extRank <- go extension
391 foldM (\rank field -> max rank <$> go field) extRank fields
393 Unit1 ->
394 -- THEORY: a unit never needs to get generalized
395 return outermostRank
397 Tuple1 a b maybeC ->
398 do ma <- go a
399 mb <- go b
400 case maybeC of
401 Nothing ->
402 return (max ma mb)
404 Just c ->
405 max (max ma mb) <$> go c
407 Alias _ _ args _ ->
408 -- THEORY: anything in the realVar would be outermostRank
409 foldM (\rank (_, argVar) -> max rank <$> go argVar) outermostRank args
411 Error ->
412 return groupRank
416-- REGISTER VARIABLES
419introduce :: Int -> Pools -> [Variable] -> IO ()
420introduce rank pools variables =
421 do MVector.modify pools (variables++) rank
422 forM_ variables $ \var ->
423 UF.modify var $ \(Descriptor content _ mark copy) ->
424 Descriptor content rank mark copy
428-- TYPE TO VARIABLE
431typeToVariable :: Int -> Pools -> Type -> IO Variable
432typeToVariable rank pools tipe =
433 typeToVar rank pools Map.empty tipe
436typeToVar :: Int -> Pools -> Map.Map N.Name Variable -> Type -> IO Variable
437typeToVar rank pools aliasDict tipe =
438 let go = typeToVar rank pools aliasDict in
439 case tipe of
440 VarN v ->
441 return v
443 AppN home name args ->
444 do argVars <- traverse go args
445 register rank pools (Structure (App1 home name argVars))
447 FunN a b ->
448 do aVar <- go a
449 bVar <- go b
450 register rank pools (Structure (Fun1 aVar bVar))
452 AliasN home name args aliasType ->
453 do argVars <- traverse (traverse go) args
454 aliasVar <- typeToVar rank pools (Map.fromList argVars) aliasType
455 register rank pools (Alias home name argVars aliasVar)
457 PlaceHolder name ->
458 return (aliasDict ! name)
460 RecordN fields ext ->
461 do fieldVars <- traverse go fields
462 extVar <- go ext
463 register rank pools (Structure (Record1 fieldVars extVar))
465 EmptyRecordN ->
466 register rank pools emptyRecord1
468 UnitN ->
469 register rank pools unit1
471 TupleN a b c ->
472 do aVar <- go a
473 bVar <- go b
474 cVar <- traverse go c
475 register rank pools (Structure (Tuple1 aVar bVar cVar))
478register :: Int -> Pools -> Content -> IO Variable
479register rank pools content =
480 do var <- UF.fresh (Descriptor content rank noMark Nothing)
481 MVector.modify pools (var:) rank
482 return var
485{-# NOINLINE emptyRecord1 #-}
486emptyRecord1 :: Content
487emptyRecord1 =
488 Structure EmptyRecord1
491{-# NOINLINE unit1 #-}
492unit1 :: Content
493unit1 =
494 Structure Unit1
498-- SOURCE TYPE TO VARIABLE
501srcTypeToVariable :: Int -> Pools -> Map.Map N.Name () -> Can.Type -> IO Variable
502srcTypeToVariable rank pools freeVars srcType =
503 let
504 nameToContent name
505 | N.startsWith "number" name = FlexSuper Number (Just name)
506 | N.startsWith "comparable" name = FlexSuper Comparable (Just name)
507 | N.startsWith "appendable" name = FlexSuper Appendable (Just name)
508 | N.startsWith "compappend" name = FlexSuper CompAppend (Just name)
509 | otherwise = FlexVar (Just name)
511 makeVar name _ =
512 UF.fresh (Descriptor (nameToContent name) rank noMark Nothing)
513 in
514 do flexVars <- Map.traverseWithKey makeVar freeVars
515 MVector.modify pools (Map.elems flexVars ++) rank
516 srcTypeToVar rank pools flexVars srcType
519srcTypeToVar :: Int -> Pools -> Map.Map N.Name Variable -> Can.Type -> IO Variable
520srcTypeToVar rank pools flexVars srcType =
521 let go = srcTypeToVar rank pools flexVars in
522 case srcType of
523 Can.TLambda argument result ->
524 do argVar <- go argument
525 resultVar <- go result
526 register rank pools (Structure (Fun1 argVar resultVar))
528 Can.TVar name ->
529 return (flexVars ! name)
531 Can.TType home name args ->
532 do argVars <- traverse go args
533 register rank pools (Structure (App1 home name argVars))
535 Can.TRecord fields maybeExt ->
536 do fieldVars <- traverse go fields
537 extVar <-
538 case maybeExt of
539 Nothing -> register rank pools emptyRecord1
540 Just ext -> return (flexVars ! ext)
541 register rank pools (Structure (Record1 fieldVars extVar))
543 Can.TUnit ->
544 register rank pools unit1
546 Can.TTuple a b c ->
547 do aVar <- go a
548 bVar <- go b
549 cVar <- traverse go c
550 register rank pools (Structure (Tuple1 aVar bVar cVar))
552 Can.TAlias home name args aliasType ->
553 do argVars <- traverse (traverse go) args
554 aliasVar <-
555 case aliasType of
556 Can.Holey tipe ->
557 srcTypeToVar rank pools (Map.fromList argVars) tipe
559 Can.Filled tipe ->
560 go tipe
562 register rank pools (Alias home name argVars aliasVar)
566-- COPY
569makeCopy :: Int -> Pools -> Variable -> IO Variable
570makeCopy rank pools var =
571 do copy <- makeCopyHelp rank pools var
572 restore var
573 return copy
576makeCopyHelp :: Int -> Pools -> Variable -> IO Variable
577makeCopyHelp maxRank pools variable =
578 do (Descriptor content rank _ maybeCopy) <- UF.get variable
580 case maybeCopy of
581 Just copy ->
582 return copy
584 Nothing ->
585 if rank /= noRank then
586 return variable
588 else
589 do let makeDescriptor c = Descriptor c maxRank noMark Nothing
590 copy <- UF.fresh $ makeDescriptor content
591 MVector.modify pools (copy:) maxRank
593 -- Link the original variable to the new variable. This lets us
594 -- avoid making multiple copies of the variable we are instantiating.
595 --
596 -- Need to do this before recursively copying to avoid looping.
597 UF.set variable $
598 Descriptor content rank noMark (Just copy)
600 -- Now we recursively copy the content of the variable.
601 -- We have already marked the variable as copied, so we
602 -- will not repeat this work or crawl this variable again.
603 case content of
604 Structure term ->
605 do newTerm <- traverseFlatType (makeCopyHelp maxRank pools) term
606 UF.set copy $ makeDescriptor (Structure newTerm)
607 return copy
609 FlexVar _ ->
610 return copy
612 FlexSuper _ _ ->
613 return copy
615 RigidVar name ->
616 do UF.set copy $ makeDescriptor $ FlexVar (Just name)
617 return copy
619 RigidSuper super name ->
620 do UF.set copy $ makeDescriptor $ FlexSuper super (Just name)
621 return copy
623 Alias home name args realType ->
624 do newArgs <- mapM (traverse (makeCopyHelp maxRank pools)) args
625 newRealType <- makeCopyHelp maxRank pools realType
626 UF.set copy $ makeDescriptor (Alias home name newArgs newRealType)
627 return copy
629 Error ->
630 return copy
634-- RESTORE
637restore :: Variable -> IO ()
638restore variable =
639 do (Descriptor content _ _ maybeCopy) <- UF.get variable
640 case maybeCopy of
641 Nothing ->
642 return ()
644 Just _ ->
645 do UF.set variable $ Descriptor content noRank noMark Nothing
646 restoreContent content
649restoreContent :: Content -> IO ()
650restoreContent content =
651 case content of
652 FlexVar _ ->
653 return ()
655 FlexSuper _ _ ->
656 return ()
658 RigidVar _ ->
659 return ()
661 RigidSuper _ _ ->
662 return ()
664 Structure term ->
665 case term of
666 App1 _ _ args ->
667 mapM_ restore args
669 Fun1 arg result ->
670 do restore arg
671 restore result
673 EmptyRecord1 ->
674 return ()
676 Record1 fields ext ->
677 do mapM_ restore fields
678 restore ext
680 Unit1 ->
681 return ()
683 Tuple1 a b maybeC ->
684 do restore a
685 restore b
686 case maybeC of
687 Nothing -> return ()
688 Just c -> restore c
690 Alias _ _ args var ->
691 do mapM_ (traverse restore) args
692 restore var
694 Error ->
695 return ()
699-- TRAVERSE FLAT TYPE
702traverseFlatType :: (Variable -> IO Variable) -> FlatType -> IO FlatType
703traverseFlatType f flatType =
704 case flatType of
705 App1 home name args ->
706 liftM (App1 home name) (traverse f args)
708 Fun1 a b ->
709 liftM2 Fun1 (f a) (f b)
711 EmptyRecord1 ->
712 pure EmptyRecord1
714 Record1 fields ext ->
715 liftM2 Record1 (traverse f fields) (f ext)
717 Unit1 ->
718 pure Unit1
720 Tuple1 a b cs ->
721 liftM3 Tuple1 (f a) (f b) (traverse f cs)