git.iko.soy/elk
on dcce951 help sign in
elk/src/Type/Solve.hs
315 lines 9.5 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 maybeName ->
75 Var Rigid maybeSuper maybeName
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 youngPool <- TS.getPool
234 TS.switchToPool oldPool
235 generalize youngPool
236 mapM isGeneric rigidQuantifiers
237 return header'
240-- ADDITIONAL CHECKS
243-- Check that a variable has rank == noRank, meaning that it can be generalized.
244isGeneric :: Variable -> TS.Solver ()
245isGeneric var =
246 do desc <- liftIO $ UF.descriptor var
247 if _rank desc == noRank
248 then return ()
249 else crash "Unable to generalize a type variable. It is not unranked."
252crash :: String -> a
253crash msg =
254 error $
255 "It looks like something went wrong with the type inference algorithm.\n\n"
256 ++ msg ++ "\n\n"
257 ++ "Please create a minimal example that triggers this problem and report it to\n"
258 ++ "<https://github.com/elm-lang/elm-compiler/issues>"
262-- OCCURS CHECK
265occurs :: (String, A.Located Variable) -> TS.Solver ()
266occurs (name, A.A region variable) =
267 do isInfinite <- liftIO $ occursHelp [] variable
268 case isInfinite of
269 False ->
270 return ()
272 True ->
273 do overallType <- liftIO (Type.toSrcType variable)
274 TS.addError region (Error.InfiniteType name overallType)
277occursHelp :: [Variable] -> Variable -> IO Bool
278occursHelp seen var =
279 if elem var seen then
280 do infiniteDescriptor <- UF.descriptor var
281 UF.setDescriptor var (infiniteDescriptor { _content = Error })
282 return True
284 else
285 do desc <- UF.descriptor var
286 case _content desc of
287 Atom _ ->
288 return False
290 Var _ _ _ ->
291 return False
293 Error ->
294 return False
296 Alias _ args _ ->
297 -- TODO is it okay to only check args?
298 or <$> mapM (occursHelp (var:seen) . snd) args
300 Structure term ->
301 let
302 go = occursHelp (var:seen)
303 in
304 case term of
305 App1 a b ->
306 (||) <$> go a <*> go b
308 Fun1 a b ->
309 (||) <$> go a <*> go b
311 EmptyRecord1 ->
312 return False
314 Record1 fields ext ->
315 or <$> mapM go (ext : Map.elems fields)