git.iko.soy/elk
on 368cdbc help sign in
elk/src/Type/Solve.hs
279 lines 8.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
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 Atom _ ->
126 return groupRank
128 Var _ _ _ ->
129 return groupRank
131 Alias _ args realVar ->
132 -- TODO do you have to crawl the args?
133 do realRank <- go realVar
134 foldM (\rank (_, argVar) -> max rank <$> go argVar) realRank args
136 Structure (App1 func arg) ->
137 max <$> go func <*> go arg
139 Structure (Fun1 arg result) ->
140 max <$> go arg <*> go result
142 Structure EmptyRecord1 ->
143 return outermostRank
145 Structure (Record1 fields extension) ->
146 do extRank <- go extension
147 foldM (\rank field -> max rank <$> go field) extRank fields
151-- SOLVER
154solve :: Constraint -> ExceptT [A.Located Error.Error] IO TS.State
155solve constraint =
156 {-# SCC elm_compiler_type_solve #-}
157 do state <- liftIO (TS.run (actuallySolve constraint))
158 case TS.sError state of
159 [] ->
160 return state
161 errors ->
162 throwError errors
165actuallySolve :: Constraint -> TS.Solver ()
166actuallySolve constraint =
167 case constraint of
168 CTrue ->
169 return ()
171 CSaveEnv ->
172 TS.saveLocalEnv
174 CEqual hint region term1 term2 ->
175 do t1 <- TS.flatten term1
176 t2 <- TS.flatten term2
177 unify hint region t1 t2
179 CAnd cs ->
180 mapM_ actuallySolve cs
182 CLet [Scheme [] fqs constraint' _] CTrue ->
183 do oldEnv <- TS.getEnv
184 mapM_ TS.introduce fqs
185 actuallySolve constraint'
186 TS.modifyEnv (\_ -> oldEnv)
188 CLet schemes constraint' ->
189 do oldEnv <- TS.getEnv
190 headers <- Map.unions <$> mapM solveScheme schemes
191 TS.modifyEnv $ \env -> Map.union headers env
192 actuallySolve constraint'
193 mapM_ occurs $ Map.toList headers
194 TS.modifyEnv (\_ -> oldEnv)
196 CInstance region name term ->
197 do env <- TS.getEnv
198 freshCopy <-
199 case Map.lookup name env of
200 Just (A.A _ tipe) ->
201 TS.makeInstance tipe
203 Nothing ->
204 if ModuleName.isKernel name then
205 liftIO (mkVar Nothing)
207 else
208 error ("Could not find `" ++ Text.unpack name ++ "` when solving type constraints.")
210 t <- TS.flatten term
211 unify (Error.Instance name) region freshCopy t
214solveScheme :: Scheme -> TS.Solver TS.Env
215solveScheme scheme =
216 let
217 flatten (A.A region term) =
218 A.A region <$> TS.flatten term
219 in
220 case scheme of
221 Scheme [] [] constraint header ->
222 do actuallySolve constraint
223 traverse flatten header
225 Scheme rigidQuantifiers flexibleQuantifiers constraint header ->
226 do let quantifiers = rigidQuantifiers ++ flexibleQuantifiers
227 oldPool <- TS.getPool
229 -- fill in a new pool when working on this scheme's constraints
230 freshPool <- TS.nextRankPool
231 TS.switchToPool freshPool
232 mapM_ TS.introduce quantifiers
233 header' <- traverse flatten header
234 actuallySolve constraint
236 youngPool <- TS.getPool
237 TS.switchToPool oldPool
238 generalize youngPool
239 mapM_ isGeneric rigidQuantifiers
240 return header'
244-- ADDITIONAL CHECKS
247-- Check that a variable has rank == noRank, meaning that it can be generalized.
248isGeneric :: Variable -> TS.Solver ()
249isGeneric var =
250 do desc <- liftIO $ UF.descriptor var
251 if _rank desc == noRank
252 then return ()
253 else crash "Unable to generalize a type variable. It is not unranked."
256crash :: String -> a
257crash msg =
258 error $
259 "It looks like something went wrong with the type inference algorithm.\n\n"
260 ++ msg ++ "\n\n"
261 ++ "Please create a minimal example that triggers this problem and report it to\n"
262 ++ "<https://github.com/elm-lang/elm-compiler/issues>"
266-- OCCURS CHECK
269occurs :: (Text.Text, A.Located Variable) -> TS.Solver ()
270occurs (name, A.A region variable) =
271 {-# SCC elm_compiler_type_occurs #-}
272 do hasOccurred <- liftIO $ Occurs.occurs variable
273 case hasOccurred of
274 False ->
275 return ()
277 True ->
278 do overallType <- liftIO (Type.toSrcType variable)
279 TS.addError region (Error.InfiniteType name overallType)