Commit 7d2e5da6 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Fix zonk_eq_types in TcCanonical

This fixes Trac #13083. An egregious bug.

Merge to the 8.0 branch
parent 6c869f90
......@@ -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
......
{-# 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
......@@ -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, [''])
......@@ -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 _
......
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