| ... |
... |
@@ -99,13 +99,13 @@ import qualified GHC.LanguageExtensions as LangExt |
|
99
|
99
|
|
|
100
|
100
|
import GHC.Builtin.Types
|
|
101
|
101
|
import GHC.Types.Name
|
|
102
|
|
-import GHC.Types.Id( idType, isDataConId )
|
|
|
102
|
+import GHC.Types.Id( idType )
|
|
103
|
103
|
import GHC.Types.Var as Var
|
|
104
|
104
|
import GHC.Types.Var.Set
|
|
105
|
105
|
import GHC.Types.Var.Env
|
|
106
|
106
|
import GHC.Types.Basic
|
|
107
|
107
|
import GHC.Types.Unique.Set (nonDetEltsUniqSet)
|
|
108
|
|
-import GHC.Types.SrcLoc (unLoc, GenLocated (..))
|
|
|
108
|
+import GHC.Types.SrcLoc ( GenLocated (..) )
|
|
109
|
109
|
|
|
110
|
110
|
import GHC.Utils.Misc
|
|
111
|
111
|
import GHC.Utils.Outputable as Outputable
|
| ... |
... |
@@ -1305,7 +1305,7 @@ Usually this field is `IIF_DeepRho` meaning "return a (possibly deep) rho-type". |
|
1305
|
1305
|
Why is this the common case? See #17173 for discussion. Here are some examples
|
|
1306
|
1306
|
of why:
|
|
1307
|
1307
|
|
|
1308
|
|
-1. Consider
|
|
|
1308
|
+(IIR1) Consider
|
|
1309
|
1309
|
f x = (*)
|
|
1310
|
1310
|
We want to instantiate the type of (*) before returning, else we
|
|
1311
|
1311
|
will infer the type
|
| ... |
... |
@@ -1317,21 +1317,46 @@ of why: |
|
1317
|
1317
|
instantiating. This could perhaps be worked around, but it may be
|
|
1318
|
1318
|
hard to know even when instantiation should happen.
|
|
1319
|
1319
|
|
|
1320
|
|
-2. Another reason. Consider
|
|
|
1320
|
+(IIR2) Another reason. Consider
|
|
1321
|
1321
|
f :: (?x :: Int) => a -> a
|
|
1322
|
1322
|
g y = let ?x = 3::Int in f
|
|
1323
|
1323
|
Here want to instantiate f's type so that the ?x::Int constraint
|
|
1324
|
1324
|
gets discharged by the enclosing implicit-parameter binding.
|
|
1325
|
1325
|
|
|
1326
|
|
-3. Suppose one defines plus = (+). If we instantiate lazily, we will
|
|
|
1326
|
+(IIR3) Suppose one defines plus = (+). If we instantiate lazily, we will
|
|
1327
|
1327
|
infer plus :: forall a. Num a => a -> a -> a. However, the monomorphism
|
|
1328
|
1328
|
restriction compels us to infer
|
|
1329
|
1329
|
plus :: Integer -> Integer -> Integer
|
|
1330
|
1330
|
(or similar monotype). Indeed, the only way to know whether to apply
|
|
1331
|
1331
|
the monomorphism restriction at all is to instantiate
|
|
1332
|
1332
|
|
|
1333
|
|
-HOWEVER, not always! Here are places where we want `IIF_Sigma` meaning
|
|
1334
|
|
-"return a sigma-type":
|
|
|
1333
|
+(IIR4) When -XDeepSubsumption is on, we /deeply/ instantiate. Why isn't
|
|
|
1334
|
+ top-instantiation enough? Answer: to accept the following program (T26225b) with
|
|
|
1335
|
+ -XDeepSubsumption, we need to deeply instantiate when inferring in checkResultTy:
|
|
|
1336
|
+
|
|
|
1337
|
+ f :: Int -> (forall a. a->a)
|
|
|
1338
|
+ g :: Int -> Bool -> Bool
|
|
|
1339
|
+
|
|
|
1340
|
+ test b = case b of
|
|
|
1341
|
+ True -> f
|
|
|
1342
|
+ False -> g
|
|
|
1343
|
+
|
|
|
1344
|
+ If we don't deeply instantiate in the branches of the case expression, we will
|
|
|
1345
|
+ try to unify the type of `f` with that of `g`, which fails. If we instead
|
|
|
1346
|
+ deeply instantiate `f`, we will fill the `InferResult` with `Int -> alpha -> alpha`
|
|
|
1347
|
+ which then successfully unifies with the type of `g` when we come to fill the
|
|
|
1348
|
+ `InferResult` hole a second time for the second case branch.
|
|
|
1349
|
+
|
|
|
1350
|
+(IIR5) When inferring, even /without/ -XDeepSubsumption, we must deeply instantiate
|
|
|
1351
|
+ the types of data constructors. E.g
|
|
|
1352
|
+ data T = MkT Int int
|
|
|
1353
|
+ f = MkT 3
|
|
|
1354
|
+ We must infer MkT 3 :: Int ->{mu} T (fresh mu)
|
|
|
1355
|
+ and not MkT 3 :: Int ->{one} T
|
|
|
1356
|
+ See Note [Typechecking data constructors] in GHC.Tc.Gen.Head
|
|
|
1357
|
+ Hence the use of `getDeepSubsumptionFlag_DataConHead` in `checkResultTy`.
|
|
|
1358
|
+
|
|
|
1359
|
+HOWEVER, `ir_inst` is not always `IIF_DeepRho`! Here are places when it isn't:
|
|
1335
|
1360
|
|
|
1336
|
1361
|
* IIF_Sigma: In GHC.Tc.Module.tcRnExpr, which implements GHCi's :type
|
|
1337
|
1362
|
command, we want to return a completely uninstantiated type.
|
| ... |
... |
@@ -1347,23 +1372,6 @@ HOWEVER, not always! Here are places where we want `IIF_Sigma` meaning |
|
1347
|
1372
|
but /not/ deeply instantiate (#26331). See Note [View patterns and polymorphism]
|
|
1348
|
1373
|
in GHC.Tc.Gen.Pat. This the only place we use IIF_ShallowRho.
|
|
1349
|
1374
|
|
|
1350
|
|
-Why do we want to deeply instantiate, ever? Why isn't top-instantiation enough?
|
|
1351
|
|
-Answer: to accept the following program (T26225b) with -XDeepSubsumption, we
|
|
1352
|
|
-need to deeply instantiate when inferring in checkResultTy:
|
|
1353
|
|
-
|
|
1354
|
|
- f :: Int -> (forall a. a->a)
|
|
1355
|
|
- g :: Int -> Bool -> Bool
|
|
1356
|
|
-
|
|
1357
|
|
- test b =
|
|
1358
|
|
- case b of
|
|
1359
|
|
- True -> f
|
|
1360
|
|
- False -> g
|
|
1361
|
|
-
|
|
1362
|
|
-If we don't deeply instantiate in the branches of the case expression, we will
|
|
1363
|
|
-try to unify the type of 'f' with that of 'g', which fails. If we instead
|
|
1364
|
|
-deeply instantiate 'f', we will fill the 'InferResult' with 'Int -> alpha -> alpha'
|
|
1365
|
|
-which then successfully unifies with the type of 'g' when we come to fill the
|
|
1366
|
|
-'InferResult' hole a second time for the second case branch.
|
|
1367
|
1375
|
-}
|
|
1368
|
1376
|
|
|
1369
|
1377
|
{-
|