Commit f5cf9d1a authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

Fix floating of equalities

This rather subtle patch fixes Trac #14584.  The problem was
that we'd allowed a coercion, bound in a nested scope, to escape
into an outer scope.

The main changes are

* TcSimplify.floatEqualities takes more care when floating
  equalities to make sure we don't float one out that mentions
  a locally-bound coercion.
  See Note [What prevents a constraint from floating]

* TcSimplify.emitResidualConstraints (which emits the residual
  constraints in simplifyInfer) now avoids burying the constraints
  for escaping CoVars inside the implication constraint.

* Since I had do to this stuff with CoVars, I moved the
  fancy footwork about not quantifying over CoVars from
  TcMType.quantifyTyVars to its caller
  TcSimplify.decideQuantifiedTyVars.  I think its other
  callers don't need to worry about all this CoVar stuff.

This turned out to be surprisigly tricky, and took me a solid
day to get right.  I think the result is reasonably neat, though,
and well documented with Notes.
parent a492af06
......@@ -950,15 +950,11 @@ quantifyTyVars
quantifyTyVars gbl_tvs dvs@(DV{ dv_kvs = dep_tkvs, dv_tvs = nondep_tkvs })
= do { traceTc "quantifyTyVars" (vcat [ppr dvs, ppr gbl_tvs])
; let all_cvs = filterVarSet isCoVar $ dVarSetToVarSet dep_tkvs
dep_kvs = dVarSetElemsWellScoped $
; let dep_kvs = dVarSetElemsWellScoped $
dep_tkvs `dVarSetMinusVarSet` gbl_tvs
`dVarSetMinusVarSet` closeOverKinds all_cvs
-- dVarSetElemsWellScoped: put the kind variables into
-- well-scoped order.
-- E.g. [k, (a::k)] not the other way roud
-- closeOverKinds all_cvs: do not quantify over coercion
-- variables, or any any tvs that a covar depends on
-- dVarSetElemsWellScoped: put the kind variables into
-- well-scoped order.
-- E.g. [k, (a::k)] not the other way roud
nondep_tvs = dVarSetElems $
(nondep_tkvs `minusDVarSet` dep_tkvs)
......@@ -981,6 +977,7 @@ quantifyTyVars gbl_tvs dvs@(DV{ dv_kvs = dep_tkvs, dv_tvs = nondep_tkvs })
; poly_kinds <- xoptM LangExt.PolyKinds
; dep_kvs' <- mapMaybeM (zonk_quant (not poly_kinds)) dep_kvs
; nondep_tvs' <- mapMaybeM (zonk_quant False) nondep_tvs
; let final_qtvs = dep_kvs' ++ nondep_tvs'
-- Because of the order, any kind variables
-- mentioned in the kinds of the nondep_tvs'
-- now refer to the dep_kvs'
......@@ -992,7 +989,11 @@ quantifyTyVars gbl_tvs dvs@(DV{ dv_kvs = dep_tkvs, dv_tvs = nondep_tkvs })
, text "dep_kvs'" <+> pprTyVars dep_kvs'
, text "nondep_tvs'" <+> pprTyVars nondep_tvs' ])
; return (dep_kvs' ++ nondep_tvs') }
-- We should never quantify over coercion variables; check this
; let co_vars = filter isCoVar final_qtvs
; MASSERT2( null co_vars, ppr co_vars )
; return final_qtvs }
where
-- zonk_quant returns a tyvar if it should be quantified over;
-- otherwise, it returns Nothing. The latter case happens for
......
......@@ -2724,10 +2724,9 @@ getTcEvBindsAndTCVs ev_binds_var
; tcvs <- TcM.getTcEvTyCoVars ev_binds_var
; return (bnds, tcvs) }
getTcEvBindsMap :: TcS EvBindMap
getTcEvBindsMap
= do { ev_binds_var <- getTcEvBindsVar
; wrapTcS $ TcM.getTcEvBindsMap ev_binds_var }
getTcEvBindsMap :: EvBindsVar -> TcS EvBindMap
getTcEvBindsMap ev_binds_var
= wrapTcS $ TcM.getTcEvBindsMap ev_binds_var
unifyTyVar :: TcTyVar -> TcType -> TcS ()
-- Unify a meta-tyvar with a type
......
This diff is collapsed.
......@@ -2,7 +2,9 @@
T13877.hs:65:17: error:
• Couldn't match type ‘Apply p (x : xs)’ with ‘p (x : xs)’
Expected type: Sing x
-> Sing xs -> App [a] (':->) * p xs -> App [a] (':->) * p (x : xs)
-> Sing xs
-> App [a1] (':->) * p xs
-> App [a1] (':->) * p (x : xs)
Actual type: Sing x -> Sing xs -> (p @@ xs) -> p @@ (x : xs)
• In the expression: listElimPoly @(:->) @a @p @l
In an equation for ‘listElimTyFun’:
......@@ -10,14 +12,14 @@ T13877.hs:65:17: error:
• Relevant bindings include
listElimTyFun :: Sing l
-> (p @@ '[])
-> (forall (x :: a) (xs :: [a]).
-> (forall (x :: a1) (xs :: [a1]).
Sing x -> Sing xs -> (p @@ xs) -> p @@ (x : xs))
-> p @@ l
(bound at T13877.hs:65:1)
T13877.hs:65:41: error:
• Expecting one more argument to ‘p’
Expected kind ‘(-?>) [a] * (':->)’, but ‘p’ has kind ‘[a] ~> *’
Expected kind ‘(-?>) [a1] * (':->)’, but ‘p’ has kind ‘[a1] ~> *’
• In the type ‘p’
In the expression: listElimPoly @(:->) @a @p @l
In an equation for ‘listElimTyFun’:
......@@ -25,7 +27,7 @@ T13877.hs:65:41: error:
• Relevant bindings include
listElimTyFun :: Sing l
-> (p @@ '[])
-> (forall (x :: a) (xs :: [a]).
-> (forall (x :: a1) (xs :: [a1]).
Sing x -> Sing xs -> (p @@ xs) -> p @@ (x : xs))
-> p @@ l
(bound at T13877.hs:65:1)
{-# OPTIONS_GHC -fdefer-type-errors #-} -- Very important to this bug!
{-# Language PartialTypeSignatures #-}
{-# Language TypeFamilyDependencies, KindSignatures #-}
{-# Language PolyKinds #-}
{-# Language DataKinds #-}
{-# Language TypeFamilies #-}
{-# Language RankNTypes #-}
{-# Language NoImplicitPrelude #-}
{-# Language FlexibleContexts #-}
{-# Language MultiParamTypeClasses #-}
{-# Language GADTs #-}
{-# Language ConstraintKinds #-}
{-# Language FlexibleInstances #-}
{-# Language TypeOperators #-}
{-# Language ScopedTypeVariables #-}
{-# Language DefaultSignatures #-}
{-# Language FunctionalDependencies #-}
{-# Language UndecidableSuperClasses #-}
{-# Language UndecidableInstances #-}
{-# Language TypeInType #-}
{-# Language AllowAmbiguousTypes #-}
{-# Language InstanceSigs, TypeApplications #-}
module T14584 where
import Data.Monoid
import Data.Kind
data family Sing (a::k)
class SingKind k where
type Demote k = (res :: Type) | res -> k
fromSing :: Sing (a::k) -> Demote k
class SingI (a::k) where
sing :: Sing a
data ACT :: Type -> Type -> Type
data MHOM :: Type -> Type -> Type
type m %%- a = ACT m a -> Type
type m %%-> m' = MHOM m m' -> Type
class Monoid m => Action (act :: m %%- a) where
act :: m -> (a -> a)
class (Monoid m, Monoid m') => MonHom (mhom :: m %%-> m') where
monHom :: m -> m'
data MonHom_Distributive m :: (m %%- a) -> (a %%-> a)
type Good k = (Demote k ~ k, SingKind k)
instance (Action act, Monoid a, Good m) => MonHom (MonHom_Distributive m act :: a %%-> a) where
monHom :: a -> a
monHom = act @_ @_ @act (fromSing @m (sing @m @a :: Sing _))
T14584.hs:56:50: warning: [-Wdeferred-type-errors (in -Wdefault)]
• Expected kind ‘m1’, but ‘a’ has kind ‘*’
• In the type ‘a’
In the second argument of ‘fromSing’, namely
‘(sing @m @a :: Sing _)’
In the fourth argument of ‘act’, namely
‘(fromSing @m (sing @m @a :: Sing _))’
T14584.hs:56:60: warning: [-Wpartial-type-signatures (in -Wdefault)]
• Found type wildcard ‘_’ standing for ‘a :: m’
Where: ‘a’, ‘m’ are rigid type variables bound by
the instance declaration
at T14584.hs:54:10-89
• In an expression type signature: Sing _
In the second argument of ‘fromSing’, namely
‘(sing @m @a :: Sing _)’
In the fourth argument of ‘act’, namely
‘(fromSing @m (sing @m @a :: Sing _))’
• Relevant bindings include
monHom :: a -> a (bound at T14584.hs:56:3)
{-# OPTIONS_GHC -fdefer-type-errors #-} -- Very important to this bug!
{-# Language PartialTypeSignatures #-}
{-# Language KindSignatures #-}
{-# Language PolyKinds #-}
{-# Language ScopedTypeVariables #-}
{-# Language AllowAmbiguousTypes #-}
{-# Language TypeApplications #-}
module T14584a where
f :: forall m. ()
f = id @m :: _
g :: forall m. ()
g = let h = id @m
in h
T14584a.hs:12:5: warning: [-Wdeferred-type-errors (in -Wdefault)]
• Couldn't match expected type ‘()’ with actual type ‘m -> m’
• In the expression: id @m :: _
In an equation for ‘f’: f = id @m :: _
T14584a.hs:12:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
• Found type wildcard ‘_’ standing for ‘m -> m’
Where: ‘m’, ‘k’ are rigid type variables bound by
the type signature for:
f :: forall k2 (m :: k2). ()
at T14584a.hs:11:1-17
• In an expression type signature: _
In the expression: id @m :: _
In an equation for ‘f’: f = id @m :: _
• Relevant bindings include f :: () (bound at T14584a.hs:12:1)
T14584a.hs:16:8: warning: [-Wdeferred-type-errors (in -Wdefault)]
• Couldn't match expected type ‘()’ with actual type ‘m -> m’
• Probable cause: ‘h’ is applied to too few arguments
In the expression: h
In the expression: let h = id @m in h
In an equation for ‘g’: g = let h = id @m in h
• Relevant bindings include h :: m -> m (bound at T14584a.hs:15:9)
......@@ -67,3 +67,5 @@ test('T12732', normal, compile_fail, ['-fobject-code -fdefer-typed-holes'])
test('T14040a', normal, compile_fail, [''])
test('T14449', normal, compile_fail, [''])
test('T14479', normal, compile_fail, [''])
test('T14584', normal, compile, [''])
test('T14584a', normal, compile, [''])
......@@ -6,12 +6,6 @@ VtaFail.hs:7:16: error:
In an equation for ‘answer_nosig’:
answer_nosig = pairup_nosig @Int @Bool 5 True
VtaFail.hs:12:26: error:
• No instance for (Num Bool) arising from a use of ‘addOne’
• In the expression: addOne @Bool 5
In an equation for ‘answer_constraint_fail’:
answer_constraint_fail = addOne @Bool 5
VtaFail.hs:14:17: error:
• Cannot apply expression of type ‘p0 -> p0’
to a visible type argument ‘Int’
......
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