git.iko.soy/elk
on ae8d75c help sign in
elk/src/Type/Solve.hs
318 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
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 {-# SCC elm_compiler_type_generalize #-}
26 do youngMark <- TS.uniqueMark
27 let insert dict var =
28 {-# SCC elm_compiler_type_insert #-}
29 do descriptor <- UF.descriptor var
30 UF.modifyDescriptor var (\desc -> desc { _mark = youngMark })
31 return $ Map.insertWith (++) (_rank descriptor) [var] dict
33 -- Sort the youngPool variables by rank.
34 rankDict <- liftIO $ foldM insert Map.empty youngInhabitants
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 liftIO $ forM_ (Map.toList rankDict) $ \(poolRank, vars) ->
41 forM_ vars (adjustRank youngMark visitedMark poolRank)
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_ (F.traverse_ registerIfNotRedundant) rankDict'
52 -- For variables with rank youngRank
53 -- If rank < youngRank: register in oldPool
54 -- otherwise generalize
55 let registerIfLowerRank var =
56 {-# SCC elm_compiler_type_register #-}
57 do isRedundant <- liftIO $ UF.redundant var
58 case isRedundant of
59 True -> return ()
60 False -> do
61 desc <- liftIO $ UF.descriptor var
62 case _rank desc < youngRank of
63 True ->
64 TS.register var >> return ()
65 False ->
66 liftIO $ UF.setDescriptor var $ desc
67 { _rank = noRank
68 , _content = rigidify (_content desc)
69 }
71 mapM_ registerIfLowerRank (Map.findWithDefault [] youngRank rankDict)
74rigidify :: Content -> Content
75rigidify content =
76 case content of
77 Var Flex maybeSuper maybeName ->
78 Var Rigid maybeSuper maybeName
80 _ ->
81 content
84-- adjust the ranks of variables such that ranks never increase as you
85-- move deeper into a variable.
86adjustRank :: Int -> Int -> Int -> Variable -> IO Int
87adjustRank youngMark visitedMark groupRank var =
88 {-# SCC elm_compiler_type_adjust #-}
89 do descriptor <- UF.descriptor var
90 adjustRankHelp youngMark visitedMark groupRank var descriptor
93adjustRankHelp :: Int -> Int -> Int -> Variable -> Descriptor -> IO Int
94adjustRankHelp youngMark visitedMark groupRank var descriptor@(Descriptor content rank mark _) =
95 if mark == youngMark then
97 do -- Set the variable as marked first because it may be cyclic.
98 UF.modifyDescriptor var $ \desc -> desc { _mark = visitedMark }
99 maxRank <- adjustRankContent youngMark visitedMark groupRank content
100 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 {-# SCC elm_compiler_type_solve #-}
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 {-# SCC elm_compiler_type_occurs #-}
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)