git.iko.soy/elk
on fcf5cef help sign in
elk/src/Type/Solve.hs
316 lines 9.5 kB history raw
1{-# OPTIONS_GHC -Wall #-}
2module Type.Solve (solve) where
4import Control.Monad
5import Control.Monad.State (execStateT, liftIO)
6import Control.Monad.Except (ExceptT, throwError)
7import qualified Data.List as List
8import qualified Data.Map as Map
9import qualified Data.Foldable as F
10import qualified Data.UnionFind.IO as UF
12import qualified Reporting.Annotation as A
13import qualified Reporting.Error.Type as Error
14import qualified Type.State as TS
15import Type.Type as Type
16import Type.Unify
20{-| Every variable has rank less than or equal to the maxRank of the pool.
21This sorts variables into the young and old pools accordingly.
22-}
23generalize :: TS.Pool -> TS.Solver ()
24generalize youngPool =
25 do youngMark <- TS.uniqueMark
26 let youngRank = TS.maxRank youngPool
27 let insert dict var =
28 do descriptor <- liftIO $ UF.descriptor var
29 liftIO $ UF.modifyDescriptor var (\desc -> desc { _mark = youngMark })
30 return $ Map.insertWith (++) (_rank descriptor) [var] dict
32 -- Sort the youngPool variables by rank.
33 rankDict <- foldM insert Map.empty (TS.inhabitants youngPool)
35 -- get the ranks right for each entry.
36 -- start at low ranks so that we only have to pass
37 -- over the information once.
38 visitedMark <- TS.uniqueMark
39 forM_ (Map.toList rankDict) $ \(poolRank, vars) ->
40 mapM (adjustRank youngMark visitedMark poolRank) vars
42 -- For variables that have rank lowerer than youngRank, register them in
43 -- the old pool if they are not redundant.
44 let registerIfNotRedundant var =
45 do isRedundant <- liftIO $ UF.redundant var
46 if isRedundant then return var else TS.register var
48 let rankDict' = Map.delete youngRank rankDict
49 F.traverse_ (mapM registerIfNotRedundant) rankDict'
51 -- For variables with rank youngRank
52 -- If rank < youngRank: register in oldPool
53 -- otherwise generalize
54 let registerIfLowerRank var = do
55 isRedundant <- liftIO $ UF.redundant var
56 case isRedundant of
57 True -> return ()
58 False -> do
59 desc <- liftIO $ UF.descriptor var
60 case _rank desc < youngRank of
61 True ->
62 TS.register var >> return ()
63 False ->
64 liftIO $ UF.setDescriptor var $ desc
65 { _rank = noRank
66 , _content = rigidify (_content desc)
67 }
69 mapM_ registerIfLowerRank (Map.findWithDefault [] youngRank rankDict)
72rigidify :: Content -> Content
73rigidify content =
74 case content of
75 Var Flex maybeSuper maybeName ->
76 Var Rigid maybeSuper maybeName
78 _ ->
79 content
82-- adjust the ranks of variables such that ranks never increase as you
83-- move deeper into a variable.
84adjustRank :: Int -> Int -> Int -> Variable -> TS.Solver Int
85adjustRank youngMark visitedMark groupRank var =
86 do descriptor <- liftIO $ UF.descriptor var
87 adjustRankHelp youngMark visitedMark groupRank var descriptor
90adjustRankHelp :: Int -> Int -> Int -> Variable -> Descriptor -> TS.Solver Int
91adjustRankHelp youngMark visitedMark groupRank var descriptor =
92 if _mark descriptor == youngMark then
94 do -- Set the variable as marked first because it may be cyclic.
95 liftIO $ UF.modifyDescriptor var $ \desc ->
96 desc { _mark = visitedMark }
98 maxRank <-
99 adjustRankContent youngMark visitedMark groupRank (_content descriptor)
101 liftIO $ UF.modifyDescriptor var $ \desc ->
102 desc { _rank = maxRank }
104 return maxRank
106 else if _mark descriptor /= visitedMark then
108 do let minRank = min groupRank (_rank descriptor)
109 liftIO $ UF.setDescriptor var (descriptor { _mark = visitedMark, _rank = minRank })
110 return minRank
112 else
114 return (_rank descriptor)
117adjustRankContent :: Int -> Int -> Int -> Content -> TS.Solver Int
118adjustRankContent youngMark visitedMark groupRank content =
119 let
120 go = adjustRank youngMark visitedMark groupRank
121 in
122 case content of
123 Error ->
124 return groupRank
126 Atom _ ->
127 return groupRank
129 Var _ _ _ ->
130 return groupRank
132 Alias _ args realVar ->
133 maximum <$> mapM go (realVar : map snd args)
135 Structure (App1 func arg) ->
136 max <$> go func <*> go arg
138 Structure (Fun1 arg result) ->
139 max <$> go arg <*> go result
141 Structure EmptyRecord1 ->
142 return outermostRank
144 Structure (Record1 fields extension) ->
145 maximum <$> mapM go (extension : Map.elems fields)
149-- SOLVER
152solve :: TypeConstraint -> ExceptT [A.Located Error.Error] IO TS.SolverState
153solve constraint =
154 do state <-
155 liftIO (execStateT (actuallySolve constraint) TS.initialState)
156 case TS.sError state of
157 [] ->
158 return state
159 errors ->
160 throwError errors
163actuallySolve :: TypeConstraint -> TS.Solver ()
164actuallySolve constraint =
165 case constraint of
166 CTrue ->
167 return ()
169 CSaveEnv ->
170 TS.saveLocalEnv
172 CEqual hint region term1 term2 ->
173 do t1 <- TS.flatten term1
174 t2 <- TS.flatten term2
175 unify hint region t1 t2
177 CAnd cs ->
178 mapM_ actuallySolve cs
180 CLet [Scheme [] fqs constraint' _] CTrue ->
181 do oldEnv <- TS.getEnv
182 mapM_ TS.introduce fqs
183 actuallySolve constraint'
184 TS.modifyEnv (\_ -> oldEnv)
186 CLet schemes constraint' ->
187 do oldEnv <- TS.getEnv
188 headers <- Map.unions <$> mapM solveScheme schemes
189 TS.modifyEnv $ \env -> Map.union headers env
190 actuallySolve constraint'
191 mapM_ occurs $ Map.toList headers
192 TS.modifyEnv (\_ -> oldEnv)
194 CInstance region name term ->
195 do env <- TS.getEnv
196 freshCopy <-
197 case Map.lookup name env of
198 Just (A.A _ tipe) ->
199 TS.makeInstance tipe
201 Nothing ->
202 if List.isPrefixOf "Native." name then
203 liftIO (mkVar Nothing)
205 else
206 error ("Could not find `" ++ name ++ "` when solving type constraints.")
208 t <- TS.flatten term
209 unify (Error.Instance name) region freshCopy t
212solveScheme :: TypeScheme -> TS.Solver (Map.Map String (A.Located Variable))
213solveScheme scheme =
214 let
215 flatten (A.A region term) =
216 A.A region <$> TS.flatten term
217 in
218 case scheme of
219 Scheme [] [] constraint header ->
220 do actuallySolve constraint
221 traverse flatten header
223 Scheme rigidQuantifiers flexibleQuantifiers constraint header ->
224 do let quantifiers = rigidQuantifiers ++ flexibleQuantifiers
225 oldPool <- TS.getPool
227 -- fill in a new pool when working on this scheme's constraints
228 freshPool <- TS.nextRankPool
229 TS.switchToPool freshPool
230 mapM_ TS.introduce quantifiers
231 header' <- traverse flatten header
232 actuallySolve constraint
234 youngPool <- TS.getPool
235 TS.switchToPool oldPool
236 generalize youngPool
237 mapM_ isGeneric rigidQuantifiers
238 return header'
241-- ADDITIONAL CHECKS
244-- Check that a variable has rank == noRank, meaning that it can be generalized.
245isGeneric :: Variable -> TS.Solver ()
246isGeneric var =
247 do desc <- liftIO $ UF.descriptor var
248 if _rank desc == noRank
249 then return ()
250 else crash "Unable to generalize a type variable. It is not unranked."
253crash :: String -> a
254crash msg =
255 error $
256 "It looks like something went wrong with the type inference algorithm.\n\n"
257 ++ msg ++ "\n\n"
258 ++ "Please create a minimal example that triggers this problem and report it to\n"
259 ++ "<https://github.com/elm-lang/elm-compiler/issues>"
263-- OCCURS CHECK
266occurs :: (String, A.Located Variable) -> TS.Solver ()
267occurs (name, A.A region variable) =
268 do hasOccurred <- liftIO $ occursHelp [] variable
269 case hasOccurred of
270 False ->
271 return ()
273 True ->
274 do overallType <- liftIO (Type.toSrcType variable)
275 TS.addError region (Error.InfiniteType name overallType)
278occursHelp :: [Variable] -> Variable -> IO Bool
279occursHelp seen var =
280 if elem var seen then
281 do infiniteDescriptor <- UF.descriptor var
282 UF.setDescriptor var (infiniteDescriptor { _content = Error })
283 return True
285 else
286 do desc <- UF.descriptor var
287 case _content desc of
288 Atom _ ->
289 return False
291 Var _ _ _ ->
292 return False
294 Error ->
295 return False
297 Alias _ args _ ->
298 -- TODO is it okay to only check args?
299 or <$> mapM (occursHelp (var:seen) . snd) args
301 Structure term ->
302 let
303 go = occursHelp (var:seen)
304 in
305 case term of
306 App1 a b ->
307 (||) <$> go a <*> go b
309 Fun1 a b ->
310 (||) <$> go a <*> go b
312 EmptyRecord1 ->
313 return False
315 Record1 fields ext ->
316 or <$> mapM go (ext : Map.elems fields)