diff options
| -rw-r--r-- | compiler/typecheck/TcCanonical.hs | 19 | ||||
| -rw-r--r-- | testsuite/tests/typecheck/should_compile/T13083.hs | 80 | ||||
| -rw-r--r-- | testsuite/tests/typecheck/should_compile/all.T | 1 | ||||
| -rw-r--r-- | testsuite/tests/typecheck/should_fail/T3950.stderr | 2 |
4 files changed, 96 insertions, 6 deletions
diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs index 5aeeeb8e18..7f5ea9aaa8 100644 --- a/compiler/typecheck/TcCanonical.hs +++ b/compiler/typecheck/TcCanonical.hs @@ -700,8 +700,15 @@ zonk_eq_types = go go ty1 ty2 | Just (tc1, tys1) <- tcRepSplitTyConApp_maybe ty1 , Just (tc2, tys2) <- tcRepSplitTyConApp_maybe ty2 - , tc1 == tc2 - = tycon tc1 tys1 tys2 + = if tc1 == tc2 && tys1 `equalLength` tys2 + -- Crucial to check for equal-length args, because + -- we cannot assume that the two args to 'go' have + -- the same kind. E.g go (Proxy * (Maybe Int)) + -- (Proxy (*->*) Maybe) + -- We'll call (go (Maybe Int) Maybe) + -- See Trac #13083 + then tycon tc1 tys1 tys2 + else bale_out ty1 ty2 go ty1 ty2 | Just (ty1a, ty1b) <- tcRepSplitAppTy_maybe ty1 @@ -714,12 +721,14 @@ zonk_eq_types = go | lit1 == lit2 = return (Right ty1) - go ty1 ty2 = return $ Left (Pair ty1 ty2) - -- we don't handle more complex forms here + go ty1 ty2 = bale_out ty1 ty2 + -- We don't handle more complex forms here + + bale_out ty1 ty2 = return $ Left (Pair ty1 ty2) tyvar :: SwapFlag -> TcTyVar -> TcType -> TcS (Either (Pair TcType) TcType) - -- try to do as little as possible, as anything we do here is redundant + -- Try to do as little as possible, as anything we do here is redundant -- with flattening. In particular, no need to zonk kinds. That's why -- we don't use the already-defined zonking functions tyvar swapped tv ty diff --git a/testsuite/tests/typecheck/should_compile/T13083.hs b/testsuite/tests/typecheck/should_compile/T13083.hs new file mode 100644 index 0000000000..220da0855a --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/T13083.hs @@ -0,0 +1,80 @@ +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE UndecidableInstances #-} + +{-# OPTIONS_GHC -Wall #-} + +-- | Bug(?) in Coercible constraint solving + +module T13083 where + +import GHC.Generics (Par1(..),(:*:)(..)) +import GHC.Exts (coerce) + +-- Representation as free vector space +type family V (a :: *) :: * -> * + +type instance V R = Par1 +type instance V (a,b) = V a :*: V b + +type instance V (Par1 a) = V a + +data R = R + +-- Linear map in row-major order +newtype L a b = L (V b (V a R)) + +-- Use coerce to drop newtype wrapper +bar :: L a b -> V b (V a R) +bar = coerce + +{- +[W] L a b ~R V b (V a R) +--> + V b (V a R) ~R V b (V a R) +-} + +{-------------------------------------------------------------------- + Bug demo +--------------------------------------------------------------------} + +-- A rejected type specialization of bar with a ~ (R,R), b ~ (Par1 R,R) +foo :: L (R,R) (Par1 R,R) -> V (Par1 R,R) (V (R,R) R) +-- foo :: L (a1,R) (Par1 b1,b2) -> V (Par1 b1,b2) (V (a1,R) R) +foo = coerce + +{- +[W] L (a1,R) (Par1 b1, b2) ~R V (Par1 b1,b2) (V (a1,R) R) +--> + V (Par1 b1, b2) (V (a1,R) R) ~R same + + -> (V (Par1 b1) :*: V b2) ((V a1 :*: V R) R) + -> (:*:) (V b1) (V b2) (:*: (V a1) Par1 R) + +--> + L (a1,R) (Par1 b1, b2) ~R (:*:) (V b1) (V b2) (:*: (V a1) Par1 R) +-} + +-- • Couldn't match representation of type ‘V Par1’ +-- with that of ‘Par1’ +-- arising from a use of ‘coerce’ + +-- Note that Par1 has the wrong kind (* -> *) for V Par1 + +-- Same error: +-- +-- foo :: (a ~ (R,R), b ~ (Par1 R,R)) => L a b -> V b (V a R) + +-- The following similar signatures work: + +-- foo :: L (R,R) (R,Par1 R) -> V (R,Par1 R) (V (R,R) R) +-- foo :: L (Par1 R,R) (R,R) -> V (R,R) (V (Par1 R,R) R) + +-- Same error: + +-- -- Linear map in column-major order +-- newtype L a b = L (V a (V b s)) + +-- foo :: L (R,R) (Par1 R,R) -> V (R,R) (V (Par1 R,R) R) +-- foo = coerce + diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T index 40d31bbadb..b70ab83b34 100644 --- a/testsuite/tests/typecheck/should_compile/all.T +++ b/testsuite/tests/typecheck/should_compile/all.T @@ -564,3 +564,4 @@ test('T12925', normal, compile, ['']) test('T12919', expect_broken(12919), compile, ['']) test('T12936', normal, compile, ['']) test('T13050', normal, compile, ['-fdefer-type-errors']) +test('T13083', normal, compile, ['']) diff --git a/testsuite/tests/typecheck/should_fail/T3950.stderr b/testsuite/tests/typecheck/should_fail/T3950.stderr index ae50a74f3c..60da6c09ae 100644 --- a/testsuite/tests/typecheck/should_fail/T3950.stderr +++ b/testsuite/tests/typecheck/should_fail/T3950.stderr @@ -5,7 +5,7 @@ T3950.hs:15:8: error: w :: (* -> * -> *) -> * Sealed :: (* -> *) -> * Expected type: Maybe (w (Id p)) - Actual type: Maybe (Sealed (Id p x0)) + Actual type: Maybe (Sealed (Id p0 x0)) • In the expression: Just rp' In an equation for ‘rp’: rp _ |