git.iko.soy/elk
on fe7bbbd help sign in
elk/src/Type/Solve.hs
318 lines 9.5 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 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 F.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 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 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 Text.isPrefixOf "Native." name then
204 liftIO (mkVar Nothing)
206 else
207 error ("Could not find `" ++ Text.unpack name ++ "` when solving type constraints.")
209 t <- TS.flatten term
210 unify (Error.Instance name) region freshCopy t
213solveScheme :: TypeScheme -> TS.Solver TS.Env
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 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' <- traverse flatten header
233 actuallySolve constraint
235 youngPool <- TS.getPool
236 TS.switchToPool oldPool
237 generalize youngPool
238 mapM_ isGeneric rigidQuantifiers
239 return header'
243-- ADDITIONAL CHECKS
246-- Check that a variable has rank == noRank, meaning that it can be generalized.
247isGeneric :: Variable -> TS.Solver ()
248isGeneric var =
249 do desc <- liftIO $ UF.descriptor var
250 if _rank desc == noRank
251 then return ()
252 else crash "Unable to generalize a type variable. It is not unranked."
255crash :: String -> a
256crash msg =
257 error $
258 "It looks like something went wrong with the type inference algorithm.\n\n"
259 ++ msg ++ "\n\n"
260 ++ "Please create a minimal example that triggers this problem and report it to\n"
261 ++ "<https://github.com/elm-lang/elm-compiler/issues>"
265-- OCCURS CHECK
268occurs :: (Text.Text, A.Located Variable) -> TS.Solver ()
269occurs (name, A.A region variable) =
270 do hasOccurred <- liftIO $ occursHelp [] variable
271 case hasOccurred of
272 False ->
273 return ()
275 True ->
276 do overallType <- liftIO (Type.toSrcType variable)
277 TS.addError region (Error.InfiniteType name overallType)
280occursHelp :: [Variable] -> Variable -> IO Bool
281occursHelp seen var =
282 if elem var seen then
283 do infiniteDescriptor <- UF.descriptor var
284 UF.setDescriptor var (infiniteDescriptor { _content = Error })
285 return True
287 else
288 do desc <- UF.descriptor var
289 case _content desc of
290 Atom _ ->
291 return False
293 Var _ _ _ ->
294 return False
296 Error ->
297 return False
299 Alias _ args _ ->
300 -- TODO is it okay to only check args?
301 or <$> mapM (occursHelp (var:seen) . snd) args
303 Structure term ->
304 let
305 go = occursHelp (var:seen)
306 in
307 case term of
308 App1 a b ->
309 (||) <$> go a <*> go b
311 Fun1 a b ->
312 (||) <$> go a <*> go b
314 EmptyRecord1 ->
315 return False
317 Record1 fields ext ->
318 or <$> mapM go (ext : Map.elems fields)