git.iko.soy/elk
on 314be83 help sign in
elk/src/Type/Solve.hs
317 lines 9.5 kB history raw
1{-# OPTIONS_GHC -Wall #-}
2{-# LANGUAGE OverloadedStrings #-}
3module Type.Solve (solve) where
5import Control.Monad
6import Control.Monad.Except (ExceptT, liftIO, throwError)
7import qualified Data.Foldable as F
8import qualified Data.Map as Map
9import qualified Data.Text as Text
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 liftIO $ forM_ (Map.toList rankDict) $ \(poolRank, vars) ->
40 forM_ vars (adjustRank youngMark visitedMark poolRank)
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_ (F.traverse_ 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 -> IO Int
85adjustRank youngMark visitedMark groupRank var =
86 do descriptor <- UF.descriptor var
87 adjustRankHelp youngMark visitedMark groupRank var descriptor
90adjustRankHelp :: Int -> Int -> Int -> Variable -> Descriptor -> IO Int
91adjustRankHelp youngMark visitedMark groupRank var descriptor@(Descriptor content rank mark _) =
92 if mark == youngMark then
94 do -- Set the variable as marked first because it may be cyclic.
95 UF.modifyDescriptor var $ \desc -> desc { _mark = visitedMark }
97 maxRank <-
98 adjustRankContent youngMark visitedMark groupRank content
100 UF.modifyDescriptor var $ \desc -> desc { _rank = maxRank }
102 return maxRank
104 else if mark /= visitedMark then
106 do let minRank = min groupRank rank
107 UF.setDescriptor var (descriptor { _mark = visitedMark, _rank = minRank })
108 return minRank
110 else
112 return rank
115adjustRankContent :: Int -> Int -> Int -> Content -> IO Int
116adjustRankContent youngMark visitedMark groupRank content =
117 let
118 go = adjustRank youngMark visitedMark groupRank
119 in
120 case content of
121 Error ->
122 return groupRank
124 Atom _ ->
125 return groupRank
127 Var _ _ _ ->
128 return groupRank
130 Alias _ args realVar ->
131 -- TODO do you have to crawl the args?
132 do realRank <- go realVar
133 foldM (\rank (_, argVar) -> max rank <$> go argVar) realRank 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 do extRank <- go extension
146 foldM (\rank field -> max rank <$> go field) extRank fields
150-- SOLVER
153solve :: TypeConstraint -> ExceptT [A.Located Error.Error] IO TS.SolverState
154solve constraint =
155 do state <- liftIO (TS.run (actuallySolve constraint))
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 Text.isPrefixOf "Elm.Kernel." name then
203 liftIO (mkVar Nothing)
205 else
206 error ("Could not find `" ++ Text.unpack name ++ "` when solving type constraints.")
208 t <- TS.flatten term
209 unify (Error.Instance name) region freshCopy t
212solveScheme :: TypeScheme -> TS.Solver TS.Env
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'
242-- ADDITIONAL CHECKS
245-- Check that a variable has rank == noRank, meaning that it can be generalized.
246isGeneric :: Variable -> TS.Solver ()
247isGeneric var =
248 do desc <- liftIO $ UF.descriptor var
249 if _rank desc == noRank
250 then return ()
251 else crash "Unable to generalize a type variable. It is not unranked."
254crash :: String -> a
255crash msg =
256 error $
257 "It looks like something went wrong with the type inference algorithm.\n\n"
258 ++ msg ++ "\n\n"
259 ++ "Please create a minimal example that triggers this problem and report it to\n"
260 ++ "<https://github.com/elm-lang/elm-compiler/issues>"
264-- OCCURS CHECK
267occurs :: (Text.Text, A.Located Variable) -> TS.Solver ()
268occurs (name, A.A region variable) =
269 do hasOccurred <- liftIO $ occursHelp [] variable
270 case hasOccurred of
271 False ->
272 return ()
274 True ->
275 do overallType <- liftIO (Type.toSrcType variable)
276 TS.addError region (Error.InfiniteType name overallType)
279occursHelp :: [Variable] -> Variable -> IO Bool
280occursHelp seen var =
281 if elem var seen then
282 do infiniteDescriptor <- UF.descriptor var
283 UF.setDescriptor var (infiniteDescriptor { _content = Error })
284 return True
286 else
287 do desc <- UF.descriptor var
288 case _content desc of
289 Atom _ ->
290 return False
292 Var _ _ _ ->
293 return False
295 Error ->
296 return False
298 Alias _ args _ ->
299 -- TODO is it okay to only check args?
300 or <$> mapM (occursHelp (var:seen) . snd) args
302 Structure term ->
303 let
304 go = occursHelp (var:seen)
305 in
306 case term of
307 App1 a b ->
308 (||) <$> go a <*> go b
310 Fun1 a b ->
311 (||) <$> go a <*> go b
313 EmptyRecord1 ->
314 return False
316 Record1 fields ext ->
317 or <$> mapM go (ext : Map.elems fields)