git.iko.soy/elk
on 09076eb help sign in
elk/src/Type/Solve.hs
285 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
10import qualified Data.Vector as Vector
11import qualified Data.Vector.Mutable as MVector
13import qualified AST.Module.Name as ModuleName
14import qualified Reporting.Annotation as A
15import qualified Reporting.Error.Type as Error
16import qualified Type.Occurs as Occurs
17import qualified Type.State as TS
18import Type.Constraint (Constraint(..), Scheme(..))
19import Type.Type as Type
20import Type.Unify
21import qualified Type.UnionFind as UF
25-- SOLVER
28solve :: Constraint -> ExceptT [A.Located Error.Error] IO TS.State
29solve constraint =
30 {-# SCC elm_compiler_type_solve #-}
31 do state <- liftIO (TS.run (actuallySolve constraint))
32 case TS.sError state of
33 [] ->
34 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 mapM_ 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
88solveScheme :: Scheme -> TS.Solver TS.Env
89solveScheme scheme =
90 let
91 flatten (A.A region term) =
92 A.A region <$> TS.flatten term
93 in
94 case scheme of
95 Scheme [] [] constraint header ->
96 do actuallySolve constraint
97 traverse flatten header
99 Scheme rigidQuantifiers flexibleQuantifiers constraint header ->
100 do let quantifiers = rigidQuantifiers ++ flexibleQuantifiers
101 oldPool <- TS.getPool
103 -- fill in a new pool when working on this scheme's constraints
104 freshPool <- TS.nextRankPool
105 TS.switchToPool freshPool
106 mapM_ TS.introduce quantifiers
107 header' <- traverse flatten header
108 actuallySolve constraint
110 youngPool <- TS.getPool
111 TS.switchToPool oldPool
112 generalize youngPool
113 mapM_ isGeneric rigidQuantifiers
114 return header'
118-- ADDITIONAL CHECKS
121-- Check that a variable has rank == noRank, meaning that it can be generalized.
122isGeneric :: Variable -> TS.Solver ()
123isGeneric var =
124 do (Descriptor _ rank _ _) <- liftIO $ UF.descriptor var
125 if rank == noRank
126 then return ()
127 else crash "Unable to generalize a type variable. It is not unranked."
130crash :: String -> a
131crash msg =
132 error $
133 "It looks like something went wrong with the type inference algorithm.\n\n"
134 ++ msg ++ "\n\n"
135 ++ "Please create a minimal example that triggers this problem and report it to\n"
136 ++ "<https://github.com/elm-lang/elm-compiler/issues>"
140-- OCCURS CHECK
143occurs :: (Text.Text, A.Located Variable) -> TS.Solver ()
144occurs (name, A.A region variable) =
145 {-# SCC elm_compiler_type_occurs #-}
146 do hasOccurred <- liftIO $ Occurs.occurs variable
147 case hasOccurred of
148 False ->
149 return ()
151 True ->
152 do overallType <- liftIO $ Type.toSrcType variable
153 (Descriptor _ rank mark copy) <- liftIO $ UF.descriptor variable
154 liftIO $ UF.setDescriptor variable (Descriptor (Error "∞") rank mark copy)
155 TS.addError region (Error.InfiniteType (Right name) overallType)
159-- GENERALIZE
162{-| Every variable has rank less than or equal to the maxRank of the pool.
163This sorts variables into the young and old pools accordingly.
164-}
165generalize :: TS.Pool -> TS.Solver ()
166generalize pool@(TS.Pool youngRank _) =
167 {-# SCC elm_compiler_type_generalize #-}
168 do youngMark <- TS.uniqueMark
170 rankTable <- liftIO $ poolToRankTable youngMark pool
172 -- get the ranks right for each entry.
173 -- start at low ranks so that we only have to pass
174 -- over the information once.
175 visitedMark <- TS.uniqueMark
176 let adjust poolRank vars =
177 F.traverse_ (adjustRank youngMark visitedMark poolRank) vars
178 liftIO $ Vector.imapM_ adjust rankTable
180 -- For variables that have rank lowerer than youngRank, register them in
181 -- the old pool if they are not redundant.
182 Vector.forM_ (Vector.unsafeInit rankTable) $ \vars ->
183 forM_ vars $ \var ->
184 do isRedundant <- liftIO $ UF.redundant var
185 if isRedundant then return var else TS.register var
187 -- For variables with rank youngRank
188 -- If rank < youngRank: register in oldPool
189 -- otherwise generalize
190 forM_ (Vector.unsafeLast rankTable) $ \var ->
191 {-# SCC elm_compiler_type_register #-}
192 do isRedundant <- liftIO $ UF.redundant var
193 if isRedundant
194 then return ()
195 else do
196 (Descriptor content rank mark copy) <- liftIO $ UF.descriptor var
197 if rank < youngRank
198 then
199 TS.register var >> return ()
200 else
201 liftIO $ UF.setDescriptor var $ Descriptor (rigidify content) noRank mark copy
204poolToRankTable :: Mark -> TS.Pool -> IO (Vector.Vector [Variable])
205poolToRankTable youngMark (TS.Pool youngRank youngInhabitants) =
206 do mutableTable <- MVector.replicate (youngRank + 1) []
208 -- Sort the youngPool variables by rank.
209 forM_ youngInhabitants $ \var ->
210 do (Descriptor content rank _ copy) <- UF.descriptor var
211 UF.setDescriptor var (Descriptor content rank youngMark copy)
212 MVector.modify mutableTable (var:) rank
214 Vector.unsafeFreeze mutableTable
217rigidify :: Content -> Content
218rigidify content =
219 case content of
220 Var Flex maybeSuper maybeName ->
221 Var Rigid maybeSuper maybeName
223 _ ->
224 content
228-- ADJUST RANK
230--
231-- Adjust variable ranks such that ranks never increase as you move deeper.
232-- This way the outermost rank is representative of the entire structure.
233--
234adjustRank :: Mark -> Mark -> Int -> Variable -> IO Int
235adjustRank youngMark visitedMark groupRank var =
236 {-# SCC elm_compiler_type_adjust #-}
237 do (Descriptor content rank mark copy) <- UF.descriptor var
238 if mark == youngMark then
239 do -- Set the variable as marked first because it may be cyclic.
240 UF.setDescriptor var $ Descriptor content rank visitedMark copy
241 maxRank <- adjustRankContent youngMark visitedMark groupRank content
242 UF.setDescriptor var $ Descriptor content maxRank visitedMark copy
243 return maxRank
245 else if mark == visitedMark then
246 return rank
248 else
249 do let minRank = min groupRank rank
250 -- TODO how can minRank ever be groupRank?
251 UF.setDescriptor var $ Descriptor content minRank visitedMark copy
252 return minRank
255adjustRankContent :: Mark -> Mark -> Int -> Content -> IO Int
256adjustRankContent youngMark visitedMark groupRank content =
257 let
258 go = adjustRank youngMark visitedMark groupRank
259 in
260 case content of
261 Error _ ->
262 return groupRank
264 Var _ _ _ ->
265 return groupRank
267 Alias _ args _ ->
268 -- THEORY: anything in the realVar would be outermostRank
269 foldM (\rank (_, argVar) -> max rank <$> go argVar) outermostRank args
271 Structure flatType ->
272 case flatType of
273 App1 _ args ->
274 foldM (\rank arg -> max rank <$> go arg) outermostRank args
276 Fun1 arg result ->
277 max <$> go arg <*> go result
279 EmptyRecord1 ->
280 -- THEORY: an empty record never needs to get generalized
281 return outermostRank
283 Record1 fields extension ->
284 do extRank <- go extension
285 foldM (\rank field -> max rank <$> go field) extRank fields