git.iko.soy/elk
on 7dfbc30 help sign in
elk/src/Type/Solve.hs
704 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 16 []
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 problem 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)
96 problem
98 CLookup region name expectation ->
99 do actual <- makeCopy rank pools (env ! name)
100 expected <- expectedToVariable rank pools expectation
101 answer <- Unify.unify actual expected
102 case answer of
103 Unify.Ok vars ->
104 do introduce rank pools vars
105 return state
107 Unify.Err vars problem actualType expectedType ->
108 do introduce rank pools vars
109 return $ addError state $
110 Error.Mismatch
111 (Error.BadLocal region name actualType)
112 (Con.typeReplace expectation expectedType)
113 problem
115 CInstance region funcName (Can.Forall freeVars srcType) expectation ->
116 do actual <- srcTypeToVariable rank pools freeVars srcType
117 expected <- expectedToVariable rank pools expectation
118 answer <- Unify.unify actual expected
119 case answer of
120 Unify.Ok vars ->
121 do introduce rank pools vars
122 return state
124 Unify.Err vars problem actualType expectedType ->
125 do introduce rank pools vars
126 return $ addError state $
127 Error.Mismatch
128 (Error.BadForeign region funcName actualType)
129 (Con.typeReplace expectation expectedType)
130 problem
132 CPattern region category tipe expectation ->
133 do actual <- typeToVariable rank pools tipe
134 expected <- patternExpectationToVariable rank pools expectation
135 answer <- Unify.unify actual expected
136 case answer of
137 Unify.Ok vars ->
138 do introduce rank pools vars
139 return state
141 Unify.Err vars problem actualType expectedType ->
142 do introduce rank pools vars
143 return $ addError state $
144 Error.BadPattern region category actualType
145 (Con.ptypeReplace expectation expectedType)
146 problem
148 CAnd constraints ->
149 foldM (solve env rank pools) state constraints
151 CBranch a b eqCon makeNotEqCon ->
152 do aVar <- typeToVariable rank pools a
153 bVar <- typeToVariable rank pools b
154 answer <- Unify.unify aVar bVar
155 case answer of
156 Unify.Ok vars ->
157 do introduce rank pools vars
158 solve env rank pools state eqCon
160 Unify.Err vars _ _ _ ->
161 do introduce rank pools vars
162 solve env rank pools state =<< makeNotEqCon
164 CLet [] flexs _ headerCon CTrue ->
165 do introduce rank pools flexs
166 solve env rank pools state headerCon
168 CLet [] [] header headerCon subCon ->
169 do state1 <- solve env rank pools state headerCon
170 locals <- traverse (A.traverse (typeToVariable rank pools)) header
171 let newEnv = Map.union env (Map.map A.toValue locals)
172 state2 <- solve newEnv rank pools state1 subCon
173 foldM occurs state2 $ Map.toList locals
175 CLet rigids flexs header headerCon subCon ->
176 do
177 -- work in the next pool to localize header
178 let nextRank = rank + 1
179 let poolsLength = MVector.length pools
180 nextPools <-
181 if nextRank < poolsLength
182 then return pools
183 else MVector.grow pools poolsLength
185 -- introduce variables
186 let vars = rigids ++ flexs
187 forM_ vars $ \var ->
188 UF.modify var $ \(Descriptor content _ mark copy) ->
189 Descriptor content nextRank mark copy
190 MVector.write nextPools nextRank vars
192 -- run solver in next pool
193 locals <- traverse (A.traverse (typeToVariable rank nextPools)) header
194 (State savedEnv mark errors) <-
195 solve env nextRank nextPools state headerCon
197 let youngMark = mark
198 let visitMark = nextMark youngMark
199 let finalMark = nextMark visitMark
201 -- pop pool
202 generalize youngMark visitMark nextRank nextPools
203 MVector.write nextPools nextRank []
205 -- check that things went well
206 mapM_ isGeneric rigids
208 let newEnv = Map.union env (Map.map A.toValue locals)
209 let tempState = State savedEnv finalMark errors
210 newState <- solve newEnv nextRank nextPools tempState subCon
212 foldM occurs newState (Map.toList locals)
215-- Check that a variable has rank == noRank, meaning that it can be generalized.
216isGeneric :: Variable -> IO ()
217isGeneric var =
218 do (Descriptor _ rank _ _) <- UF.get var
219 if rank == noRank
220 then return ()
221 else crash "Unable to generalize a type variable. It is not unranked."
224crash :: String -> a
225crash msg =
226 error $
227 "It looks like something went wrong with the type inference algorithm.\n\n"
228 ++ msg ++ "\n\n"
229 ++ "Please create a minimal example that triggers this problem and report it to\n"
230 ++ "<https://github.com/elm-lang/elm-compiler/issues>"
234-- EXPECTATIONS TO VARIABLE
237expectedToVariable :: Int -> Pools -> Expected Type -> IO Variable
238expectedToVariable rank pools expectation =
239 typeToVariable rank pools $
240 case expectation of
241 NoExpectation tipe ->
242 tipe
244 FromContext _ _ tipe ->
245 tipe
247 FromAnnotation _ _ _ tipe ->
248 tipe
251patternExpectationToVariable :: Int -> Pools -> PExpected Type -> IO Variable
252patternExpectationToVariable rank pools expectation =
253 typeToVariable rank pools $
254 case expectation of
255 PNoExpectation tipe ->
256 tipe
258 PFromContext _ _ tipe ->
259 tipe
263-- ERROR HELPERS
266addError :: State -> Error.Error -> State
267addError (State savedEnv rank errors) err =
268 State savedEnv rank (err:errors)
272-- OCCURS CHECK
275occurs :: State -> (N.Name, A.Located Variable) -> IO State
276occurs state (_name, A.At _region variable) =
277 do hasOccurred <- Occurs.occurs variable
278 if hasOccurred
279 then
280 do overallType <- Type.toSrcType variable
281 (Descriptor _ rank mark copy) <- UF.get variable
282 UF.set variable (Descriptor (Error "∞") rank mark copy)
283 return $ state { _errors = Error.InfiniteType overallType : _errors state }
284 else
285 return state
289-- GENERALIZE
292{-| Every variable has rank less than or equal to the maxRank of the pool.
293This sorts variables into the young and old pools accordingly.
294-}
295generalize :: Mark -> Mark -> Int -> Pools -> IO ()
296generalize youngMark visitMark youngRank pools =
297 do youngVars <- MVector.read pools youngRank
298 rankTable <- poolToRankTable youngMark youngRank youngVars
300 -- get the ranks right for each entry.
301 -- start at low ranks so that we only have to pass
302 -- over the information once.
303 Vector.imapM_ (mapM_ . adjustRank youngMark visitMark) rankTable
305 -- For variables that have rank lowerer than youngRank, register them in
306 -- the appropriate old pool if they are not redundant.
307 Vector.forM_ (Vector.unsafeInit rankTable) $ \vars ->
308 forM_ vars $ \var ->
309 do isRedundant <- UF.redundant var
310 if isRedundant
311 then return ()
312 else
313 do (Descriptor _ rank _ _) <- UF.get var
314 MVector.modify pools (var:) rank
316 -- For variables with rank youngRank
317 -- If rank < youngRank: register in oldPool
318 -- otherwise generalize
319 forM_ (Vector.unsafeLast rankTable) $ \var ->
320 do isRedundant <- UF.redundant var
321 if isRedundant
322 then return ()
323 else
324 do (Descriptor content rank mark copy) <- UF.get var
325 if rank < youngRank
326 then MVector.modify pools (var:) rank
327 else UF.set var $ Descriptor content noRank mark copy
330poolToRankTable :: Mark -> Int -> [Variable] -> IO (Vector.Vector [Variable])
331poolToRankTable youngMark youngRank youngInhabitants =
332 do mutableTable <- MVector.replicate (youngRank + 1) []
334 -- Sort the youngPool variables into buckets by rank.
335 forM_ youngInhabitants $ \var ->
336 do (Descriptor content rank _ copy) <- UF.get var
337 UF.set var (Descriptor content rank youngMark copy)
338 MVector.modify mutableTable (var:) rank
340 Vector.unsafeFreeze mutableTable
344-- ADJUST RANK
346--
347-- Adjust variable ranks such that ranks never increase as you move deeper.
348-- This way the outermost rank is representative of the entire structure.
349--
350adjustRank :: Mark -> Mark -> Int -> Variable -> IO Int
351adjustRank youngMark visitMark groupRank var =
352 {-# SCC elm_compiler_type_adjust #-}
353 do (Descriptor content rank mark copy) <- UF.get var
354 if mark == youngMark then
355 do -- Set the variable as marked first because it may be cyclic.
356 UF.set var $ Descriptor content rank visitMark copy
357 maxRank <- adjustRankContent youngMark visitMark groupRank content
358 UF.set var $ Descriptor content maxRank visitMark copy
359 return maxRank
361 else if mark == visitMark then
362 return rank
364 else
365 do let minRank = min groupRank rank
366 -- TODO how can minRank ever be groupRank?
367 UF.set var $ Descriptor content minRank visitMark copy
368 return minRank
371adjustRankContent :: Mark -> Mark -> Int -> Content -> IO Int
372adjustRankContent youngMark visitMark groupRank content =
373 let
374 go = adjustRank youngMark visitMark groupRank
375 in
376 case content of
377 FlexVar _ ->
378 return groupRank
380 FlexSuper _ _ ->
381 return groupRank
383 RigidVar _ ->
384 return groupRank
386 RigidSuper _ _ ->
387 return groupRank
389 Structure flatType ->
390 case flatType of
391 App1 _ _ args ->
392 foldM (\rank arg -> max rank <$> go arg) outermostRank args
394 Fun1 arg result ->
395 max <$> go arg <*> go result
397 EmptyRecord1 ->
398 -- THEORY: an empty record never needs to get generalized
399 return outermostRank
401 Record1 fields extension ->
402 do extRank <- go extension
403 foldM (\rank field -> max rank <$> go field) extRank fields
405 Unit1 ->
406 -- THEORY: a unit never needs to get generalized
407 return outermostRank
409 Tuple1 a b maybeC ->
410 do ma <- go a
411 mb <- go b
412 case maybeC of
413 Nothing ->
414 return (max ma mb)
416 Just c ->
417 max (max ma mb) <$> go c
419 Alias _ _ args _ ->
420 -- THEORY: anything in the realVar would be outermostRank
421 foldM (\rank (_, argVar) -> max rank <$> go argVar) outermostRank args
423 Error _ ->
424 return groupRank
428-- REGISTER VARIABLES
431introduce :: Int -> Pools -> [Variable] -> IO ()
432introduce rank pools variables =
433 do MVector.modify pools (variables++) rank
434 forM_ variables $ \var ->
435 UF.modify var $ \(Descriptor content _ mark copy) ->
436 Descriptor content rank mark copy
440-- TYPE TO VARIABLE
443typeToVariable :: Int -> Pools -> Type -> IO Variable
444typeToVariable rank pools tipe =
445 typeToVar rank pools Map.empty tipe
448typeToVar :: Int -> Pools -> Map.Map N.Name Variable -> Type -> IO Variable
449typeToVar rank pools aliasDict tipe =
450 let go = typeToVar rank pools aliasDict in
451 case tipe of
452 VarN v ->
453 return v
455 AppN home name args ->
456 do argVars <- traverse go args
457 register rank pools (Structure (App1 home name argVars))
459 FunN a b ->
460 do aVar <- go a
461 bVar <- go b
462 register rank pools (Structure (Fun1 aVar bVar))
464 AliasN home name args aliasType ->
465 do argVars <- traverse (traverse go) args
466 aliasVar <- typeToVar rank pools (Map.fromList argVars) aliasType
467 register rank pools (Alias home name argVars aliasVar)
469 PlaceHolder name ->
470 return (aliasDict ! name)
472 RecordN fields ext ->
473 do fieldVars <- traverse go fields
474 extVar <- go ext
475 register rank pools (Structure (Record1 fieldVars extVar))
477 EmptyRecordN ->
478 register rank pools emptyRecord1
480 UnitN ->
481 register rank pools unit1
483 TupleN a b c ->
484 do aVar <- go a
485 bVar <- go b
486 cVar <- traverse go c
487 register rank pools (Structure (Tuple1 aVar bVar cVar))
490register :: Int -> Pools -> Content -> IO Variable
491register rank pools content =
492 do var <- UF.fresh (Descriptor content rank noMark Nothing)
493 MVector.modify pools (var:) rank
494 return var
497{-# NOINLINE emptyRecord1 #-}
498emptyRecord1 :: Content
499emptyRecord1 =
500 Structure EmptyRecord1
503{-# NOINLINE unit1 #-}
504unit1 :: Content
505unit1 =
506 Structure Unit1
510-- SOURCE TYPE TO VARIABLE
513srcTypeToVariable :: Int -> Pools -> Map.Map N.Name () -> Can.Type -> IO Variable
514srcTypeToVariable rank pools freeVars srcType =
515 let
516 makeVar name _ =
517 UF.fresh (Descriptor (FlexVar (Just name)) rank noMark Nothing)
518 in
519 do flexVars <- Map.traverseWithKey makeVar freeVars
520 MVector.modify pools (Map.elems flexVars ++) rank
521 srcTypeToVar rank pools flexVars srcType
524srcTypeToVar :: Int -> Pools -> Map.Map N.Name Variable -> Can.Type -> IO Variable
525srcTypeToVar rank pools flexVars srcType =
526 let go = srcTypeToVar rank pools flexVars in
527 case srcType of
528 Can.TLambda argument result ->
529 do argVar <- go argument
530 resultVar <- go result
531 register rank pools (Structure (Fun1 argVar resultVar))
533 Can.TVar name ->
534 return (flexVars ! name)
536 Can.TType home name args ->
537 do argVars <- traverse go args
538 register rank pools (Structure (App1 home name argVars))
540 Can.TRecord fields maybeExt ->
541 do fieldVars <- traverse go fields
542 extVar <- maybe (register rank pools emptyRecord1) go maybeExt
543 register rank pools (Structure (Record1 fieldVars extVar))
545 Can.TUnit ->
546 register rank pools unit1
548 Can.TTuple a b c ->
549 do aVar <- go a
550 bVar <- go b
551 cVar <- traverse go c
552 register rank pools (Structure (Tuple1 aVar bVar cVar))
554 Can.TAlias home name args aliasType ->
555 do argVars <- traverse (traverse go) args
556 aliasVar <-
557 case aliasType of
558 Can.Holey tipe ->
559 srcTypeToVar rank pools (Map.fromList argVars) tipe
561 Can.Filled tipe ->
562 go tipe
564 register rank pools (Alias home name argVars aliasVar)
568-- COPY
571makeCopy :: Int -> Pools -> Variable -> IO Variable
572makeCopy rank pools var =
573 do copy <- makeCopyHelp rank pools var
574 _ <- restore var
575 return copy
578makeCopyHelp :: Int -> Pools -> Variable -> IO Variable
579makeCopyHelp maxRank pools variable =
580 do (Descriptor content rank _ maybeCopy) <-
581 UF.get variable
583 case maybeCopy of
584 Just copy ->
585 return copy
587 Nothing ->
588 if rank /= noRank then
589 return variable
591 else
592 do let makeDescriptor c = Descriptor c maxRank noMark Nothing
593 copy <- UF.fresh $ makeDescriptor content
594 MVector.modify pools (copy:) maxRank
596 -- Link the original variable to the new variable. This lets us
597 -- avoid making multiple copies of the variable we are instantiating.
598 --
599 -- Need to do this before recursively copying to avoid looping.
600 UF.set variable $
601 Descriptor content rank noMark (Just copy)
603 -- Now we recursively copy the content of the variable.
604 -- We have already marked the variable as copied, so we
605 -- will not repeat this work or crawl this variable again.
606 case content of
607 Structure term ->
608 do newTerm <- traverseFlatType (makeCopyHelp maxRank pools) term
609 UF.set copy $ makeDescriptor (Structure newTerm)
610 return copy
612 FlexVar _ ->
613 return copy
615 FlexSuper _ _ ->
616 return copy
618 RigidVar name ->
619 do UF.set copy $ makeDescriptor $ FlexVar (Just name)
620 return copy
622 RigidSuper super name ->
623 do UF.set copy $ makeDescriptor $ FlexSuper super (Just name)
624 return copy
626 Alias home name args realType ->
627 do newArgs <- mapM (traverse (makeCopyHelp maxRank pools)) args
628 newRealType <- makeCopyHelp maxRank pools realType
629 UF.set copy $ makeDescriptor (Alias home name newArgs newRealType)
630 return copy
632 Error _ ->
633 return copy
637-- RESTORE
640restore :: Variable -> IO Variable
641restore variable =
642 do (Descriptor content _rank _mark maybeCopy) <- UF.get variable
643 case maybeCopy of
644 Nothing ->
645 return variable
647 Just _ ->
648 do restoredContent <- restoreContent content
649 UF.set variable $
650 Descriptor restoredContent noRank noMark Nothing
651 return variable
654restoreContent :: Content -> IO Content
655restoreContent content =
656 case content of
657 FlexVar _ ->
658 return content
660 FlexSuper _ _ ->
661 return content
663 RigidVar _ ->
664 return content
666 RigidSuper _ _ ->
667 return content
669 Structure term ->
670 Structure <$> traverseFlatType restore term
672 Alias home name args var ->
673 Alias home name
674 <$> mapM (traverse restore) args
675 <*> restore var
677 Error _ ->
678 return content
682-- TRAVERSE FLAT TYPE
685traverseFlatType :: (Variable -> IO Variable) -> FlatType -> IO FlatType
686traverseFlatType f flatType =
687 case flatType of
688 App1 home name args ->
689 liftM (App1 home name) (traverse f args)
691 Fun1 a b ->
692 liftM2 Fun1 (f a) (f b)
694 EmptyRecord1 ->
695 pure EmptyRecord1
697 Record1 fields ext ->
698 liftM2 Record1 (traverse f fields) (f ext)
700 Unit1 ->
701 pure Unit1
703 Tuple1 a b cs ->
704 liftM3 Tuple1 (f a) (f b) (traverse f cs)