git.iko.soy/elk
on e00a3f3 help sign in
elk/src/Type/Solve.hs
319 lines 9.8 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
11import qualified AST.Module.Name as ModuleName
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
17import qualified Type.UnionFind as UF
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 (TS.Pool youngRank youngInhabitants) =
26 {-# SCC elm_compiler_type_generalize #-}
27 do youngMark <- TS.uniqueMark
28 let insert dict var =
29 {-# SCC elm_compiler_type_insert #-}
30 do descriptor <- UF.descriptor var
31 UF.modifyDescriptor var (\desc -> desc { _mark = youngMark })
32 return $ Map.insertWith (++) (_rank descriptor) [var] dict
34 -- Sort the youngPool variables by rank.
35 rankDict <- liftIO $ foldM insert Map.empty youngInhabitants
37 -- get the ranks right for each entry.
38 -- start at low ranks so that we only have to pass
39 -- over the information once.
40 visitedMark <- TS.uniqueMark
41 liftIO $ forM_ (Map.toList rankDict) $ \(poolRank, vars) ->
42 forM_ vars (adjustRank youngMark visitedMark poolRank)
44 -- For variables that have rank lowerer than youngRank, register them in
45 -- the old pool if they are not redundant.
46 let registerIfNotRedundant var =
47 do isRedundant <- liftIO $ UF.redundant var
48 if isRedundant then return var else TS.register var
50 let rankDict' = Map.delete youngRank rankDict
51 F.traverse_ (F.traverse_ registerIfNotRedundant) rankDict'
53 -- For variables with rank youngRank
54 -- If rank < youngRank: register in oldPool
55 -- otherwise generalize
56 let registerIfLowerRank var =
57 {-# SCC elm_compiler_type_register #-}
58 do isRedundant <- liftIO $ UF.redundant var
59 case isRedundant of
60 True -> return ()
61 False -> do
62 desc <- liftIO $ UF.descriptor var
63 case _rank desc < youngRank of
64 True ->
65 TS.register var >> return ()
66 False ->
67 liftIO $ UF.setDescriptor var $ desc
68 { _rank = noRank
69 , _content = rigidify (_content desc)
70 }
72 mapM_ registerIfLowerRank (Map.findWithDefault [] youngRank rankDict)
75rigidify :: Content -> Content
76rigidify content =
77 case content of
78 Var Flex maybeSuper maybeName ->
79 Var Rigid maybeSuper maybeName
81 _ ->
82 content
85-- adjust the ranks of variables such that ranks never increase as you
86-- move deeper into a variable.
87adjustRank :: Int -> Int -> Int -> Variable -> IO Int
88adjustRank youngMark visitedMark groupRank var =
89 {-# SCC elm_compiler_type_adjust #-}
90 do descriptor <- UF.descriptor var
91 adjustRankHelp youngMark visitedMark groupRank var descriptor
94adjustRankHelp :: Int -> Int -> Int -> Variable -> Descriptor -> IO Int
95adjustRankHelp youngMark visitedMark groupRank var descriptor@(Descriptor content rank mark _) =
96 if mark == youngMark then
98 do -- Set the variable as marked first because it may be cyclic.
99 UF.modifyDescriptor var $ \desc -> desc { _mark = visitedMark }
100 maxRank <- adjustRankContent youngMark visitedMark groupRank content
101 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 :: Constraint -> ExceptT [A.Located Error.Error] IO TS.State
154solve constraint =
155 {-# SCC elm_compiler_type_solve #-}
156 do state <- liftIO (TS.run (actuallySolve constraint))
157 case TS.sError state of
158 [] ->
159 return state
160 errors ->
161 throwError errors
164actuallySolve :: Constraint -> 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 ModuleName.isKernel 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 :: Scheme -> 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 {-# SCC elm_compiler_type_occurs #-}
271 do hasOccurred <- liftIO $ occursHelp [] variable
272 case hasOccurred of
273 False ->
274 return ()
276 True ->
277 do overallType <- liftIO (Type.toSrcType variable)
278 TS.addError region (Error.InfiniteType name overallType)
281occursHelp :: [Variable] -> Variable -> IO Bool
282occursHelp seen var =
283 if elem var seen then
284 do infiniteDescriptor <- UF.descriptor var
285 UF.setDescriptor var (infiniteDescriptor { _content = Error })
286 return True
288 else
289 do desc <- UF.descriptor var
290 case _content desc of
291 Atom _ ->
292 return False
294 Var _ _ _ ->
295 return False
297 Error ->
298 return False
300 Alias _ args _ ->
301 -- TODO is it okay to only check args?
302 or <$> mapM (occursHelp (var:seen) . snd) args
304 Structure term ->
305 let
306 go = occursHelp (var:seen)
307 in
308 case term of
309 App1 a b ->
310 (||) <$> go a <*> go b
312 Fun1 a b ->
313 (||) <$> go a <*> go b
315 EmptyRecord1 ->
316 return False
318 Record1 fields ext ->
319 or <$> mapM go (ext : Map.elems fields)