git.iko.soy/elk
on 445ea07 help sign in
elk/src/Type/Solve.hs
283 lines 9.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.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.Occurs as Occurs
15import qualified Type.State as TS
16import Type.Type as Type
17import Type.Unify
18import qualified Type.UnionFind as UF
22{-| Every variable has rank less than or equal to the maxRank of the pool.
23This sorts variables into the young and old pools accordingly.
24-}
25generalize :: TS.Pool -> TS.Solver ()
26generalize (TS.Pool youngRank youngInhabitants) =
27 {-# SCC elm_compiler_type_generalize #-}
28 do youngMark <- TS.uniqueMark
29 let insert dict var =
30 {-# SCC elm_compiler_type_insert #-}
31 do descriptor <- UF.descriptor var
32 UF.modifyDescriptor var (\desc -> desc { _mark = youngMark })
33 return $ Map.insertWith (++) (_rank descriptor) [var] dict
35 -- Sort the youngPool variables by rank.
36 rankDict <- liftIO $ foldM insert Map.empty youngInhabitants
38 -- get the ranks right for each entry.
39 -- start at low ranks so that we only have to pass
40 -- over the information once.
41 visitedMark <- TS.uniqueMark
42 liftIO $ forM_ (Map.toList rankDict) $ \(poolRank, vars) ->
43 forM_ vars (adjustRank youngMark visitedMark poolRank)
45 -- For variables that have rank lowerer than youngRank, register them in
46 -- the old pool if they are not redundant.
47 let registerIfNotRedundant var =
48 do isRedundant <- liftIO $ UF.redundant var
49 if isRedundant then return var else TS.register var
51 let rankDict' = Map.delete youngRank rankDict
52 F.traverse_ (F.traverse_ registerIfNotRedundant) rankDict'
54 -- For variables with rank youngRank
55 -- If rank < youngRank: register in oldPool
56 -- otherwise generalize
57 let registerIfLowerRank var =
58 {-# SCC elm_compiler_type_register #-}
59 do isRedundant <- liftIO $ UF.redundant var
60 case isRedundant of
61 True -> return ()
62 False -> do
63 desc <- liftIO $ UF.descriptor var
64 case _rank desc < youngRank of
65 True ->
66 TS.register var >> return ()
67 False ->
68 liftIO $ UF.setDescriptor var $ desc
69 { _rank = noRank
70 , _content = rigidify (_content desc)
71 }
73 mapM_ registerIfLowerRank (Map.findWithDefault [] youngRank rankDict)
76rigidify :: Content -> Content
77rigidify content =
78 case content of
79 Var Flex maybeSuper maybeName ->
80 Var Rigid maybeSuper maybeName
82 _ ->
83 content
86-- adjust the ranks of variables such that ranks never increase as you
87-- move deeper into a variable.
88adjustRank :: Int -> Int -> Int -> Variable -> IO Int
89adjustRank youngMark visitedMark groupRank var =
90 {-# SCC elm_compiler_type_adjust #-}
91 do descriptor <- UF.descriptor var
92 adjustRankHelp youngMark visitedMark groupRank var descriptor
95adjustRankHelp :: Int -> Int -> Int -> Variable -> Descriptor -> IO Int
96adjustRankHelp youngMark visitedMark groupRank var descriptor@(Descriptor content rank mark _) =
97 if mark == youngMark then
99 do -- Set the variable as marked first because it may be cyclic.
100 UF.modifyDescriptor var $ \desc -> desc { _mark = visitedMark }
101 maxRank <- adjustRankContent youngMark visitedMark groupRank content
102 UF.modifyDescriptor var $ \desc -> desc { _rank = maxRank }
103 return maxRank
105 else if mark /= visitedMark then
107 do let minRank = min groupRank rank
108 UF.setDescriptor var (descriptor { _mark = visitedMark, _rank = minRank })
109 return minRank
111 else
113 return rank
116adjustRankContent :: Int -> Int -> Int -> Content -> IO Int
117adjustRankContent youngMark visitedMark groupRank content =
118 let
119 go = adjustRank youngMark visitedMark groupRank
120 in
121 case content of
122 Error _ ->
123 return groupRank
125 Var _ _ _ ->
126 return groupRank
128 Alias _ args realVar ->
129 -- TODO do you have to crawl the args?
130 do realRank <- go realVar
131 foldM (\rank (_, argVar) -> max rank <$> go argVar) realRank args
133 Structure (App1 _ []) ->
134 return groupRank
136 Structure (App1 _ (first:rest)) ->
137 do firstRank <- go first
138 foldM (\rank arg -> max rank <$> go arg) firstRank rest
140 Structure (Fun1 arg result) ->
141 max <$> go arg <*> go result
143 Structure EmptyRecord1 ->
144 return outermostRank
146 Structure (Record1 fields extension) ->
147 do extRank <- go extension
148 foldM (\rank field -> max rank <$> go field) extRank fields
152-- SOLVER
155solve :: Constraint -> ExceptT [A.Located Error.Error] IO TS.State
156solve constraint =
157 {-# SCC elm_compiler_type_solve #-}
158 do state <- liftIO (TS.run (actuallySolve constraint))
159 case TS.sError state of
160 [] ->
161 return state
162 errors ->
163 throwError errors
166actuallySolve :: Constraint -> TS.Solver ()
167actuallySolve constraint =
168 case constraint of
169 CTrue ->
170 return ()
172 CSaveEnv ->
173 TS.saveLocalEnv
175 CEqual hint region term1 term2 ->
176 do t1 <- TS.flatten term1
177 t2 <- TS.flatten term2
178 unify hint region t1 t2
180 CAnd cs ->
181 mapM_ actuallySolve cs
183 CLet [Scheme [] fqs constraint' _] CTrue ->
184 do oldEnv <- TS.getEnv
185 mapM_ TS.introduce fqs
186 actuallySolve constraint'
187 TS.modifyEnv (\_ -> oldEnv)
189 CLet schemes constraint' ->
190 do oldEnv <- TS.getEnv
191 headers <- Map.unions <$> mapM solveScheme schemes
192 TS.modifyEnv $ \env -> Map.union headers env
193 actuallySolve constraint'
194 mapM_ occurs $ Map.toList headers
195 TS.modifyEnv (\_ -> oldEnv)
197 CInstance region name term ->
198 do env <- TS.getEnv
199 freshCopy <-
200 case Map.lookup name env of
201 Just (A.A _ tipe) ->
202 TS.makeInstance tipe
204 Nothing ->
205 if ModuleName.isKernel name then
206 liftIO (mkVar Nothing)
208 else
209 error ("Could not find `" ++ Text.unpack name ++ "` when solving type constraints.")
211 t <- TS.flatten term
212 unify (Error.Instance name) region freshCopy t
215solveScheme :: Scheme -> TS.Solver TS.Env
216solveScheme scheme =
217 let
218 flatten (A.A region term) =
219 A.A region <$> TS.flatten term
220 in
221 case scheme of
222 Scheme [] [] constraint header ->
223 do actuallySolve constraint
224 traverse flatten header
226 Scheme rigidQuantifiers flexibleQuantifiers constraint header ->
227 do let quantifiers = rigidQuantifiers ++ flexibleQuantifiers
228 oldPool <- TS.getPool
230 -- fill in a new pool when working on this scheme's constraints
231 freshPool <- TS.nextRankPool
232 TS.switchToPool freshPool
233 mapM_ TS.introduce quantifiers
234 header' <- traverse flatten header
235 actuallySolve constraint
237 youngPool <- TS.getPool
238 TS.switchToPool oldPool
239 generalize youngPool
240 mapM_ isGeneric rigidQuantifiers
241 return header'
245-- ADDITIONAL CHECKS
248-- Check that a variable has rank == noRank, meaning that it can be generalized.
249isGeneric :: Variable -> TS.Solver ()
250isGeneric var =
251 do desc <- liftIO $ UF.descriptor var
252 if _rank desc == noRank
253 then return ()
254 else crash "Unable to generalize a type variable. It is not unranked."
257crash :: String -> a
258crash msg =
259 error $
260 "It looks like something went wrong with the type inference algorithm.\n\n"
261 ++ msg ++ "\n\n"
262 ++ "Please create a minimal example that triggers this problem and report it to\n"
263 ++ "<https://github.com/elm-lang/elm-compiler/issues>"
267-- OCCURS CHECK
270occurs :: (Text.Text, A.Located Variable) -> TS.Solver ()
271occurs (name, A.A region variable) =
272 {-# SCC elm_compiler_type_occurs #-}
273 do hasOccurred <- liftIO $ Occurs.occurs variable
274 case hasOccurred of
275 False ->
276 return ()
278 True ->
279 do overallType <- liftIO $ Type.toSrcType variable
280 infiniteDescriptor <- liftIO $ UF.descriptor variable
281 liftIO $ UF.setDescriptor variable (infiniteDescriptor { _content = Error "∞" })
282 TS.addError region (Error.InfiniteType (Right name) overallType)