Commit 5c3fc921 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Fix Trac #10670

In dataConCannotMatch we were using a GADT data con without
properly instantiating the existential type variables.
The fix is easy, and the code is tighter.
parent dd365b1b
......@@ -19,7 +19,7 @@ module DataCon (
buildAlgTyCon,
-- ** Type deconstruction
dataConRepType, dataConSig, dataConFullSig,
dataConRepType, dataConSig, dataConInstSig, dataConFullSig,
dataConName, dataConIdentity, dataConTag, dataConTyCon,
dataConOrigTyCon, dataConUserType,
dataConUnivTyVars, dataConExTyVars, dataConAllTyVars,
......@@ -73,6 +73,7 @@ import qualified Data.Typeable
import Data.Maybe
import Data.Char
import Data.Word
import Data.List( mapAccumL )
{-
Data constructor representation
......@@ -857,6 +858,25 @@ dataConSig (MkData {dcUnivTyVars = univ_tvs, dcExTyVars = ex_tvs,
dcOrigArgTys = arg_tys, dcOrigResTy = res_ty})
= (univ_tvs ++ ex_tvs, eqSpecPreds eq_spec ++ theta, arg_tys, res_ty)
dataConInstSig
:: DataCon
-> [Type] -- Instantiate the *universal* tyvars with these types
-> ([TyVar], ThetaType, [Type]) -- Return instantiated existentials
-- theta and arg tys
-- ^ Instantantiate the universal tyvars of a data con,
-- returning the instantiated existentials, constraints, and args
dataConInstSig (MkData { dcUnivTyVars = univ_tvs, dcExTyVars = ex_tvs
, dcEqSpec = eq_spec, dcOtherTheta = theta
, dcOrigArgTys = arg_tys })
univ_tys
= (ex_tvs'
, substTheta subst (eqSpecPreds eq_spec ++ theta)
, substTys subst arg_tys)
where
univ_subst = zipTopTvSubst univ_tvs univ_tys
(subst, ex_tvs') = mapAccumL Type.substTyVarBndr univ_subst ex_tvs
-- | The \"full signature\" of the 'DataCon' returns, in order:
--
-- 1) The result of 'dataConUnivTyVars'
......@@ -990,16 +1010,11 @@ dataConCannotMatch :: [Type] -> DataCon -> Bool
-- NB: look at *all* equality constraints, not only those
-- in dataConEqSpec; see Trac #5168
dataConCannotMatch tys con
| null theta = False -- Common
| null inst_theta = False -- Common
| all isTyVarTy tys = False -- Also common
| otherwise
= typesCantMatch [(Type.substTy subst ty1, Type.substTy subst ty2)
| (ty1, ty2) <- concatMap predEqs theta ]
| otherwise = typesCantMatch (concatMap predEqs inst_theta)
where
dc_tvs = dataConUnivTyVars con
theta = dataConTheta con
subst = ASSERT2( length dc_tvs == length tys, ppr con $$ ppr dc_tvs $$ ppr tys )
zipTopTvSubst dc_tvs tys
(_, inst_theta, _) = dataConInstSig con tys
-- TODO: could gather equalities from superclasses too
predEqs pred = case classifyPredType pred of
......
......@@ -1136,16 +1136,12 @@ reifyTyCon tc
reifyDataCon :: [Type] -> DataCon -> TcM TH.Con
-- For GADTs etc, see Note [Reifying data constructors]
reifyDataCon tys dc
= do { let (tvs, theta, arg_tys, _) = dataConSig dc
subst = mkTopTvSubst (tvs `zip` tys) -- Dicard ex_tvs
(subst', ex_tvs') = mapAccumL substTyVarBndr subst (dropList tys tvs)
theta' = substTheta subst' theta
arg_tys' = substTys subst' arg_tys
= do { let (ex_tvs, theta, arg_tys) = dataConInstSig dc tys
stricts = map reifyStrict (dataConSrcBangs dc)
fields = dataConFieldLabels dc
name = reifyName dc
; r_arg_tys <- reifyTypes arg_tys'
; r_arg_tys <- reifyTypes arg_tys
; let main_con | not (null fields)
= TH.RecC name (zip3 (map reifyName fields) stricts r_arg_tys)
......@@ -1158,12 +1154,12 @@ reifyDataCon tys dc
[s1, s2] = stricts
; ASSERT( length arg_tys == length stricts )
if null ex_tvs' && null theta then
if null ex_tvs && null theta then
return main_con
else do
{ cxt <- reifyCxt theta'
; ex_tvs'' <- reifyTyVars ex_tvs'
; return (TH.ForallC ex_tvs'' cxt main_con) } }
{ cxt <- reifyCxt theta
; ex_tvs' <- reifyTyVars ex_tvs
; return (TH.ForallC ex_tvs' cxt main_con) } }
------------------------------
reifyClass :: Class -> TcM TH.Info
......
{-# LANGUAGE ScopedTypeVariables, RankNTypes, GADTs, PolyKinds #-}
module T10670 where
import Unsafe.Coerce
data TypeRepT (a::k) where
TRCon :: TypeRepT a
data G2 c a where
G2 :: TypeRepT a -> TypeRepT b -> G2 c (c a b)
getT2 :: TypeRepT (c :: k2 -> k1 -> k) -> TypeRepT (a :: k) -> Maybe (G2 c a)
{-# NOINLINE getT2 #-}
getT2 c t = Nothing
tyRepTArr :: TypeRepT (->)
{-# NOINLINE tyRepTArr #-}
tyRepTArr = TRCon
s :: forall a x. TypeRepT (a :: *) -> Maybe x
s tf = case getT2 tyRepTArr tf :: Maybe (G2 (->) a) of
Just (G2 _ _) -> Nothing
_ -> Nothing
{-# LANGUAGE GADTs , PolyKinds #-}
module Bug2 where
import Unsafe.Coerce
data TyConT (a::k) = TyConT String
eqTyConT :: TyConT a -> TyConT b -> Bool
eqTyConT (TyConT a) (TyConT b) = a == b
tyConTArr :: TyConT (->)
tyConTArr = TyConT "(->)"
data TypeRepT (a::k) where
TRCon :: TyConT a -> TypeRepT a
TRApp :: TypeRepT a -> TypeRepT b -> TypeRepT (a b)
data GetAppT a where
GA :: TypeRepT a -> TypeRepT b -> GetAppT (a b)
getAppT :: TypeRepT a -> Maybe (GetAppT a)
getAppT (TRApp a b) = Just $ GA a b
getAppT _ = Nothing
eqTT :: TypeRepT (a::k1) -> TypeRepT (b::k2) -> Bool
eqTT (TRCon a) (TRCon b) = eqTyConT a b
eqTT (TRApp c a) (TRApp d b) = eqTT c d && eqTT a b
eqTT _ _ = False
data G2 c a where
G2 :: TypeRepT a -> TypeRepT b -> G2 c (c a b)
getT2 :: TypeRepT (c :: k2 -> k1 -> k) -> TypeRepT (a :: k) -> Maybe (G2 c a)
getT2 c t = do GA t' b <- getAppT t
GA c' a <- getAppT t'
if eqTT c c'
then Just (unsafeCoerce $ G2 a b :: G2 c a)
else Nothing
tyRepTArr :: TypeRepT (->)
tyRepTArr = TRCon tyConTArr
s tf = case getT2 tyRepTArr tf
of Just (G2 _ _) -> Nothing
_ -> Nothing
......@@ -117,3 +117,5 @@ test('T10451', normal, compile_fail, [''])
test('T10516', normal, compile_fail, [''])
test('T10503', normal, compile_fail, [''])
test('T10570', normal, compile_fail, [''])
test('T10670', normal, compile, [''])
test('T10670a', 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