git.iko.soy/elk
on 6dc7ebd help sign in
elk/src/Type/Solve.hs
346 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.Foldable as F
7import qualified Data.List as List
8import qualified Data.Map as Map
9import qualified Data.Traversable as T
10import qualified Data.UnionFind.IO as UF
12import qualified AST.Type as Type
13import qualified Reporting.Annotation as A
14import qualified Reporting.Error.Type as Error
15import qualified Type.State as TS
16import Type.Type as Type
17import Type.Unify
21{-| Every variable has rank less than or equal to the maxRank of the pool.
22This sorts variables into the young and old pools accordingly.
23-}
24generalize :: TS.Pool -> TS.Solver ()
25generalize youngPool =
26 do youngMark <- TS.uniqueMark
27 let youngRank = TS.maxRank youngPool
28 let insert dict var =
29 do descriptor <- liftIO $ UF.descriptor var
30 liftIO $ UF.modifyDescriptor var (\desc -> desc { _mark = youngMark })
31 return $ Map.insertWith (++) (_rank descriptor) [var] dict
33 -- Sort the youngPool variables by rank.
34 rankDict <- foldM insert Map.empty (TS.inhabitants youngPool)
36 -- get the ranks right for each entry.
37 -- start at low ranks so that we only have to pass
38 -- over the information once.
39 visitedMark <- TS.uniqueMark
40 forM (Map.toList rankDict) $ \(poolRank, vars) ->
41 mapM (adjustRank youngMark visitedMark poolRank) vars
43 -- For variables that have rank lowerer than youngRank, register them in
44 -- the old pool if they are not redundant.
45 let registerIfNotRedundant var =
46 do isRedundant <- liftIO $ UF.redundant var
47 if isRedundant then return var else TS.register var
49 let rankDict' = Map.delete youngRank rankDict
50 T.traverse (mapM registerIfNotRedundant) rankDict'
52 -- For variables with rank youngRank
53 -- If rank < youngRank: register in oldPool
54 -- otherwise generalize
55 let registerIfLowerRank var = do
56 isRedundant <- liftIO $ UF.redundant var
57 case isRedundant of
58 True -> return ()
59 False -> do
60 desc <- liftIO $ UF.descriptor var
61 case _rank desc < youngRank of
62 True ->
63 TS.register var >> return ()
64 False ->
65 liftIO $ UF.setDescriptor var $ desc
66 { _rank = noRank
67 , _content = rigidify (_content desc)
68 }
70 mapM_ registerIfLowerRank (Map.findWithDefault [] youngRank rankDict)
73rigidify :: Content -> Content
74rigidify content =
75 case content of
76 Var Flex maybeSuper _ ->
77 Var Rigid maybeSuper Nothing
79 _ ->
80 content
83-- adjust the ranks of variables such that ranks never increase as you
84-- move deeper into a variable.
85adjustRank :: Int -> Int -> Int -> Variable -> TS.Solver Int
86adjustRank youngMark visitedMark groupRank var =
87 do descriptor <- liftIO $ UF.descriptor var
88 adjustRankHelp youngMark visitedMark groupRank var descriptor
91adjustRankHelp :: Int -> Int -> Int -> Variable -> Descriptor -> TS.Solver Int
92adjustRankHelp youngMark visitedMark groupRank var descriptor =
93 if _mark descriptor == youngMark then
95 do -- Set the variable as marked first because it may be cyclic.
96 liftIO $ UF.modifyDescriptor var $ \desc ->
97 desc { _mark = visitedMark }
99 maxRank <-
100 adjustRankContent youngMark visitedMark groupRank (_content descriptor)
102 liftIO $ UF.modifyDescriptor var $ \desc ->
103 desc { _rank = maxRank }
105 return maxRank
107 else if _mark descriptor /= visitedMark then
109 do let minRank = min groupRank (_rank descriptor)
110 liftIO $ UF.setDescriptor var (descriptor { _mark = visitedMark, _rank = minRank })
111 return minRank
113 else
115 return (_rank descriptor)
118adjustRankContent :: Int -> Int -> Int -> Content -> TS.Solver Int
119adjustRankContent youngMark visitedMark groupRank content =
120 let
121 go = adjustRank youngMark visitedMark groupRank
122 in
123 case content of
124 Error ->
125 return groupRank
127 Atom _ ->
128 return groupRank
130 Var _ _ _ ->
131 return groupRank
133 Alias _ args realVar ->
134 maximum <$> mapM go (realVar : map snd args)
136 Structure (App1 func arg) ->
137 max <$> go func <*> go arg
139 Structure (Fun1 arg result) ->
140 max <$> go arg <*> go result
142 Structure EmptyRecord1 ->
143 return outermostRank
145 Structure (Record1 fields extension) ->
146 maximum <$> mapM go (extension : Map.elems fields)
150-- SOLVER
153solve :: TypeConstraint -> ExceptT [A.Located Error.Error] IO TS.SolverState
154solve constraint =
155 do state <-
156 liftIO (execStateT (actuallySolve constraint) TS.initialState)
157 case TS.sError state of
158 [] ->
159 return state
160 errors ->
161 throwError errors
164actuallySolve :: TypeConstraint -> TS.Solver ()
165actuallySolve constraint =
166 case constraint of
167 CTrue ->
168 return ()
170 CSaveEnv ->
171 TS.saveLocalEnv
173 CEqual hint region term1 term2 ->
174 do t1 <- TS.flatten term1
175 t2 <- TS.flatten term2
176 unify hint region t1 t2
178 CAnd cs ->
179 mapM_ actuallySolve cs
181 CLet [Scheme [] fqs constraint' _] CTrue ->
182 do oldEnv <- TS.getEnv
183 mapM TS.introduce fqs
184 actuallySolve constraint'
185 TS.modifyEnv (\_ -> oldEnv)
187 CLet schemes constraint' ->
188 do oldEnv <- TS.getEnv
189 headers <- Map.unions <$> mapM solveScheme schemes
190 TS.modifyEnv $ \env -> Map.union headers env
191 actuallySolve constraint'
192 mapM occurs $ Map.toList headers
193 TS.modifyEnv (\_ -> oldEnv)
195 CInstance region name term ->
196 do env <- TS.getEnv
197 freshCopy <-
198 case Map.lookup name env of
199 Just (A.A _ tipe) ->
200 TS.makeInstance tipe
202 Nothing ->
203 if List.isPrefixOf "Native." name then
204 liftIO (mkVar Nothing)
206 else
207 error ("Could not find `" ++ name ++ "` when solving type constraints.")
209 t <- TS.flatten term
210 unify (Error.Instance name) region freshCopy t
213solveScheme :: TypeScheme -> TS.Solver (Map.Map String (A.Located Variable))
214solveScheme scheme =
215 let
216 flatten (A.A region term) =
217 A.A region <$> TS.flatten term
218 in
219 case scheme of
220 Scheme [] [] constraint header ->
221 do actuallySolve constraint
222 T.traverse flatten header
224 Scheme rigidQuantifiers flexibleQuantifiers constraint header ->
225 do let quantifiers = rigidQuantifiers ++ flexibleQuantifiers
226 oldPool <- TS.getPool
228 -- fill in a new pool when working on this scheme's constraints
229 freshPool <- TS.nextRankPool
230 TS.switchToPool freshPool
231 mapM TS.introduce quantifiers
232 header' <- T.traverse flatten header
233 actuallySolve constraint
235 allDistinct rigidQuantifiers
236 youngPool <- TS.getPool
237 TS.switchToPool oldPool
238 generalize youngPool
239 mapM isGeneric rigidQuantifiers
240 return header'
243-- ADDITIONAL CHECKS
245-- Checks that all of the given variables belong to distinct equivalence classes.
246-- Also checks that their structure is Nothing, so they represent a variable, not
247-- a more complex term.
248allDistinct :: [Variable] -> TS.Solver ()
249allDistinct vars =
250 do seenMark <- TS.uniqueMark
251 forM_ vars $ \var ->
252 do desc <- liftIO $ UF.descriptor var
253 case _content desc of
254 Structure _ ->
255 crash "Can only generalize type variables, not structures."
257 Atom _ ->
258 crash "Can only generalize type variables, not structures."
260 Alias _ _ _ ->
261 crash "Can only generalize type variables, not aliases."
263 Error ->
264 crash "Can only generalize type variables, not error types."
266 Var _ _ _ ->
267 if _mark desc == seenMark then
268 crash "Duplicate variable during generalization."
270 else
271 liftIO (UF.setDescriptor var (desc { _mark = seenMark }))
274-- Check that a variable has rank == noRank, meaning that it can be generalized.
275isGeneric :: Variable -> TS.Solver ()
276isGeneric var =
277 do desc <- liftIO $ UF.descriptor var
278 if _rank desc == noRank
279 then return ()
280 else crash "Unable to generalize a type variable. It is not unranked."
283crash :: String -> a
284crash msg =
285 error $
286 "It looks like something went wrong with the type inference algorithm.\n\n"
287 ++ msg ++ "\n\n"
288 ++ "Please create a minimal example that triggers this problem and report it to\n"
289 ++ "<https://github.com/elm-lang/elm-compiler/issues>"
293-- OCCURS CHECK
296occurs :: (String, A.Located Variable) -> TS.Solver ()
297occurs (name, A.A region variable) =
298 do isInfinite <- liftIO $ occursHelp [] variable
299 case isInfinite of
300 False ->
301 return ()
303 True ->
304 do overallType <- liftIO (Type.toSrcType variable)
305 TS.addError region (Error.InfiniteType name overallType)
308occursHelp :: [Variable] -> Variable -> IO Bool
309occursHelp seen var =
310 if elem var seen then
311 do infiniteDescriptor <- UF.descriptor var
312 UF.setDescriptor var (infiniteDescriptor { _content = Error })
313 return True
315 else
316 do desc <- UF.descriptor var
317 case _content desc of
318 Atom _ ->
319 return False
321 Var _ _ _ ->
322 return False
324 Error ->
325 return False
327 Alias _ args _ ->
328 -- TODO is it okay to only check args?
329 or <$> mapM (occursHelp (var:seen) . snd) args
331 Structure term ->
332 let
333 go = occursHelp (var:seen)
334 in
335 case term of
336 App1 a b ->
337 (||) <$> go a <*> go b
339 Fun1 a b ->
340 (||) <$> go a <*> go b
342 EmptyRecord1 ->
343 return False
345 Record1 fields ext ->
346 or <$> mapM go (ext : Map.elems fields)