Commit 0ae72512 authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

Yet more work on TcSimplify.simplifyInfer

The proximate cause for this patch is Trac #13482, which pointed out
further subtle interactions between
   - Inferring the most general type of a function
   - A partial type signature for that function

That led me into /further/ changes to the shiny new stuff in
TcSimplify.simplifyInfer, decideQuantification, decideMonoTyVars,
and related functions.

Happily, I was able to make some of it quite a bit simpler,
notably the bit about promoting free tyvars.  I'm happy with
the result.

Moreover I fixed Trac #13524 at the same time.  Happy days.
parent 037c2495
......@@ -921,7 +921,8 @@ chooseInferredQuantifiers inferred_theta tau_tvs qtvs
; let free_tvs = closeOverKinds (tyCoVarsOfTypes annotated_theta
`unionVarSet` tau_tvs)
; traceTc "ciq" (vcat [ ppr sig, ppr annotated_theta, ppr free_tvs])
; return (mk_binders free_tvs, annotated_theta) }
; psig_qtvs <- mk_psig_qtvs annotated_tvs
; return (mk_final_qtvs psig_qtvs free_tvs, annotated_theta) }
| Just wc_var <- wcx
= do { annotated_theta <- zonkTcTypes annotated_theta
......@@ -930,7 +931,11 @@ chooseInferredQuantifiers inferred_theta tau_tvs qtvs
-- Omitting this caused #12844
seed_tvs = tyCoVarsOfTypes annotated_theta -- These are put there
`unionVarSet` tau_tvs -- by the user
my_theta = pickCapturedPreds free_tvs inferred_theta
; psig_qtvs <- mk_psig_qtvs annotated_tvs
; let my_qtvs = mk_final_qtvs psig_qtvs free_tvs
keep_me = psig_qtvs `unionVarSet` free_tvs
my_theta = pickCapturedPreds keep_me inferred_theta
-- Report the inferred constraints for an extra-constraints wildcard/hole as
-- an error message, unless the PartialTypeSignatures flag is enabled. In this
......@@ -946,25 +951,30 @@ chooseInferredQuantifiers inferred_theta tau_tvs qtvs
, ppr annotated_theta, ppr inferred_theta
, ppr inferred_diff ]
; return (mk_binders free_tvs, my_theta) }
; return (my_qtvs, my_theta) }
| otherwise -- A complete type signature is dealt with in mkInferredPolyId
= pprPanic "chooseInferredQuantifiers" (ppr sig)
where
spec_tv_set = mkVarSet $ map snd annotated_tvs
mk_binders free_tvs
mk_final_qtvs psig_qtvs free_tvs
= [ mkTyVarBinder vis tv
| tv <- qtvs
, tv `elemVarSet` free_tvs
, let vis | tv `elemVarSet` spec_tv_set = Specified
| otherwise = Inferred ]
-- Pulling from qtvs maintains original order
| tv <- qtvs -- Pulling from qtvs maintains original order
, tv `elemVarSet` keep_me
, let vis | tv `elemVarSet` psig_qtvs = Specified
| otherwise = Inferred ]
where
keep_me = free_tvs `unionVarSet` psig_qtvs
mk_ctuple [pred] = return pred
mk_ctuple preds = do { tc <- tcLookupTyCon (cTupleTyConName (length preds))
; return (mkTyConApp tc preds) }
mk_psig_qtvs :: [(Name,TcTyVar)] -> TcM TcTyVarSet
mk_psig_qtvs annotated_tvs
= do { psig_qtvs <- mapM (zonkTcTyVarToTyVar . snd) annotated_tvs
; return (mkVarSet psig_qtvs) }
mk_impedance_match_msg :: MonoBindInfo
-> TcType -> TcType
-> TidyEnv -> TcM (TidyEnv, SDoc)
......
......@@ -1404,7 +1404,7 @@ data TcIdSigInst
= TISI { sig_inst_sig :: TcIdSigInfo
, sig_inst_skols :: [(Name, TcTyVar)]
-- Instantiated type and kind variables SKOLEMS
-- Instantiated type and kind variables, SigTvs
-- The Name is the Name that the renamer chose;
-- but the TcTyVar may come from instantiating
-- the type and hence have a different unique.
......@@ -1454,7 +1454,7 @@ Moreover the kind of a wildcard in sig_inst_wcs may mention
the universally-quantified tyvars sig_inst_skols
e.g. f :: t a -> t _
Here we get
sig_inst_skole = [k:*, (t::k ->*), (a::k)]
sig_inst_skols = [k:*, (t::k ->*), (a::k)]
sig_inst_tau = t a -> t _22
sig_inst_wcs = [ _22::k ]
-}
......
This diff is collapsed.
TYPE SIGNATURES
foo :: forall a b. (a, b) -> (a, b)
foo :: forall b a. (a, b) -> (a, b)
TYPE CONSTRUCTORS
COERCION AXIOMS
Dependent modules: []
......
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE KindSignatures #-}
module T12382 where
minimal1_noksig :: forall m. ( _ ) => Int -> Bool
minimal1_noksig _ = (mempty :: m) == (mempty :: m)
minimal1 :: forall (m :: *). _ => Bool
minimal1 = (mempty :: m) == (mempty :: m)
minimal2 :: forall m. (Eq m, _) => Bool
minimal2 = (mempty :: m) == (mempty :: m)
minimal3 :: forall m. (Monoid m, _) => Bool
minimal3 = (mempty :: m) == (mempty :: m)
minimal4 :: forall m. (Monoid m, Eq m) => Bool
minimal4 = (mempty :: m) == (mempty :: m)
T13482.hs:8:32: warning: [-Wpartial-type-signatures (in -Wdefault)]
• Found type wildcard ‘_’ standing for ‘(Monoid m, Eq m)’
Where: ‘m’ is a rigid type variable bound by
the inferred type of
minimal1_noksig :: (Monoid m, Eq m) => Int -> Bool
at T13482.hs:9:1-50
• In the type signature:
minimal1_noksig :: forall m. _ => Int -> Bool
T13482.hs:11:30: warning: [-Wpartial-type-signatures (in -Wdefault)]
• Found type wildcard ‘_’ standing for ‘(Monoid m, Eq m)’
Where: ‘m’ is a rigid type variable bound by
the inferred type of minimal1 :: (Monoid m, Eq m) => Bool
at T13482.hs:12:1-41
• In the type signature: minimal1 :: forall (m :: *). _ => Bool
T13482.hs:14:30: warning: [-Wpartial-type-signatures (in -Wdefault)]
• Found type wildcard ‘_’ standing for ‘Monoid m’
Where: ‘m’ is a rigid type variable bound by
the inferred type of minimal2 :: (Eq m, Monoid m) => Bool
at T13482.hs:15:1-41
• In the type signature: minimal2 :: forall m. (Eq m, _) => Bool
T13482.hs:17:34: warning: [-Wpartial-type-signatures (in -Wdefault)]
• Found type wildcard ‘_’ standing for ‘Eq m’
Where: ‘m’ is a rigid type variable bound by
the inferred type of minimal3 :: (Monoid m, Eq m) => Bool
at T13482.hs:18:1-41
• In the type signature:
minimal3 :: forall m. (Monoid m, _) => Bool
......@@ -69,3 +69,4 @@ test('T12156', normal, compile_fail, ['-fdefer-typed-holes'])
test('T12531', normal, compile, ['-fdefer-typed-holes'])
test('T12845', normal, compile, [''])
test('T12844', normal, compile, [''])
test('T13482', normal, compile, [''])
......@@ -551,7 +551,7 @@ test('T13343', normal, compile, [''])
test('T13458', normal, compile, [''])
test('T13490', normal, compile, [''])
test('T13474', normal, compile, [''])
test('T13524', expect_broken(13524), compile, [''])
test('T13524', normal, compile, [''])
test('T13509', normal, compile, [''])
test('T13526', normal, compile, [''])
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment