git.iko.soy/elk
on b02b4aa 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
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{-| Every variable has rank less than or equal to the maxRank of the pool.
26This sorts variables into the young and old pools accordingly.
27-}
28generalize :: TS.Pool -> TS.Solver ()
29generalize pool@(TS.Pool youngRank _) =
30 {-# SCC elm_compiler_type_generalize #-}
31 do youngMark <- TS.uniqueMark
33 rankTable <- liftIO $ poolToRankTable youngMark pool
35 -- get the ranks right for each entry.
36 -- start at low ranks so that we only have to pass
37 -- over the information once.
38 visitedMark <- TS.uniqueMark
39 let adjust poolRank vars =
40 F.traverse_ (adjustRank youngMark visitedMark poolRank) vars
41 liftIO $ Vector.imapM_ adjust rankTable
43 -- For variables that have rank lowerer than youngRank, register them in
44 -- the old pool if they are not redundant.
45 Vector.forM_ (Vector.unsafeInit rankTable) $ \vars ->
46 forM_ vars $ \var ->
47 do isRedundant <- liftIO $ UF.redundant var
48 if isRedundant then return var else TS.register var
50 -- For variables with rank youngRank
51 -- If rank < youngRank: register in oldPool
52 -- otherwise generalize
53 forM_ (Vector.unsafeLast rankTable) $ \var ->
54 {-# SCC elm_compiler_type_register #-}
55 do isRedundant <- liftIO $ UF.redundant var
56 if isRedundant
57 then return ()
58 else do
59 (Descriptor content rank mark copy) <- liftIO $ UF.descriptor var
60 if rank < youngRank
61 then
62 TS.register var >> return ()
63 else
64 liftIO $ UF.setDescriptor var $ Descriptor (rigidify content) noRank mark copy
67poolToRankTable :: Int -> TS.Pool -> IO (Vector.Vector [Variable])
68poolToRankTable youngMark (TS.Pool youngRank youngInhabitants) =
69 do mutableTable <- MVector.replicate (youngRank + 1) []
71 -- Sort the youngPool variables by rank.
72 forM_ youngInhabitants $ \var ->
73 do (Descriptor content rank _ copy) <- UF.descriptor var
74 UF.setDescriptor var (Descriptor content rank youngMark copy)
75 MVector.modify mutableTable (var:) rank
77 Vector.unsafeFreeze mutableTable
80rigidify :: Content -> Content
81rigidify content =
82 case content of
83 Var Flex maybeSuper maybeName ->
84 Var Rigid maybeSuper maybeName
86 _ ->
87 content
91-- ADJUST RANK
93--
94-- Adjust variable ranks such that ranks never increase as you move deeper.
95-- This way the outermost rank is representative of the entire structure.
96--
97adjustRank :: Int -> Int -> Int -> Variable -> IO Int
98adjustRank youngMark visitedMark groupRank var =
99 {-# SCC elm_compiler_type_adjust #-}
100 do (Descriptor content rank mark copy) <- UF.descriptor var
101 if mark == youngMark then
102 do -- Set the variable as marked first because it may be cyclic.
103 UF.setDescriptor var $ Descriptor content rank visitedMark copy
104 maxRank <- adjustRankContent youngMark visitedMark groupRank content
105 UF.setDescriptor var $ Descriptor content maxRank visitedMark copy
106 return maxRank
108 else if mark == visitedMark then
109 return rank
111 else
112 do let minRank = min groupRank rank
113 -- TODO how can minRank ever be groupRank?
114 UF.setDescriptor var $ Descriptor content minRank visitedMark copy
115 return minRank
118adjustRankContent :: Int -> Int -> Int -> Content -> IO Int
119adjustRankContent youngMark visitedMark groupRank content =
120 let
121 go = adjustRank youngMark visitedMark groupRank
122 in
123 case content of
124 Error _ ->
125 return groupRank
127 Var _ _ _ ->
128 return groupRank
130 Alias _ args _ ->
131 -- THEORY: anything in the realVar would be outermostRank
132 foldM (\rank (_, argVar) -> max rank <$> go argVar) outermostRank args
134 Structure flatType ->
135 case flatType of
136 App1 _ args ->
137 foldM (\rank arg -> max rank <$> go arg) outermostRank args
139 Fun1 arg result ->
140 max <$> go arg <*> go result
142 EmptyRecord1 ->
143 -- THEORY: an empty record never needs to get generalized
144 return outermostRank
146 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.copy 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 (Descriptor _ rank _ _) <- liftIO $ UF.descriptor var
252 if rank == 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 (Descriptor _ rank mark copy) <- liftIO $ UF.descriptor variable
281 liftIO $ UF.setDescriptor variable (Descriptor (Error "∞") rank mark copy)
282 TS.addError region (Error.InfiniteType (Right name) overallType)