git.iko.soy/elk
on 769faec help sign in
elk/src/Type/Solve.hs
349 lines 11 kB history raw
1module Type.Solve (solve) where
3import Control.Applicative ((<|>))
4import Control.Monad
5import Control.Monad.State (execStateT, liftIO)
6import Control.Monad.Except (ExceptT, throwError)
7import qualified Data.Foldable as F
8import qualified Data.List as List
9import qualified Data.Map as Map
10import qualified Data.Traversable as T
11import qualified Data.UnionFind.IO as UF
13import qualified AST.Type as Type
14import qualified Reporting.Annotation as A
15import qualified Reporting.Error.Type as Error
16import qualified Type.State as TS
17import Type.Type as Type
18import Type.Unify
22{-| Every variable has rank less than or equal to the maxRank of the pool.
23This sorts variables into the young and old pools accordingly.
24-}
25generalize :: TS.Pool -> TS.Solver ()
26generalize youngPool =
27 do youngMark <- TS.uniqueMark
28 let youngRank = TS.maxRank youngPool
29 let insert dict var =
30 do descriptor <- liftIO $ UF.descriptor var
31 liftIO $ UF.modifyDescriptor var (\desc -> desc { _mark = youngMark })
32 return $ Map.insertWith (++) (_rank descriptor) [var] dict
34 -- Sort the youngPool variables by rank.
35 rankDict <- foldM insert Map.empty (TS.inhabitants youngPool)
37 -- get the ranks right for each entry.
38 -- start at low ranks so that we only have to pass
39 -- over the information once.
40 visitedMark <- TS.uniqueMark
41 forM (Map.toList rankDict) $ \(poolRank, vars) ->
42 mapM (adjustRank youngMark visitedMark poolRank) vars
44 -- For variables that have rank lowerer than youngRank, register them in
45 -- the old pool if they are not redundant.
46 let registerIfNotRedundant var =
47 do isRedundant <- liftIO $ UF.redundant var
48 if isRedundant then return var else TS.register var
50 let rankDict' = Map.delete youngRank rankDict
51 T.traverse (mapM registerIfNotRedundant) rankDict'
53 -- For variables with rank youngRank
54 -- If rank < youngRank: register in oldPool
55 -- otherwise generalize
56 let registerIfLowerRank var = do
57 isRedundant <- liftIO $ UF.redundant var
58 case isRedundant of
59 True -> return ()
60 False -> do
61 desc <- liftIO $ UF.descriptor var
62 case _rank desc < youngRank of
63 True ->
64 TS.register var >> return ()
65 False ->
66 liftIO $ UF.setDescriptor var $ desc
67 { _rank = noRank
68 , _content = rigidify (_content desc)
69 }
71 mapM_ registerIfLowerRank (Map.findWithDefault [] youngRank rankDict)
74rigidify :: Content -> Content
75rigidify content =
76 case content of
77 Var Flex maybeSuper _ ->
78 Var Rigid maybeSuper Nothing
80 _ ->
81 content
84-- adjust the ranks of variables such that ranks never increase as you
85-- move deeper into a variable.
86adjustRank :: Int -> Int -> Int -> Variable -> TS.Solver Int
87adjustRank youngMark visitedMark groupRank var =
88 do descriptor <- liftIO $ UF.descriptor var
89 adjustRankHelp youngMark visitedMark groupRank var descriptor
92adjustRankHelp :: Int -> Int -> Int -> Variable -> Descriptor -> TS.Solver Int
93adjustRankHelp youngMark visitedMark groupRank var descriptor =
94 if _mark descriptor == youngMark then
96 do -- Set the variable as marked first because it may be cyclic.
97 liftIO $ UF.modifyDescriptor var $ \desc ->
98 desc { _mark = visitedMark }
100 maxRank <-
101 adjustRankContent youngMark visitedMark groupRank (_content descriptor)
103 liftIO $ UF.modifyDescriptor var $ \desc ->
104 desc { _rank = maxRank }
106 return maxRank
108 else if _mark descriptor /= visitedMark then
110 do let minRank = min groupRank (_rank descriptor)
111 liftIO $ UF.setDescriptor var (descriptor { _mark = visitedMark, _rank = minRank })
112 return minRank
114 else
116 return (_rank descriptor)
119adjustRankContent :: Int -> Int -> Int -> Content -> TS.Solver Int
120adjustRankContent youngMark visitedMark groupRank content =
121 let
122 go = adjustRank youngMark visitedMark groupRank
123 in
124 case content of
125 Error ->
126 return groupRank
128 Atom _ ->
129 return groupRank
131 Var _ _ _ ->
132 return groupRank
134 Alias _ args realVar ->
135 maximum <$> mapM go (realVar : map snd args)
137 Structure (App1 func arg) ->
138 max <$> go func <*> go arg
140 Structure (Fun1 arg result) ->
141 max <$> go arg <*> go result
143 Structure EmptyRecord1 ->
144 return outermostRank
146 Structure (Record1 fields extension) ->
147 maximum <$> mapM go (extension : Map.elems fields)
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 maybeInfinite <- liftIO $ occursHelp [] variable
300 case maybeInfinite of
301 Nothing ->
302 return ()
304 Just infiniteType ->
305 do overallType <- liftIO (Type.toSrcType variable)
306 TS.addError region (Error.InfiniteType name overallType infiniteType)
309occursHelp :: [Variable] -> Variable -> IO (Maybe Type.Canonical)
310occursHelp seen var =
311 if elem var seen then
312 do infiniteDescriptor <- UF.descriptor var
313 structureVar <- UF.fresh infiniteDescriptor
314 UF.setDescriptor var (infiniteDescriptor { _content = Error })
315 srcVar <- Type.toSrcType structureVar
316 return (Just srcVar)
318 else
319 do desc <- UF.descriptor var
320 case _content desc of
321 Atom _ ->
322 return Nothing
324 Var _ _ _ ->
325 return Nothing
327 Error ->
328 return Nothing
330 Alias _ args _ ->
331 -- TODO is it okay to only check args?
332 F.asum <$> mapM (occursHelp (var:seen) . snd) args
334 Structure term ->
335 let
336 go = occursHelp (var:seen)
337 in
338 case term of
339 App1 a b ->
340 (<|>) <$> go a <*> go b
342 Fun1 a b ->
343 (<|>) <$> go a <*> go b
345 EmptyRecord1 ->
346 return Nothing
348 Record1 fields ext ->
349 F.asum <$> mapM go (ext : Map.elems fields)