git.iko.soy/elk
on ba5bfd2 help sign in
elk/src/Type/Solve.hs
350 lines 11 kB history raw
1module Type.Solve (solve) where
3import Control.Monad
4import Control.Monad.State (execStateT, liftIO)
5import Control.Monad.Except (ExceptT, throwError)
6import qualified Data.List as List
7import qualified Data.Map as Map
8import qualified Data.Traversable as T
9import qualified Data.UnionFind.IO as UF
11import qualified Reporting.Annotation as A
12import qualified Reporting.Error.Type as Error
13import qualified Type.State as TS
14import Type.Type as Type
15import Type.Unify
19{-| Every variable has rank less than or equal to the maxRank of the pool.
20This sorts variables into the young and old pools accordingly.
21-}
22generalize :: TS.Pool -> TS.Solver ()
23generalize youngPool =
24 do youngMark <- TS.uniqueMark
25 let youngRank = TS.maxRank youngPool
26 let insert dict var =
27 do descriptor <- liftIO $ UF.descriptor var
28 liftIO $ UF.modifyDescriptor var (\desc -> desc { _mark = youngMark })
29 return $ Map.insertWith (++) (_rank descriptor) [var] dict
31 -- Sort the youngPool variables by rank.
32 rankDict <- foldM insert Map.empty (TS.inhabitants youngPool)
34 -- get the ranks right for each entry.
35 -- start at low ranks so that we only have to pass
36 -- over the information once.
37 visitedMark <- TS.uniqueMark
38 forM (Map.toList rankDict) $ \(poolRank, vars) ->
39 mapM (adjustRank youngMark visitedMark poolRank) vars
41 -- For variables that have rank lowerer than youngRank, register them in
42 -- the old pool if they are not redundant.
43 let registerIfNotRedundant var =
44 do isRedundant <- liftIO $ UF.redundant var
45 if isRedundant then return var else TS.register var
47 let rankDict' = Map.delete youngRank rankDict
48 T.traverse (mapM registerIfNotRedundant) rankDict'
50 -- For variables with rank youngRank
51 -- If rank < youngRank: register in oldPool
52 -- otherwise generalize
53 let registerIfLowerRank var = do
54 isRedundant <- liftIO $ UF.redundant var
55 case isRedundant of
56 True -> return ()
57 False -> do
58 desc <- liftIO $ UF.descriptor var
59 case _rank desc < youngRank of
60 True ->
61 TS.register var >> return ()
62 False ->
63 liftIO $ UF.setDescriptor var $ desc
64 { _rank = noRank
65 , _content = rigidify (_content desc)
66 }
68 mapM_ registerIfLowerRank (Map.findWithDefault [] youngRank rankDict)
71rigidify :: Content -> Content
72rigidify content =
73 case content of
74 Var Flex maybeSuper _ ->
75 Var Rigid maybeSuper Nothing
77 _ ->
78 content
81-- adjust the ranks of variables such that ranks never increase as you
82-- move deeper into a variable.
83adjustRank :: Int -> Int -> Int -> Variable -> TS.Solver Int
84adjustRank youngMark visitedMark groupRank var =
85 do descriptor <- liftIO $ UF.descriptor var
86 adjustRankHelp youngMark visitedMark groupRank var descriptor
89adjustRankHelp :: Int -> Int -> Int -> Variable -> Descriptor -> TS.Solver Int
90adjustRankHelp youngMark visitedMark groupRank var descriptor =
91 if _mark descriptor == youngMark then
93 do -- Set the variable as marked first because it may be cyclic.
94 liftIO $ UF.modifyDescriptor var $ \desc ->
95 desc { _mark = visitedMark }
97 maxRank <-
98 adjustRankContent youngMark visitedMark groupRank (_content descriptor)
100 liftIO $ UF.modifyDescriptor var $ \desc ->
101 desc { _rank = maxRank }
103 return maxRank
105 else if _mark descriptor /= visitedMark then
107 do let minRank = min groupRank (_rank descriptor)
108 liftIO $ UF.setDescriptor var (descriptor { _mark = visitedMark, _rank = minRank })
109 return minRank
111 else
113 return (_rank descriptor)
116adjustRankContent :: Int -> Int -> Int -> Content -> TS.Solver Int
117adjustRankContent youngMark visitedMark groupRank content =
118 let
119 go = adjustRank youngMark visitedMark groupRank
120 in
121 case content of
122 Error ->
123 return groupRank
125 Atom _ ->
126 return groupRank
128 Var _ _ _ ->
129 return groupRank
131 Alias _ args realVar ->
132 maximum <$> mapM go (realVar : map snd args)
134 Structure (App1 func arg) ->
135 max <$> go func <*> go arg
137 Structure (Fun1 arg result) ->
138 max <$> go arg <*> go result
140 Structure EmptyRecord1 ->
141 return outermostRank
143 Structure (Record1 fields extension) ->
144 maximum <$> mapM go (extension : Map.elems fields)
146 Structure (Effects1 _) ->
147 return outermostRank
151-- SOLVER
154solve :: TypeConstraint -> ExceptT [A.Located Error.Error] IO TS.SolverState
155solve constraint =
156 do state <-
157 liftIO (execStateT (actuallySolve constraint) TS.initialState)
158 case TS.sError state of
159 [] ->
160 return state
161 errors ->
162 throwError errors
165actuallySolve :: TypeConstraint -> TS.Solver ()
166actuallySolve constraint =
167 case constraint of
168 CTrue ->
169 return ()
171 CSaveEnv ->
172 TS.saveLocalEnv
174 CEqual hint region term1 term2 ->
175 do t1 <- TS.flatten term1
176 t2 <- TS.flatten term2
177 unify hint region t1 t2
179 CAnd cs ->
180 mapM_ actuallySolve cs
182 CLet [Scheme [] fqs constraint' _] CTrue ->
183 do oldEnv <- TS.getEnv
184 mapM TS.introduce fqs
185 actuallySolve constraint'
186 TS.modifyEnv (\_ -> oldEnv)
188 CLet schemes constraint' ->
189 do oldEnv <- TS.getEnv
190 headers <- Map.unions <$> mapM solveScheme schemes
191 TS.modifyEnv $ \env -> Map.union headers env
192 actuallySolve constraint'
193 mapM occurs $ Map.toList headers
194 TS.modifyEnv (\_ -> oldEnv)
196 CInstance region name term ->
197 do env <- TS.getEnv
198 freshCopy <-
199 case Map.lookup name env of
200 Just (A.A _ tipe) ->
201 TS.makeInstance tipe
203 Nothing ->
204 if List.isPrefixOf "Native." name then
205 liftIO (mkVar Nothing)
207 else
208 error ("Could not find `" ++ name ++ "` when solving type constraints.")
210 t <- TS.flatten term
211 unify (Error.Instance name) region freshCopy t
214solveScheme :: TypeScheme -> TS.Solver (Map.Map String (A.Located Variable))
215solveScheme scheme =
216 let
217 flatten (A.A region term) =
218 A.A region <$> TS.flatten term
219 in
220 case scheme of
221 Scheme [] [] constraint header ->
222 do actuallySolve constraint
223 T.traverse flatten header
225 Scheme rigidQuantifiers flexibleQuantifiers constraint header ->
226 do let quantifiers = rigidQuantifiers ++ flexibleQuantifiers
227 oldPool <- TS.getPool
229 -- fill in a new pool when working on this scheme's constraints
230 freshPool <- TS.nextRankPool
231 TS.switchToPool freshPool
232 mapM TS.introduce quantifiers
233 header' <- T.traverse flatten header
234 actuallySolve constraint
236 allDistinct rigidQuantifiers
237 youngPool <- TS.getPool
238 TS.switchToPool oldPool
239 generalize youngPool
240 mapM isGeneric rigidQuantifiers
241 return header'
244-- ADDITIONAL CHECKS
246-- Checks that all of the given variables belong to distinct equivalence classes.
247-- Also checks that their structure is Nothing, so they represent a variable, not
248-- a more complex term.
249allDistinct :: [Variable] -> TS.Solver ()
250allDistinct vars =
251 do seenMark <- TS.uniqueMark
252 forM_ vars $ \var ->
253 do desc <- liftIO $ UF.descriptor var
254 case _content desc of
255 Structure _ ->
256 crash "Can only generalize type variables, not structures."
258 Atom _ ->
259 crash "Can only generalize type variables, not structures."
261 Alias _ _ _ ->
262 crash "Can only generalize type variables, not aliases."
264 Error ->
265 crash "Can only generalize type variables, not error types."
267 Var _ _ _ ->
268 if _mark desc == seenMark then
269 crash "Duplicate variable during generalization."
271 else
272 liftIO (UF.setDescriptor var (desc { _mark = seenMark }))
275-- Check that a variable has rank == noRank, meaning that it can be generalized.
276isGeneric :: Variable -> TS.Solver ()
277isGeneric var =
278 do desc <- liftIO $ UF.descriptor var
279 if _rank desc == noRank
280 then return ()
281 else crash "Unable to generalize a type variable. It is not unranked."
284crash :: String -> a
285crash msg =
286 error $
287 "It looks like something went wrong with the type inference algorithm.\n\n"
288 ++ msg ++ "\n\n"
289 ++ "Please create a minimal example that triggers this problem and report it to\n"
290 ++ "<https://github.com/elm-lang/elm-compiler/issues>"
294-- OCCURS CHECK
297occurs :: (String, A.Located Variable) -> TS.Solver ()
298occurs (name, A.A region variable) =
299 do isInfinite <- liftIO $ occursHelp [] variable
300 case isInfinite of
301 False ->
302 return ()
304 True ->
305 do overallType <- liftIO (Type.toSrcType variable)
306 TS.addError region (Error.InfiniteType name overallType)
309occursHelp :: [Variable] -> Variable -> IO Bool
310occursHelp seen var =
311 if elem var seen then
312 do infiniteDescriptor <- UF.descriptor var
313 UF.setDescriptor var (infiniteDescriptor { _content = Error })
314 return True
316 else
317 do desc <- UF.descriptor var
318 case _content desc of
319 Atom _ ->
320 return False
322 Var _ _ _ ->
323 return False
325 Error ->
326 return False
328 Alias _ args _ ->
329 -- TODO is it okay to only check args?
330 or <$> mapM (occursHelp (var:seen) . snd) args
332 Structure term ->
333 let
334 go = occursHelp (var:seen)
335 in
336 case term of
337 App1 a b ->
338 (||) <$> go a <*> go b
340 Fun1 a b ->
341 (||) <$> go a <*> go b
343 EmptyRecord1 ->
344 return False
346 Record1 fields ext ->
347 or <$> mapM go (ext : Map.elems fields)
349 Effects1 _ ->
350 return False