Fix Trac #10670
authorSimon Peyton Jones <simonpj@microsoft.com>
Thu, 23 Jul 2015 07:33:43 +0000 (08:33 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Thu, 23 Jul 2015 07:34:35 +0000 (08:34 +0100)
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.

compiler/basicTypes/DataCon.hs
compiler/typecheck/TcSplice.hs
testsuite/tests/polykinds/T10670.hs [new file with mode: 0644]
testsuite/tests/polykinds/T10670a.hs [new file with mode: 0644]
testsuite/tests/polykinds/all.T

index 5a72458..a70bcbd 100644 (file)
@@ -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
index 2e368a9..586b2b8 100644 (file)
@@ -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
diff --git a/testsuite/tests/polykinds/T10670.hs b/testsuite/tests/polykinds/T10670.hs
new file mode 100644 (file)
index 0000000..5b9cc72
--- /dev/null
@@ -0,0 +1,24 @@
+{-# 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
diff --git a/testsuite/tests/polykinds/T10670a.hs b/testsuite/tests/polykinds/T10670a.hs
new file mode 100644 (file)
index 0000000..d398cb7
--- /dev/null
@@ -0,0 +1,54 @@
+{-# 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
index c05e47e..3c8096c 100644 (file)
@@ -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, [''])