on 2ecbee3 help sign in
elk/compiler/src/Type/Solve.hs
719 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.Vector as Vector
14import qualified Data.Vector.Mutable as MVector
16import qualified AST.Canonical as Can
17import qualified Reporting.Annotation as A
18import qualified Reporting.Error.Type as Error
19import qualified Reporting.Render.Type as RT
20import qualified Reporting.Render.Type.Localizer as L
21import qualified Type.Occurs as Occurs
22import Type.Type as Type
23import qualified Type.Error as ET
24import qualified Type.Unify as Unify
25import qualified Type.UnionFind as UF
29-- RUN SOLVER
32run :: Constraint -> IO (Either [Error.Error] (Map.Map Name.Name Can.Annotation))
33run constraint =
34 do pools <- MVector.replicate 8 []
36 (State env _ errors) <-
37 solve Map.empty outermostRank pools emptyState constraint
39 case errors of
40 [] ->
41 Right <$> traverse Type.toAnnotation env
43 _ ->
44 return $ Left errors
48{-# NOINLINE emptyState #-}
49emptyState :: State
50emptyState =
51 State Map.empty (nextMark noMark) []
55-- SOLVER
58type Env =
59 Map.Map Name.Name Variable
62type Pools =
63 MVector.IOVector [Variable]
66data State =
67 State
68 { _env :: Env
69 , _mark :: Mark
70 , _errors :: [Error.Error]
71 }
74solve :: Env -> Int -> Pools -> State -> Constraint -> IO State
75solve env rank pools state constraint =
76 case constraint of
77 CTrue ->
78 return state
80 CSaveTheEnvironment ->
81 return (state { _env = env })
83 CEqual region category tipe expectation ->
84 do actual <- typeToVariable rank pools tipe
85 expected <- expectedToVariable rank pools expectation
86 answer <- Unify.unify actual expected
87 case answer of
88 Unify.Ok vars ->
89 do introduce rank pools vars
90 return state
92 Unify.Err vars actualType expectedType ->
93 do introduce rank pools vars
94 return $ addError state $
95 Error.BadExpr region category actualType $
96 Error.typeReplace expectation expectedType
98 CLocal 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 actualType expectedType ->
108 do introduce rank pools vars
109 return $ addError state $
110 Error.BadExpr region (Error.Local name) actualType $
111 Error.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.BadExpr region (Error.Foreign name) actualType $
126 Error.typeReplace expectation expectedType
128 CPattern region category tipe expectation ->
129 do actual <- typeToVariable rank pools tipe
130 expected <- patternExpectationToVariable rank pools expectation
131 answer <- Unify.unify actual expected
132 case answer of
133 Unify.Ok vars ->
134 do introduce rank pools vars
135 return state
137 Unify.Err vars actualType expectedType ->
138 do introduce rank pools vars
139 return $ addError state $
140 Error.BadPattern region category actualType
141 (Error.ptypeReplace expectation expectedType)
143 CAnd constraints ->
144 foldM (solve env rank pools) state constraints
146 CLet [] flexs _ headerCon CTrue ->
147 do introduce rank pools flexs
148 solve env rank pools state headerCon
150 CLet [] [] header headerCon subCon ->
151 do state1 <- solve env rank pools state headerCon
152 locals <- traverse (A.traverse (typeToVariable rank pools)) header
153 let newEnv = Map.union env (Map.map A.toValue locals)
154 state2 <- solve newEnv rank pools state1 subCon
155 foldM occurs state2 $ Map.toList locals
157 CLet rigids flexs header headerCon subCon ->
158 do
159 -- work in the next pool to localize header
160 let nextRank = rank + 1
161 let poolsLength = MVector.length pools
162 nextPools <-
163 if nextRank < poolsLength
164 then return pools
165 else MVector.grow pools poolsLength
167 -- introduce variables
168 let vars = rigids ++ flexs
169 forM_ vars $ \var ->
170 UF.modify var $ \(Descriptor content _ mark copy) ->
171 Descriptor content nextRank mark copy
172 MVector.write nextPools nextRank vars
174 -- run solver in next pool
175 locals <- traverse (A.traverse (typeToVariable nextRank nextPools)) header
176 (State savedEnv mark errors) <-
177 solve env nextRank nextPools state headerCon
179 let youngMark = mark
180 let visitMark = nextMark youngMark
181 let finalMark = nextMark visitMark
183 -- pop pool
184 generalize youngMark visitMark nextRank nextPools
185 MVector.write nextPools nextRank []
187 -- check that things went well
188 mapM_ isGeneric rigids
190 let newEnv = Map.union env (Map.map A.toValue locals)
191 let tempState = State savedEnv finalMark errors
192 newState <- solve newEnv rank nextPools tempState subCon
194 foldM occurs newState (Map.toList locals)
197-- Check that a variable has rank == noRank, meaning that it can be generalized.
198isGeneric :: Variable -> IO ()
199isGeneric var =
200 do (Descriptor _ rank _ _) <- UF.get var
201 if rank == noRank
202 then return ()
203 else
204 do tipe <- Type.toErrorType var
205 error $
206 "You ran into a compiler bug. Here are some details for the developers:\n\n"
207 ++ " " ++ show (ET.toDoc L.empty RT.None tipe) ++ " [rank = " ++ show rank ++ "]\n\n"
208 ++
209 "Please create an <http://sscce.org/> and then report it\n\
210 \at <https://github.com/elm/compiler/issues>\n\n"
214-- EXPECTATIONS TO VARIABLE
217expectedToVariable :: Int -> Pools -> Error.Expected Type -> IO Variable
218expectedToVariable rank pools expectation =
219 typeToVariable rank pools $
220 case expectation of
221 Error.NoExpectation tipe ->
222 tipe
224 Error.FromContext _ _ tipe ->
225 tipe
227 Error.FromAnnotation _ _ _ tipe ->
228 tipe
231patternExpectationToVariable :: Int -> Pools -> Error.PExpected Type -> IO Variable
232patternExpectationToVariable rank pools expectation =
233 typeToVariable rank pools $
234 case expectation of
235 Error.PNoExpectation tipe ->
236 tipe
238 Error.PFromContext _ _ tipe ->
239 tipe
243-- ERROR HELPERS
246addError :: State -> Error.Error -> State
247addError (State savedEnv rank errors) err =
248 State savedEnv rank (err:errors)
252-- OCCURS CHECK
255occurs :: State -> (Name.Name, A.Located Variable) -> IO State
256occurs state (name, A.At region variable) =
257 do hasOccurred <- Occurs.occurs variable
258 if hasOccurred
259 then
260 do errorType <- Type.toErrorType variable
261 (Descriptor _ rank mark copy) <- UF.get variable
262 UF.set variable (Descriptor Error rank mark copy)
263 return $ addError state (Error.InfiniteType region name errorType)
264 else
265 return state
269-- GENERALIZE
272{-| Every variable has rank less than or equal to the maxRank of the pool.
273This sorts variables into the young and old pools accordingly.
274-}
275generalize :: Mark -> Mark -> Int -> Pools -> IO ()
276generalize youngMark visitMark youngRank pools =
277 do youngVars <- MVector.read pools youngRank
278 rankTable <- poolToRankTable youngMark youngRank youngVars
280 -- get the ranks right for each entry.
281 -- start at low ranks so that we only have to pass
282 -- over the information once.
283 Vector.imapM_
284 (\rank table -> mapM_ (adjustRank youngMark visitMark rank) table)
285 rankTable
287 -- For variables that have rank lowerer than youngRank, register them in
288 -- the appropriate old pool if they are not redundant.
289 Vector.forM_ (Vector.unsafeInit rankTable) $ \vars ->
290 forM_ vars $ \var ->
291 do isRedundant <- UF.redundant var
292 if isRedundant
293 then return ()
294 else
295 do (Descriptor _ rank _ _) <- UF.get var
296 MVector.modify pools (var:) rank
298 -- For variables with rank youngRank
299 -- If rank < youngRank: register in oldPool
300 -- otherwise generalize
301 forM_ (Vector.unsafeLast rankTable) $ \var ->
302 do isRedundant <- UF.redundant var
303 if isRedundant
304 then return ()
305 else
306 do (Descriptor content rank mark copy) <- UF.get var
307 if rank < youngRank
308 then MVector.modify pools (var:) rank
309 else UF.set var $ Descriptor content noRank mark copy
312poolToRankTable :: Mark -> Int -> [Variable] -> IO (Vector.Vector [Variable])
313poolToRankTable youngMark youngRank youngInhabitants =
314 do mutableTable <- MVector.replicate (youngRank + 1) []
316 -- Sort the youngPool variables into buckets by rank.
317 forM_ youngInhabitants $ \var ->
318 do (Descriptor content rank _ copy) <- UF.get var
319 UF.set var (Descriptor content rank youngMark copy)
320 MVector.modify mutableTable (var:) rank
322 Vector.unsafeFreeze mutableTable
326-- ADJUST RANK
328--
329-- Adjust variable ranks such that ranks never increase as you move deeper.
330-- This way the outermost rank is representative of the entire structure.
331--
332adjustRank :: Mark -> Mark -> Int -> Variable -> IO Int
333adjustRank youngMark visitMark groupRank var =
334 do (Descriptor content rank mark copy) <- UF.get var
335 if mark == youngMark then
336 do -- Set the variable as marked first because it may be cyclic.
337 UF.set var $ Descriptor content rank visitMark copy
338 maxRank <- adjustRankContent youngMark visitMark groupRank content
339 UF.set var $ Descriptor content maxRank visitMark copy
340 return maxRank
342 else if mark == visitMark then
343 return rank
345 else
346 do let minRank = min groupRank rank
347 -- TODO how can minRank ever be groupRank?
348 UF.set var $ Descriptor content minRank visitMark copy
349 return minRank
352adjustRankContent :: Mark -> Mark -> Int -> Content -> IO Int
353adjustRankContent youngMark visitMark groupRank content =
354 let
355 go = adjustRank youngMark visitMark groupRank
356 in
357 case content of
358 FlexVar _ ->
359 return groupRank
361 FlexSuper _ _ ->
362 return groupRank
364 RigidVar _ ->
365 return groupRank
367 RigidSuper _ _ ->
368 return groupRank
370 Structure flatType ->
371 case flatType of
372 App1 _ _ args ->
373 foldM (\rank arg -> max rank <$> go arg) outermostRank args
375 Fun1 arg result ->
376 max <$> go arg <*> go result
378 EmptyRecord1 ->
379 -- THEORY: an empty record never needs to get generalized
380 return outermostRank
382 Record1 fields extension ->
383 do extRank <- go extension
384 foldM (\rank field -> max rank <$> go field) extRank fields
386 Unit1 ->
387 -- THEORY: a unit never needs to get generalized
388 return outermostRank
390 Tuple1 a b maybeC ->
391 do ma <- go a
392 mb <- go b
393 case maybeC of
394 Nothing ->
395 return (max ma mb)
397 Just c ->
398 max (max ma mb) <$> go c
400 Alias _ _ args _ ->
401 -- THEORY: anything in the realVar would be outermostRank
402 foldM (\rank (_, argVar) -> max rank <$> go argVar) outermostRank args
404 Error ->
405 return groupRank
409-- REGISTER VARIABLES
412introduce :: Int -> Pools -> [Variable] -> IO ()
413introduce rank pools variables =
414 do MVector.modify pools (variables++) rank
415 forM_ variables $ \var ->
416 UF.modify var $ \(Descriptor content _ mark copy) ->
417 Descriptor content rank mark copy
421-- TYPE TO VARIABLE
424typeToVariable :: Int -> Pools -> Type -> IO Variable
425typeToVariable rank pools tipe =
426 typeToVar rank pools Map.empty tipe
429typeToVar :: Int -> Pools -> Map.Map Name.Name Variable -> Type -> IO Variable
430typeToVar rank pools aliasDict tipe =
431 let go = typeToVar rank pools aliasDict in
432 case tipe of
433 VarN v ->
434 return v
436 AppN home name args ->
437 do argVars <- traverse go args
438 register rank pools (Structure (App1 home name argVars))
440 FunN a b ->
441 do aVar <- go a
442 bVar <- go b
443 register rank pools (Structure (Fun1 aVar bVar))
445 AliasN home name args aliasType ->
446 do argVars <- traverse (traverse go) args
447 aliasVar <- typeToVar rank pools (Map.fromList argVars) aliasType
448 register rank pools (Alias home name argVars aliasVar)
450 PlaceHolder name ->
451 return (aliasDict ! name)
453 RecordN fields ext ->
454 do fieldVars <- traverse go fields
455 extVar <- go ext
456 register rank pools (Structure (Record1 fieldVars extVar))
458 EmptyRecordN ->
459 register rank pools emptyRecord1
461 UnitN ->
462 register rank pools unit1
464 TupleN a b c ->
465 do aVar <- go a
466 bVar <- go b
467 cVar <- traverse go c
468 register rank pools (Structure (Tuple1 aVar bVar cVar))
471register :: Int -> Pools -> Content -> IO Variable
472register rank pools content =
473 do var <- UF.fresh (Descriptor content rank noMark Nothing)
474 MVector.modify pools (var:) rank
475 return var
478{-# NOINLINE emptyRecord1 #-}
479emptyRecord1 :: Content
480emptyRecord1 =
481 Structure EmptyRecord1
484{-# NOINLINE unit1 #-}
485unit1 :: Content
486unit1 =
487 Structure Unit1
491-- SOURCE TYPE TO VARIABLE
494srcTypeToVariable :: Int -> Pools -> Map.Map Name.Name () -> Can.Type -> IO Variable
495srcTypeToVariable rank pools freeVars srcType =
496 let
497 nameToContent name
498 | Name.isNumberType name = FlexSuper Number (Just name)
499 | Name.isComparableType name = FlexSuper Comparable (Just name)
500 | Name.isAppendableType name = FlexSuper Appendable (Just name)
501 | Name.isCompappendType name = FlexSuper CompAppend (Just name)
502 | otherwise = FlexVar (Just name)
504 makeVar name _ =
505 UF.fresh (Descriptor (nameToContent name) rank noMark Nothing)
506 in
507 do flexVars <- Map.traverseWithKey makeVar freeVars
508 MVector.modify pools (Map.elems flexVars ++) rank
509 srcTypeToVar rank pools flexVars srcType
512srcTypeToVar :: Int -> Pools -> Map.Map Name.Name Variable -> Can.Type -> IO Variable
513srcTypeToVar rank pools flexVars srcType =
514 let go = srcTypeToVar rank pools flexVars in
515 case srcType of
516 Can.TLambda argument result ->
517 do argVar <- go argument
518 resultVar <- go result
519 register rank pools (Structure (Fun1 argVar resultVar))
521 Can.TVar name ->
522 return (flexVars ! name)
524 Can.TType home name args ->
525 do argVars <- traverse go args
526 register rank pools (Structure (App1 home name argVars))
528 Can.TRecord fields maybeExt ->
529 do fieldVars <- traverse (srcFieldTypeToVar rank pools flexVars) fields
530 extVar <-
531 case maybeExt of
532 Nothing -> register rank pools emptyRecord1
533 Just ext -> return (flexVars ! ext)
534 register rank pools (Structure (Record1 fieldVars extVar))
536 Can.TUnit ->
537 register rank pools unit1
539 Can.TTuple a b c ->
540 do aVar <- go a
541 bVar <- go b
542 cVar <- traverse go c
543 register rank pools (Structure (Tuple1 aVar bVar cVar))
545 Can.TAlias home name args aliasType ->
546 do argVars <- traverse (traverse go) args
547 aliasVar <-
548 case aliasType of
549 Can.Holey tipe ->
550 srcTypeToVar rank pools (Map.fromList argVars) tipe
552 Can.Filled tipe ->
553 go tipe
555 register rank pools (Alias home name argVars aliasVar)
558srcFieldTypeToVar :: Int -> Pools -> Map.Map Name.Name Variable -> Can.FieldType -> IO Variable
559srcFieldTypeToVar rank pools flexVars (Can.FieldType _ srcTipe) =
560 srcTypeToVar rank pools flexVars srcTipe
564-- COPY
567makeCopy :: Int -> Pools -> Variable -> IO Variable
568makeCopy rank pools var =
569 do copy <- makeCopyHelp rank pools var
570 restore var
571 return copy
574makeCopyHelp :: Int -> Pools -> Variable -> IO Variable
575makeCopyHelp maxRank pools variable =
576 do (Descriptor content rank _ maybeCopy) <- UF.get variable
578 case maybeCopy of
579 Just copy ->
580 return copy
582 Nothing ->
583 if rank /= noRank then
584 return variable
586 else
587 do let makeDescriptor c = Descriptor c maxRank noMark Nothing
588 copy <- UF.fresh $ makeDescriptor content
589 MVector.modify pools (copy:) maxRank
591 -- Link the original variable to the new variable. This lets us
592 -- avoid making multiple copies of the variable we are instantiating.
593 --
594 -- Need to do this before recursively copying to avoid looping.
595 UF.set variable $
596 Descriptor content rank noMark (Just copy)
598 -- Now we recursively copy the content of the variable.
599 -- We have already marked the variable as copied, so we
600 -- will not repeat this work or crawl this variable again.
601 case content of
602 Structure term ->
603 do newTerm <- traverseFlatType (makeCopyHelp maxRank pools) term
604 UF.set copy $ makeDescriptor (Structure newTerm)
605 return copy
607 FlexVar _ ->
608 return copy
610 FlexSuper _ _ ->
611 return copy
613 RigidVar name ->
614 do UF.set copy $ makeDescriptor $ FlexVar (Just name)
615 return copy
617 RigidSuper super name ->
618 do UF.set copy $ makeDescriptor $ FlexSuper super (Just name)
619 return copy
621 Alias home name args realType ->
622 do newArgs <- mapM (traverse (makeCopyHelp maxRank pools)) args
623 newRealType <- makeCopyHelp maxRank pools realType
624 UF.set copy $ makeDescriptor (Alias home name newArgs newRealType)
625 return copy
627 Error ->
628 return copy
632-- RESTORE
635restore :: Variable -> IO ()
636restore variable =
637 do (Descriptor content _ _ maybeCopy) <- UF.get variable
638 case maybeCopy of
639 Nothing ->
640 return ()
642 Just _ ->
643 do UF.set variable $ Descriptor content noRank noMark Nothing
644 restoreContent content
647restoreContent :: Content -> IO ()
648restoreContent content =
649 case content of
650 FlexVar _ ->
651 return ()
653 FlexSuper _ _ ->
654 return ()
656 RigidVar _ ->
657 return ()
659 RigidSuper _ _ ->
660 return ()
662 Structure term ->
663 case term of
664 App1 _ _ args ->
665 mapM_ restore args
667 Fun1 arg result ->
668 do restore arg
669 restore result
671 EmptyRecord1 ->
672 return ()
674 Record1 fields ext ->
675 do mapM_ restore fields
676 restore ext
678 Unit1 ->
679 return ()
681 Tuple1 a b maybeC ->
682 do restore a
683 restore b
684 case maybeC of
685 Nothing -> return ()
686 Just c -> restore c
688 Alias _ _ args var ->
689 do mapM_ (traverse restore) args
690 restore var
692 Error ->
693 return ()
697-- TRAVERSE FLAT TYPE
700traverseFlatType :: (Variable -> IO Variable) -> FlatType -> IO FlatType
701traverseFlatType f flatType =
702 case flatType of
703 App1 home name args ->
704 liftM (App1 home name) (traverse f args)
706 Fun1 a b ->
707 liftM2 Fun1 (f a) (f b)
709 EmptyRecord1 ->
710 pure EmptyRecord1
712 Record1 fields ext ->
713 liftM2 Record1 (traverse f fields) (f ext)
715 Unit1 ->
716 pure Unit1
718 Tuple1 a b cs ->
719 liftM3 Tuple1 (f a) (f b) (traverse f cs)