git.iko.soy/elk
on 087045f help sign in
elk/src/Type/Solve.hs
313 lines 10.0 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.Map.Strict as Map
8import qualified Data.Text as Text
9import qualified Data.Vector as Vector
10import qualified Data.Vector.Mutable as MVector
12import qualified AST.Module.Name as ModuleName
13import qualified Reporting.Annotation as A
14import qualified Reporting.Error.Type as Error
15import qualified Type.Occurs as Occurs
16import qualified Type.State as TS
17import Type.Constraint (Constraint(..), Scheme(..))
18import Type.Type as Type
19import Type.Unify
20import qualified Type.UnionFind as UF
24-- SOLVER
27solve :: Constraint -> ExceptT [A.Located Error.Error] IO TS.State
28solve constraint =
29 {-# SCC elm_compiler_type_solve #-}
30 do state <- liftIO (TS.run (actuallySolve constraint))
31 case TS._errors state of
32 [] ->
33 return state
35 errors ->
36 throwError errors
39actuallySolve :: Constraint -> TS.Solver ()
40actuallySolve constraint =
41 case constraint of
42 CTrue ->
43 return ()
45 CSaveEnv ->
46 TS.saveLocalEnv
48 CEqual hint region term1 term2 ->
49 do t1 <- TS.flatten term1
50 t2 <- TS.flatten term2
51 unify hint region t1 t2
53 CAnd cs ->
54 mapM_ actuallySolve cs
56 CLet [Scheme [] fqs constraint' _] CTrue ->
57 do oldEnv <- TS.getEnv
58 TS.introduce fqs
59 actuallySolve constraint'
60 TS.modifyEnv (\_ -> oldEnv)
62 CLet schemes constraint' ->
63 do oldEnv <- TS.getEnv
64 headers <- Map.unions <$> mapM solveScheme schemes
65 TS.modifyEnv $ \env -> Map.union headers env
66 actuallySolve constraint'
67 mapM_ occurs $ Map.toList headers
68 TS.modifyEnv (\_ -> oldEnv)
70 CInstance region name term ->
71 do env <- TS.getEnv
72 freshCopy <-
73 case Map.lookup name env of
74 Just (A.A _ tipe) ->
75 TS.copy tipe
77 Nothing ->
78 if ModuleName.isKernel name then
79 liftIO mkFlexVar
81 else
82 error ("Could not find `" ++ Text.unpack name ++ "` when solving type constraints.")
84 t <- TS.flatten term
85 unify (Error.Instance name) region freshCopy t
89-- SOLVE SCHEMES
92solveScheme :: Scheme -> TS.Solver TS.Env
93solveScheme scheme =
94 let
95 flatten (A.A region term) =
96 A.A region <$> TS.flatten term
97 in
98 case scheme of
99 Scheme [] [] constraint header ->
100 do actuallySolve constraint
101 traverse flatten header
103 Scheme rigidQuantifiers flexQuantifiers constraint header ->
104 -- work in the next pool for this scheme's constraints
105 solveSchemeHelp rigidQuantifiers flexQuantifiers $
106 do flatHeader <- traverse flatten header
107 actuallySolve constraint
108 return flatHeader
112solveSchemeHelp :: [Variable] -> [Variable] -> TS.Solver a -> TS.Solver a
113solveSchemeHelp rigidQuantifiers flexQuantifiers (TS.Solver stepState) =
114 TS.Solver $ \state@(TS.SS _ _ rank oldPools _ _) ->
115 do
116 -- push pool
117 let nextRank = rank + 1
118 let poolsLength = MVector.length oldPools
120 pools <-
121 if nextRank < poolsLength
122 then return oldPools
123 else MVector.grow oldPools poolsLength
125 -- introduce quantifiers
126 let allQuantifiers = rigidQuantifiers ++ flexQuantifiers
127 forM_ allQuantifiers $ \var ->
128 UF.modifyDescriptor var $ \(Descriptor content _ mark copy) ->
129 Descriptor content nextRank mark copy
130 MVector.write pools nextRank allQuantifiers
132 -- run solver in next pool
133 (value, TS.SS env savedEnv _ _ mark errors) <- stepState (state { TS._rank = nextRank })
135 -- pop pool
136 let youngMark = mark
137 let visitMark = nextMark mark
138 let finalMark = nextMark visitMark
139 generalize youngMark visitMark nextRank pools
140 MVector.write pools nextRank []
142 -- check that things went well
143 mapM_ isGeneric rigidQuantifiers
145 -- return result with pool popped
146 return ( value, TS.SS env savedEnv rank pools finalMark errors )
149-- Check that a variable has rank == noRank, meaning that it can be generalized.
150isGeneric :: Variable -> IO ()
151isGeneric var =
152 do (Descriptor _ rank _ _) <- UF.descriptor var
153 if rank == noRank
154 then return ()
155 else crash "Unable to generalize a type variable. It is not unranked."
158crash :: String -> a
159crash msg =
160 error $
161 "It looks like something went wrong with the type inference algorithm.\n\n"
162 ++ msg ++ "\n\n"
163 ++ "Please create a minimal example that triggers this problem and report it to\n"
164 ++ "<https://github.com/elm-lang/elm-compiler/issues>"
168-- OCCURS CHECK
171occurs :: (Text.Text, A.Located Variable) -> TS.Solver ()
172occurs (name, A.A region variable) =
173 {-# SCC elm_compiler_type_occurs #-}
174 do hasOccurred <- liftIO $ Occurs.occurs variable
175 case hasOccurred of
176 False ->
177 return ()
179 True ->
180 do overallType <- liftIO $ Type.toSrcType variable
181 (Descriptor _ rank mark copy) <- liftIO $ UF.descriptor variable
182 liftIO $ UF.setDescriptor variable (Descriptor (Error "∞") rank mark copy)
183 TS.addError region (Error.InfiniteType (Right name) overallType)
187-- GENERALIZE
190{-| Every variable has rank less than or equal to the maxRank of the pool.
191This sorts variables into the young and old pools accordingly.
192-}
193generalize :: Mark -> Mark -> Int -> TS.Pools -> IO ()
194generalize youngMark visitMark youngRank pools =
195 {-# SCC elm_compiler_type_generalize #-}
196 do
197 youngVars <- MVector.read pools youngRank
198 rankTable <- poolToRankTable youngMark youngRank youngVars
200 -- get the ranks right for each entry.
201 -- start at low ranks so that we only have to pass
202 -- over the information once.
203 Vector.imapM_ (mapM_ . adjustRank youngMark visitMark) rankTable
205 -- For variables that have rank lowerer than youngRank, register them in
206 -- the appropriate old pool if they are not redundant.
207 Vector.forM_ (Vector.unsafeInit rankTable) $ \vars ->
208 forM_ vars $ \var ->
209 do isRedundant <- UF.redundant var
210 if isRedundant
211 then return ()
212 else
213 do (Descriptor _ rank _ _) <- UF.descriptor var
214 MVector.modify pools (var:) rank
216 -- For variables with rank youngRank
217 -- If rank < youngRank: register in oldPool
218 -- otherwise generalize
219 forM_ (Vector.unsafeLast rankTable) $ \var ->
220 do isRedundant <- UF.redundant var
221 if isRedundant
222 then return ()
223 else
224 do (Descriptor content rank mark copy) <- liftIO $ UF.descriptor var
225 if rank < youngRank
226 then
227 MVector.modify pools (var:) rank
228 else
229 UF.setDescriptor var $ Descriptor content noRank mark copy
232poolToRankTable :: Mark -> Int -> [Variable] -> IO (Vector.Vector [Variable])
233poolToRankTable youngMark youngRank youngInhabitants =
234 do mutableTable <- MVector.replicate (youngRank + 1) []
236 -- Sort the youngPool variables into buckets by rank.
237 forM_ youngInhabitants $ \var ->
238 do (Descriptor content rank _ copy) <- UF.descriptor var
239 UF.setDescriptor var (Descriptor content rank youngMark copy)
240 MVector.modify mutableTable (var:) rank
242 Vector.unsafeFreeze mutableTable
246-- ADJUST RANK
248--
249-- Adjust variable ranks such that ranks never increase as you move deeper.
250-- This way the outermost rank is representative of the entire structure.
251--
252adjustRank :: Mark -> Mark -> Int -> Variable -> IO Int
253adjustRank youngMark visitMark groupRank var =
254 {-# SCC elm_compiler_type_adjust #-}
255 do (Descriptor content rank mark copy) <- UF.descriptor var
256 if mark == youngMark then
257 do -- Set the variable as marked first because it may be cyclic.
258 UF.setDescriptor var $ Descriptor content rank visitMark copy
259 maxRank <- adjustRankContent youngMark visitMark groupRank content
260 UF.setDescriptor var $ Descriptor content maxRank visitMark copy
261 return maxRank
263 else if mark == visitMark then
264 return rank
266 else
267 do let minRank = min groupRank rank
268 -- TODO how can minRank ever be groupRank?
269 UF.setDescriptor var $ Descriptor content minRank visitMark copy
270 return minRank
273adjustRankContent :: Mark -> Mark -> Int -> Content -> IO Int
274adjustRankContent youngMark visitMark groupRank content =
275 let
276 go = adjustRank youngMark visitMark groupRank
277 in
278 case content of
279 FlexVar _ ->
280 return groupRank
282 FlexSuper _ _ ->
283 return groupRank
285 RigidVar _ ->
286 return groupRank
288 RigidSuper _ _ ->
289 return groupRank
291 Structure flatType ->
292 case flatType of
293 App1 _ args ->
294 foldM (\rank arg -> max rank <$> go arg) outermostRank args
296 Fun1 arg result ->
297 max <$> go arg <*> go result
299 EmptyRecord1 ->
300 -- THEORY: an empty record never needs to get generalized
301 return outermostRank
303 Record1 fields extension ->
304 do extRank <- go extension
305 foldM (\rank field -> max rank <$> go field) extRank fields
307 Alias _ args _ ->
308 -- THEORY: anything in the realVar would be outermostRank
309 foldM (\rank (_, argVar) -> max rank <$> go argVar) outermostRank args
311 Error _ ->
312 return groupRank