git.iko.soy/elk
on 3734eff help sign in
elk/src/Type/Solve.hs
320 lines 9.7 kB history raw
1{-# OPTIONS_GHC -Wall #-}
2{-# LANGUAGE OverloadedStrings #-}
3module Type.Solve (solve) where
5import Control.Monad
6import Control.Monad.State (execStateT, liftIO)
7import Control.Monad.Except (ExceptT, throwError)
8import qualified Data.Foldable as F
9import qualified Data.Map as Map
10import qualified Data.Text as Text
11import qualified Data.UnionFind.IO as UF
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 forM_ vars (adjustRank youngMark visitedMark poolRank)
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 F.traverse_ (F.traverse_ 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 maybeName ->
77 Var Rigid maybeSuper maybeName
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 do realRank <- go realVar
135 foldM (\rank (_, argVar) -> max rank <$> go argVar) realRank 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 do extRank <- go extension
148 foldM (\rank field -> max rank <$> go field) extRank fields
152-- SOLVER
155solve :: TypeConstraint -> ExceptT [A.Located Error.Error] IO TS.SolverState
156solve constraint =
157 do state <-
158 liftIO (execStateT (actuallySolve constraint) TS.initialState)
159 case TS.sError state of
160 [] ->
161 return state
162 errors ->
163 throwError errors
166actuallySolve :: TypeConstraint -> TS.Solver ()
167actuallySolve constraint =
168 case constraint of
169 CTrue ->
170 return ()
172 CSaveEnv ->
173 TS.saveLocalEnv
175 CEqual hint region term1 term2 ->
176 do t1 <- TS.flatten term1
177 t2 <- TS.flatten term2
178 unify hint region t1 t2
180 CAnd cs ->
181 mapM_ actuallySolve cs
183 CLet [Scheme [] fqs constraint' _] CTrue ->
184 do oldEnv <- TS.getEnv
185 mapM_ TS.introduce fqs
186 actuallySolve constraint'
187 TS.modifyEnv (\_ -> oldEnv)
189 CLet schemes constraint' ->
190 do oldEnv <- TS.getEnv
191 headers <- Map.unions <$> mapM solveScheme schemes
192 TS.modifyEnv $ \env -> Map.union headers env
193 actuallySolve constraint'
194 mapM_ occurs $ Map.toList headers
195 TS.modifyEnv (\_ -> oldEnv)
197 CInstance region name term ->
198 do env <- TS.getEnv
199 freshCopy <-
200 case Map.lookup name env of
201 Just (A.A _ tipe) ->
202 TS.makeInstance tipe
204 Nothing ->
205 if Text.isPrefixOf "Elm.Kernel." name then
206 liftIO (mkVar Nothing)
208 else
209 error ("Could not find `" ++ Text.unpack name ++ "` when solving type constraints.")
211 t <- TS.flatten term
212 unify (Error.Instance name) region freshCopy t
215solveScheme :: TypeScheme -> TS.Solver TS.Env
216solveScheme scheme =
217 let
218 flatten (A.A region term) =
219 A.A region <$> TS.flatten term
220 in
221 case scheme of
222 Scheme [] [] constraint header ->
223 do actuallySolve constraint
224 traverse flatten header
226 Scheme rigidQuantifiers flexibleQuantifiers constraint header ->
227 do let quantifiers = rigidQuantifiers ++ flexibleQuantifiers
228 oldPool <- TS.getPool
230 -- fill in a new pool when working on this scheme's constraints
231 freshPool <- TS.nextRankPool
232 TS.switchToPool freshPool
233 mapM_ TS.introduce quantifiers
234 header' <- traverse flatten header
235 actuallySolve constraint
237 youngPool <- TS.getPool
238 TS.switchToPool oldPool
239 generalize youngPool
240 mapM_ isGeneric rigidQuantifiers
241 return header'
245-- ADDITIONAL CHECKS
248-- Check that a variable has rank == noRank, meaning that it can be generalized.
249isGeneric :: Variable -> TS.Solver ()
250isGeneric var =
251 do desc <- liftIO $ UF.descriptor var
252 if _rank desc == noRank
253 then return ()
254 else crash "Unable to generalize a type variable. It is not unranked."
257crash :: String -> a
258crash msg =
259 error $
260 "It looks like something went wrong with the type inference algorithm.\n\n"
261 ++ msg ++ "\n\n"
262 ++ "Please create a minimal example that triggers this problem and report it to\n"
263 ++ "<https://github.com/elm-lang/elm-compiler/issues>"
267-- OCCURS CHECK
270occurs :: (Text.Text, A.Located Variable) -> TS.Solver ()
271occurs (name, A.A region variable) =
272 do hasOccurred <- liftIO $ occursHelp [] variable
273 case hasOccurred of
274 False ->
275 return ()
277 True ->
278 do overallType <- liftIO (Type.toSrcType variable)
279 TS.addError region (Error.InfiniteType name overallType)
282occursHelp :: [Variable] -> Variable -> IO Bool
283occursHelp seen var =
284 if elem var seen then
285 do infiniteDescriptor <- UF.descriptor var
286 UF.setDescriptor var (infiniteDescriptor { _content = Error })
287 return True
289 else
290 do desc <- UF.descriptor var
291 case _content desc of
292 Atom _ ->
293 return False
295 Var _ _ _ ->
296 return False
298 Error ->
299 return False
301 Alias _ args _ ->
302 -- TODO is it okay to only check args?
303 or <$> mapM (occursHelp (var:seen) . snd) args
305 Structure term ->
306 let
307 go = occursHelp (var:seen)
308 in
309 case term of
310 App1 a b ->
311 (||) <$> go a <*> go b
313 Fun1 a b ->
314 (||) <$> go a <*> go b
316 EmptyRecord1 ->
317 return False
319 Record1 fields ext ->
320 or <$> mapM go (ext : Map.elems fields)