git.iko.soy/elk
on 5a9bb97 help sign in
elk/src/Type/Solve.hs
316 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 (TS.Pool youngRank youngInhabitants) =
25 do youngMark <- TS.uniqueMark
26 let insert dict var =
27 do descriptor <- UF.descriptor var
28 UF.modifyDescriptor var (\desc -> desc { _mark = youngMark })
29 return $ Map.insertWith (++) (_rank descriptor) [var] dict
31 -- Sort the youngPool variables by rank.
32 rankDict <- liftIO $ foldM insert Map.empty youngInhabitants
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 liftIO $ forM_ (Map.toList rankDict) $ \(poolRank, vars) ->
39 forM_ vars (adjustRank youngMark visitedMark poolRank)
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 F.traverse_ (F.traverse_ 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 -> IO Int
84adjustRank youngMark visitedMark groupRank var =
85 do descriptor <- UF.descriptor var
86 adjustRankHelp youngMark visitedMark groupRank var descriptor
89adjustRankHelp :: Int -> Int -> Int -> Variable -> Descriptor -> IO Int
90adjustRankHelp youngMark visitedMark groupRank var descriptor@(Descriptor content rank mark _) =
91 if mark == youngMark then
93 do -- Set the variable as marked first because it may be cyclic.
94 UF.modifyDescriptor var $ \desc -> desc { _mark = visitedMark }
96 maxRank <-
97 adjustRankContent youngMark visitedMark groupRank content
99 UF.modifyDescriptor var $ \desc -> desc { _rank = maxRank }
101 return maxRank
103 else if mark /= visitedMark then
105 do let minRank = min groupRank rank
106 UF.setDescriptor var (descriptor { _mark = visitedMark, _rank = minRank })
107 return minRank
109 else
111 return rank
114adjustRankContent :: Int -> Int -> Int -> Content -> IO Int
115adjustRankContent youngMark visitedMark groupRank content =
116 let
117 go = adjustRank youngMark visitedMark groupRank
118 in
119 case content of
120 Error ->
121 return groupRank
123 Atom _ ->
124 return groupRank
126 Var _ _ _ ->
127 return groupRank
129 Alias _ args realVar ->
130 -- TODO do you have to crawl the args?
131 do realRank <- go realVar
132 foldM (\rank (_, argVar) -> max rank <$> go argVar) realRank 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 do extRank <- go extension
145 foldM (\rank field -> max rank <$> go field) extRank fields
149-- SOLVER
152solve :: TypeConstraint -> ExceptT [A.Located Error.Error] IO TS.State
153solve constraint =
154 do state <- liftIO (TS.run (actuallySolve constraint))
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 Text.isPrefixOf "Elm.Kernel." name then
202 liftIO (mkVar Nothing)
204 else
205 error ("Could not find `" ++ Text.unpack name ++ "` when solving type constraints.")
207 t <- TS.flatten term
208 unify (Error.Instance name) region freshCopy t
211solveScheme :: TypeScheme -> TS.Solver TS.Env
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 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' <- traverse flatten header
231 actuallySolve constraint
233 youngPool <- TS.getPool
234 TS.switchToPool oldPool
235 generalize youngPool
236 mapM_ isGeneric rigidQuantifiers
237 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 :: (Text.Text, 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)