git.iko.soy/elk
on 33261ec help sign in
elk/src/Type/Solve.hs
279 lines 9.6 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.List as List
8import qualified Data.Map as Map
9import qualified Data.Traversable as Traversable
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
16import Type.Unify
19{-| Every variable has rank less than or equal to the maxRank of the pool.
20This sorts variables into the young and old pools accordingly.
21-}
22generalize :: TS.Pool -> StateT TS.SolverState IO ()
23generalize youngPool =
24 do youngMark <- TS.uniqueMark
25 let youngRank = TS.maxRank youngPool
26 let insert dict var =
27 do descriptor <- liftIO $ UF.descriptor var
28 liftIO $ UF.modifyDescriptor var (\desc -> desc { mark = youngMark })
29 return $ Map.insertWith (++) (rank descriptor) [var] dict
31 -- Sort the youngPool variables by rank.
32 rankDict <- foldM insert Map.empty (TS.inhabitants youngPool)
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 forM (Map.toList rankDict) $ \(poolRank, vars) ->
39 mapM (adjustRank youngMark visitedMark poolRank) vars
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 Traversable.traverse (mapM 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 -> TS.register var >> return ()
61 False -> do
62 let flex' = case flex desc of { Flexible -> Rigid ; other -> other }
63 liftIO $ UF.setDescriptor var (desc { rank = noRank, flex = flex' })
65 mapM_ registerIfLowerRank (Map.findWithDefault [] youngRank rankDict)
68-- adjust the ranks of variables such that ranks never increase as you
69-- move deeper into a variable.
70adjustRank :: Int -> Int -> Int -> Variable -> StateT TS.SolverState IO Int
71adjustRank youngMark visitedMark groupRank var =
72 do descriptor <- liftIO $ UF.descriptor var
73 case () of
74 () | mark descriptor == youngMark ->
75 do -- Set the variable as marked first because it may be cyclic.
76 liftIO $ UF.modifyDescriptor var $ \desc ->
77 desc { mark = visitedMark }
78 rank' <- maybe (return groupRank) adjustTerm (structure descriptor)
79 liftIO $ UF.modifyDescriptor var $ \desc ->
80 desc { rank = rank' }
81 return rank'
83 | mark descriptor /= visitedMark ->
84 do let rank' = min groupRank (rank descriptor)
85 liftIO $ UF.setDescriptor var (descriptor { mark = visitedMark, rank = rank' })
86 return rank'
88 | otherwise ->
89 return (rank descriptor)
90 where
91 adjust =
92 adjustRank youngMark visitedMark groupRank
94 adjustTerm term =
95 case term of
96 App1 a b ->
97 max `liftM` adjust a `ap` adjust b
99 Fun1 a b ->
100 max `liftM` adjust a `ap` adjust b
102 Var1 x ->
103 adjust x
105 EmptyRecord1 ->
106 return outermostRank
108 Record1 fields extension ->
109 do ranks <- mapM adjust (concat (Map.elems fields))
110 rnk <- adjust extension
111 return . maximum $ rnk : ranks
114-- SOLVER
116solve :: TypeConstraint -> ExceptT [A.Located Error.Error] IO TS.SolverState
117solve constraint =
118 do state <-
119 liftIO (execStateT (actuallySolve constraint) TS.initialState)
120 case TS.sError state of
121 [] ->
122 return state
123 errors ->
124 throwError errors
127actuallySolve :: TypeConstraint -> StateT TS.SolverState IO ()
128actuallySolve constraint =
129 case constraint of
130 CTrue ->
131 return ()
133 CSaveEnv ->
134 TS.saveLocalEnv
136 CEqual hint region term1 term2 ->
137 do t1 <- TS.flatten term1
138 t2 <- TS.flatten term2
139 unify hint region t1 t2
141 CAnd cs ->
142 mapM_ actuallySolve cs
144 CLet [Scheme [] fqs constraint' _] CTrue ->
145 do oldEnv <- TS.getEnv
146 mapM TS.introduce fqs
147 actuallySolve constraint'
148 TS.modifyEnv (\_ -> oldEnv)
150 CLet schemes constraint' ->
151 do oldEnv <- TS.getEnv
152 headers <- Map.unions `fmap` mapM solveScheme schemes
153 TS.modifyEnv $ \env -> Map.union headers env
154 actuallySolve constraint'
155 mapM occurs $ Map.toList headers
156 TS.modifyEnv (\_ -> oldEnv)
158 CInstance region name term ->
159 do env <- TS.getEnv
160 freshCopy <-
161 case Map.lookup name env of
162 Just tipe ->
163 TS.makeInstance tipe
164 Nothing ->
165 if List.isPrefixOf "Native." name
166 then liftIO (variable Flexible)
167 else error ("Could not find '" ++ name ++ "' when solving type constraints.")
169 t <- TS.flatten term
170 unify Error.None region freshCopy t
173solveScheme :: TypeScheme -> StateT TS.SolverState IO (Map.Map String Variable)
174solveScheme scheme =
175 case scheme of
176 Scheme [] [] constraint header ->
177 do actuallySolve constraint
178 Traversable.traverse TS.flatten header
180 Scheme rigidQuantifiers flexibleQuantifiers constraint header ->
181 do let quantifiers = rigidQuantifiers ++ flexibleQuantifiers
182 oldPool <- TS.getPool
184 -- fill in a new pool when working on this scheme's constraints
185 freshPool <- TS.nextRankPool
186 TS.switchToPool freshPool
187 mapM TS.introduce quantifiers
188 header' <- Traversable.traverse TS.flatten header
189 actuallySolve constraint
191 allDistinct rigidQuantifiers
192 youngPool <- TS.getPool
193 TS.switchToPool oldPool
194 generalize youngPool
195 mapM isGeneric rigidQuantifiers
196 return header'
199-- ADDITIONAL CHECKS
201-- Checks that all of the given variables belong to distinct equivalence classes.
202-- Also checks that their structure is Nothing, so they represent a variable, not
203-- a more complex term.
204allDistinct :: [Variable] -> StateT TS.SolverState IO ()
205allDistinct vars =
206 do seen <- TS.uniqueMark
207 forM_ vars $ \var ->
208 do desc <- liftIO $ UF.descriptor var
209 case structure desc of
210 Just _ ->
211 crash "Cannot generalize something that is not a type variable."
213 Nothing ->
214 if mark desc == seen
215 then crash "Duplicate variable during generalization."
216 else liftIO (UF.setDescriptor var (desc { mark = seen }))
219-- Check that a variable has rank == noRank, meaning that it can be generalized.
220isGeneric :: Variable -> StateT TS.SolverState IO ()
221isGeneric var =
222 do desc <- liftIO $ UF.descriptor var
223 if rank desc == noRank
224 then return ()
225 else crash "Unable to generalize a type variable. It is not unranked."
228crash :: String -> a
229crash msg =
230 error $
231 "It looks like something went wrong with the type inference algorithm.\n"
232 ++ msg ++ "\n"
233 ++ "Please create a minimal example that triggers this problem and report it to\n"
234 ++ "<https://github.com/elm-lang/elm-compiler/issues>"
237occurs :: (String, Variable) -> StateT TS.SolverState IO ()
238occurs (_name, variable) =
239 do vars <- liftIO $ infiniteVars [] variable
240 case vars of
241 [] ->
242 return ()
244 var : _ ->
245 do desc <- liftIO $ UF.descriptor var
246 let region = error "TODO:occurs"
247 case structure desc of
248 Nothing ->
249 TS.addError region (Error.InfiniteType undefined (error "TODO:occurs"))
251 Just _ ->
252 TS.addError region (Error.InfiniteType undefined (error "TODO:occurs"))
253 where
254 infiniteVars :: [Variable] -> Variable -> IO [Variable]
255 infiniteVars seen var =
256 let go = infiniteVars (var:seen)
257 in
258 if var `elem` seen
259 then return [var]
260 else do
261 desc <- UF.descriptor var
262 case structure desc of
263 Nothing -> return []
264 Just struct ->
265 case struct of
266 App1 a b ->
267 (++) <$> go a <*> go b
269 Fun1 a b ->
270 (++) <$> go a <*> go b
272 Var1 a ->
273 go a
275 EmptyRecord1 ->
276 return []
278 Record1 fields ext ->
279 concat <$> mapM go (ext : concat (Map.elems fields))