git.iko.soy/elk
on df41ae8 help sign in
elk/src/Type/Solve.hs
344 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)
148-- SOLVER
151solve :: TypeConstraint -> ExceptT [A.Located Error.Error] IO TS.SolverState
152solve constraint =
153 do state <-
154 liftIO (execStateT (actuallySolve constraint) TS.initialState)
155 case TS.sError state of
156 [] ->
157 return state
158 errors ->
159 throwError errors
162actuallySolve :: TypeConstraint -> TS.Solver ()
163actuallySolve constraint =
164 case constraint of
165 CTrue ->
166 return ()
168 CSaveEnv ->
169 TS.saveLocalEnv
171 CEqual hint region term1 term2 ->
172 do t1 <- TS.flatten term1
173 t2 <- TS.flatten term2
174 unify hint region t1 t2
176 CAnd cs ->
177 mapM_ actuallySolve cs
179 CLet [Scheme [] fqs constraint' _] CTrue ->
180 do oldEnv <- TS.getEnv
181 mapM TS.introduce fqs
182 actuallySolve constraint'
183 TS.modifyEnv (\_ -> oldEnv)
185 CLet schemes constraint' ->
186 do oldEnv <- TS.getEnv
187 headers <- Map.unions <$> mapM solveScheme schemes
188 TS.modifyEnv $ \env -> Map.union headers env
189 actuallySolve constraint'
190 mapM occurs $ Map.toList headers
191 TS.modifyEnv (\_ -> oldEnv)
193 CInstance region name term ->
194 do env <- TS.getEnv
195 freshCopy <-
196 case Map.lookup name env of
197 Just (A.A _ tipe) ->
198 TS.makeInstance tipe
200 Nothing ->
201 if List.isPrefixOf "Native." name then
202 liftIO (mkVar Nothing)
204 else
205 error ("Could not find `" ++ name ++ "` when solving type constraints.")
207 t <- TS.flatten term
208 unify (Error.Instance name) region freshCopy t
211solveScheme :: TypeScheme -> TS.Solver (Map.Map String (A.Located Variable))
212solveScheme scheme =
213 let
214 flatten (A.A region term) =
215 A.A region <$> TS.flatten term
216 in
217 case scheme of
218 Scheme [] [] constraint header ->
219 do actuallySolve constraint
220 T.traverse flatten header
222 Scheme rigidQuantifiers flexibleQuantifiers constraint header ->
223 do let quantifiers = rigidQuantifiers ++ flexibleQuantifiers
224 oldPool <- TS.getPool
226 -- fill in a new pool when working on this scheme's constraints
227 freshPool <- TS.nextRankPool
228 TS.switchToPool freshPool
229 mapM TS.introduce quantifiers
230 header' <- T.traverse flatten header
231 actuallySolve constraint
233 allDistinct rigidQuantifiers
234 youngPool <- TS.getPool
235 TS.switchToPool oldPool
236 generalize youngPool
237 mapM isGeneric rigidQuantifiers
238 return header'
241-- ADDITIONAL CHECKS
243-- Checks that all of the given variables belong to distinct equivalence classes.
244-- Also checks that their structure is Nothing, so they represent a variable, not
245-- a more complex term.
246allDistinct :: [Variable] -> TS.Solver ()
247allDistinct vars =
248 do seenMark <- TS.uniqueMark
249 forM_ vars $ \var ->
250 do desc <- liftIO $ UF.descriptor var
251 case _content desc of
252 Structure _ ->
253 crash "Can only generalize type variables, not structures."
255 Atom _ ->
256 crash "Can only generalize type variables, not structures."
258 Alias _ _ _ ->
259 crash "Can only generalize type variables, not aliases."
261 Error ->
262 crash "Can only generalize type variables, not error types."
264 Var _ _ _ ->
265 if _mark desc == seenMark then
266 crash "Duplicate variable during generalization."
268 else
269 liftIO (UF.setDescriptor var (desc { _mark = seenMark }))
272-- Check that a variable has rank == noRank, meaning that it can be generalized.
273isGeneric :: Variable -> TS.Solver ()
274isGeneric var =
275 do desc <- liftIO $ UF.descriptor var
276 if _rank desc == noRank
277 then return ()
278 else crash "Unable to generalize a type variable. It is not unranked."
281crash :: String -> a
282crash msg =
283 error $
284 "It looks like something went wrong with the type inference algorithm.\n\n"
285 ++ msg ++ "\n\n"
286 ++ "Please create a minimal example that triggers this problem and report it to\n"
287 ++ "<https://github.com/elm-lang/elm-compiler/issues>"
291-- OCCURS CHECK
294occurs :: (String, A.Located Variable) -> TS.Solver ()
295occurs (name, A.A region variable) =
296 do isInfinite <- liftIO $ occursHelp [] variable
297 case isInfinite of
298 False ->
299 return ()
301 True ->
302 do overallType <- liftIO (Type.toSrcType variable)
303 TS.addError region (Error.InfiniteType name overallType)
306occursHelp :: [Variable] -> Variable -> IO Bool
307occursHelp seen var =
308 if elem var seen then
309 do infiniteDescriptor <- UF.descriptor var
310 UF.setDescriptor var (infiniteDescriptor { _content = Error })
311 return True
313 else
314 do desc <- UF.descriptor var
315 case _content desc of
316 Atom _ ->
317 return False
319 Var _ _ _ ->
320 return False
322 Error ->
323 return False
325 Alias _ args _ ->
326 -- TODO is it okay to only check args?
327 or <$> mapM (occursHelp (var:seen) . snd) args
329 Structure term ->
330 let
331 go = occursHelp (var:seen)
332 in
333 case term of
334 App1 a b ->
335 (||) <$> go a <*> go b
337 Fun1 a b ->
338 (||) <$> go a <*> go b
340 EmptyRecord1 ->
341 return False
343 Record1 fields ext ->
344 or <$> mapM go (ext : Map.elems fields)