git.iko.soy/elk
on ed48cd2 help sign in
elk/src/Type/Solve.hs
295 lines 9.9 kB history raw
1module Type.Solve (solve) where
3import Control.Applicative ((<$>), (<*>), (<|>))
4import Control.Monad
5import Control.Monad.State (StateT, execStateT, liftIO)
6import Control.Monad.Except (ExceptT, throwError)
7import qualified Data.Foldable as F
8import qualified Data.List as List
9import qualified Data.Map as Map
10import qualified Data.Traversable as T
11import qualified Data.UnionFind.IO as UF
13import qualified AST.Type as Type
14import qualified Reporting.Annotation as A
15import qualified Reporting.Error.Type as Error
16import qualified Type.State as TS
17import Type.Type
18import Type.Unify
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 -> StateT TS.SolverState IO ()
25generalize youngPool =
26 do youngMark <- TS.uniqueMark
27 let youngRank = TS.maxRank youngPool
28 let insert dict var =
29 do descriptor <- liftIO $ UF.descriptor var
30 liftIO $ UF.modifyDescriptor var (\desc -> desc { mark = youngMark })
31 return $ Map.insertWith (++) (rank descriptor) [var] dict
33 -- Sort the youngPool variables by rank.
34 rankDict <- foldM insert Map.empty (TS.inhabitants youngPool)
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 forM (Map.toList rankDict) $ \(poolRank, vars) ->
41 mapM (adjustRank youngMark visitedMark poolRank) vars
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 T.traverse (mapM registerIfNotRedundant) rankDict'
52 -- For variables with rank youngRank
53 -- If rank < youngRank: register in oldPool
54 -- otherwise generalize
55 let registerIfLowerRank var = do
56 isRedundant <- liftIO $ UF.redundant var
57 case isRedundant of
58 True -> return ()
59 False -> do
60 desc <- liftIO $ UF.descriptor var
61 case rank desc < youngRank of
62 True -> TS.register var >> return ()
63 False -> do
64 let flex' = case flex desc of { Flexible -> Rigid ; other -> other }
65 liftIO $ UF.setDescriptor var (desc { rank = noRank, flex = flex' })
67 mapM_ registerIfLowerRank (Map.findWithDefault [] youngRank rankDict)
70-- adjust the ranks of variables such that ranks never increase as you
71-- move deeper into a variable.
72adjustRank :: Int -> Int -> Int -> Variable -> StateT TS.SolverState IO Int
73adjustRank youngMark visitedMark groupRank var =
74 do descriptor <- liftIO $ UF.descriptor var
75 case () of
76 () | mark descriptor == youngMark ->
77 do -- Set the variable as marked first because it may be cyclic.
78 liftIO $ UF.modifyDescriptor var $ \desc ->
79 desc { mark = visitedMark }
80 rank' <- maybe (return groupRank) adjustTerm (structure descriptor)
81 liftIO $ UF.modifyDescriptor var $ \desc ->
82 desc { rank = rank' }
83 return rank'
85 | mark descriptor /= visitedMark ->
86 do let rank' = min groupRank (rank descriptor)
87 liftIO $ UF.setDescriptor var (descriptor { mark = visitedMark, rank = rank' })
88 return rank'
90 | otherwise ->
91 return (rank descriptor)
92 where
93 adjust =
94 adjustRank youngMark visitedMark groupRank
96 adjustTerm term =
97 case term of
98 App1 a b ->
99 max `liftM` adjust a `ap` adjust b
101 Fun1 a b ->
102 max `liftM` adjust a `ap` adjust b
104 Var1 x ->
105 adjust x
107 EmptyRecord1 ->
108 return outermostRank
110 Record1 fields extension ->
111 do ranks <- mapM adjust (concat (Map.elems fields))
112 rnk <- adjust extension
113 return . maximum $ rnk : ranks
116-- SOLVER
118solve :: TypeConstraint -> ExceptT [A.Located Error.Error] IO TS.SolverState
119solve constraint =
120 do state <-
121 liftIO (execStateT (actuallySolve constraint) TS.initialState)
122 case TS.sError state of
123 [] ->
124 return state
125 errors ->
126 throwError errors
129actuallySolve :: TypeConstraint -> StateT TS.SolverState IO ()
130actuallySolve constraint =
131 case constraint of
132 CTrue ->
133 return ()
135 CSaveEnv ->
136 TS.saveLocalEnv
138 CEqual hint region term1 term2 ->
139 do t1 <- TS.flatten term1
140 t2 <- TS.flatten term2
141 unify hint region t1 t2
143 CAnd cs ->
144 mapM_ actuallySolve cs
146 CLet [Scheme [] fqs constraint' _] CTrue ->
147 do oldEnv <- TS.getEnv
148 mapM TS.introduce fqs
149 actuallySolve constraint'
150 TS.modifyEnv (\_ -> oldEnv)
152 CLet schemes constraint' ->
153 do oldEnv <- TS.getEnv
154 headers <- Map.unions `fmap` mapM solveScheme schemes
155 TS.modifyEnv $ \env -> Map.union headers env
156 actuallySolve constraint'
157 mapM occurs $ Map.toList headers
158 TS.modifyEnv (\_ -> oldEnv)
160 CInstance region name term ->
161 do env <- TS.getEnv
162 freshCopy <-
163 case Map.lookup name env of
164 Just (A.A _ tipe) ->
165 TS.makeInstance tipe
167 Nothing ->
168 if List.isPrefixOf "Native." name
169 then liftIO (variable Flexible)
170 else error ("Could not find `" ++ name ++ "` when solving type constraints.")
172 t <- TS.flatten term
173 unify (Error.Instance name) region freshCopy t
176solveScheme
177 :: TypeScheme
178 -> StateT TS.SolverState IO (Map.Map String (A.Located Variable))
179solveScheme scheme =
180 let
181 flatten (A.A region term) =
182 A.A region <$> TS.flatten term
183 in
184 case scheme of
185 Scheme [] [] constraint header ->
186 do actuallySolve constraint
187 T.traverse flatten header
189 Scheme rigidQuantifiers flexibleQuantifiers constraint header ->
190 do let quantifiers = rigidQuantifiers ++ flexibleQuantifiers
191 oldPool <- TS.getPool
193 -- fill in a new pool when working on this scheme's constraints
194 freshPool <- TS.nextRankPool
195 TS.switchToPool freshPool
196 mapM TS.introduce quantifiers
197 header' <- T.traverse flatten header
198 actuallySolve constraint
200 allDistinct rigidQuantifiers
201 youngPool <- TS.getPool
202 TS.switchToPool oldPool
203 generalize youngPool
204 mapM isGeneric rigidQuantifiers
205 return header'
208-- ADDITIONAL CHECKS
210-- Checks that all of the given variables belong to distinct equivalence classes.
211-- Also checks that their structure is Nothing, so they represent a variable, not
212-- a more complex term.
213allDistinct :: [Variable] -> StateT TS.SolverState IO ()
214allDistinct vars =
215 do seen <- TS.uniqueMark
216 forM_ vars $ \var ->
217 do desc <- liftIO $ UF.descriptor var
218 case structure desc of
219 Just _ ->
220 crash "Cannot generalize something that is not a type variable."
222 Nothing ->
223 if mark desc == seen
224 then crash "Duplicate variable during generalization."
225 else liftIO (UF.setDescriptor var (desc { mark = seen }))
228-- Check that a variable has rank == noRank, meaning that it can be generalized.
229isGeneric :: Variable -> StateT TS.SolverState IO ()
230isGeneric var =
231 do desc <- liftIO $ UF.descriptor var
232 if rank desc == noRank
233 then return ()
234 else crash "Unable to generalize a type variable. It is not unranked."
237crash :: String -> a
238crash msg =
239 error $
240 "It looks like something went wrong with the type inference algorithm.\n"
241 ++ msg ++ "\n"
242 ++ "Please create a minimal example that triggers this problem and report it to\n"
243 ++ "<https://github.com/elm-lang/elm-compiler/issues>"
246occurs :: (String, A.Located Variable) -> StateT TS.SolverState IO ()
247occurs (name, A.A region variable) =
248 do maybePair <- liftIO $ occursHelp [] variable
249 case maybePair of
250 Nothing ->
251 return ()
253 Just (t1, t2) ->
254 let
255 info = Error.InfiniteTypeInfo name t1 t2
256 in
257 TS.addError region (Error.InfiniteType info)
260occursHelp
261 :: [Variable]
262 -> Variable
263 -> IO (Maybe (Type.Canonical, Type.Canonical))
264occursHelp seen var =
265 if elem var seen then
266 do desc <- UF.descriptor var
267 UF.setDescriptor var (desc { structure = Nothing })
268 var' <- UF.fresh desc
269 srcVar <- toSrcType var
270 srcVar' <- toSrcType var'
271 return (Just (srcVar, srcVar'))
272 else
273 do desc <- UF.descriptor var
274 case structure desc of
275 Nothing ->
276 return Nothing
278 Just struct ->
279 let go = occursHelp (var:seen)
280 in
281 case struct of
282 App1 a b ->
283 (<|>) <$> go a <*> go b
285 Fun1 a b ->
286 (<|>) <$> go a <*> go b
288 Var1 a ->
289 go a
291 EmptyRecord1 ->
292 return Nothing
294 Record1 fields ext ->
295 F.asum <$> mapM go (ext : concat (Map.elems fields))