Commit af624071 authored by Richard Eisenberg's avatar Richard Eisenberg

Fix some casts.

This fixes #15346, and is a team effort between Ryan Scott and
myself (mostly Ryan). We discovered two errors related to FC's
"push" rules, one in the TPush rule (as implemented in pushCoTyArg)
and one in KPush rule (it shows up in liftCoSubstVarBndr).

The solution: do what the paper says, instead of whatever random
thoughts popped into my head as I was actually implementing.

Also fixes #15419, which is actually the same underlying problem.

Test case: dependent/should_compile/T{15346,15419}.
parent a606750b
......@@ -979,7 +979,7 @@ pushCoTyArg co ty
| isForAllTy tyL
= ASSERT2( isForAllTy tyR, ppr co $$ ppr ty )
Just (ty `mkCastTy` mkSymCo co1, MCo co2)
Just (ty `mkCastTy` co1, MCo co2)
| otherwise
= Nothing
......@@ -989,8 +989,8 @@ pushCoTyArg co ty
-- tyL = forall (a1 :: k1). ty1
-- tyR = forall (a2 :: k2). ty2
co1 = mkNthCo Nominal 0 co
-- co1 :: k1 ~N k2
co1 = mkSymCo (mkNthCo Nominal 0 co)
-- co1 :: k2 ~N k1
-- Note that NthCo can extract a Nominal equality between the
-- kinds of the types related by a coercion between forall-types.
-- See the NthCo case in CoreLint.
......
......@@ -1812,7 +1812,7 @@ liftCoSubstVarBndrUsing fun lc@(LC subst cenv) old_var
Pair k1 _ = coercionKind eta
new_var = uniqAway (getTCvInScope subst) (setVarType old_var k1)
lifted = Refl (TyVarTy new_var)
lifted = GRefl Nominal (TyVarTy new_var) (MCo eta)
new_cenv = extendVarEnv cenv old_var lifted
-- | Is a var in the domain of a lifting context?
......
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeApplications #-}
module T15346 where
import Data.Kind
import Data.Proxy
-----
type family Rep (a :: Type) :: Type
type instance Rep () = ()
type family PFrom (x :: a) :: Rep a
-----
class SDecide k where
test :: forall (a :: k). Proxy a
instance SDecide () where
test = undefined
test1 :: forall (a :: k). SDecide (Rep k) => Proxy a
test1 = seq (test @_ @(PFrom a)) Proxy
test2 :: forall (a :: ()). Proxy a
test2 = test1
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE UndecidableInstances #-}
module T15419 where
import Data.Kind
data Prod a b
data Proxy p = Proxy
-----
data family Sing :: forall k. k -> Type
data instance Sing x = STuple
-----
type family Rep1 (f :: k -> Type) :: k -> Type
type instance Rep1 ((,) a) = Prod a
type family From1 (f :: Type -> Type) a (z :: f a) :: Rep1 f a
type family To1 (f :: Type -> Type) a (z :: Rep1 f a) :: f a
class Generic1 (f :: Type -> Type) where
sFrom1 :: forall (a :: Type) (z :: f a). Proxy z -> Sing (From1 f a z)
sTo1 :: forall (a :: Type) (r :: Rep1 f a). Proxy r -> Proxy (To1 f a r :: f a)
instance Generic1 ((,) a) where
sFrom1 Proxy = undefined
sTo1 Proxy = undefined
-----
type family Fmap (g :: b) (x :: f a) :: f b
type instance Fmap (g :: b) (x :: (u, a)) = To1 ((,) u) b (Fmap g (From1 ((,) u) a x))
class PFunctor (f :: Type -> Type) where
sFmap :: forall a b (g :: b) (x :: f a).
Proxy g -> Sing x -> Proxy (Fmap g x)
instance PFunctor (Prod a) where
sFmap _ STuple = undefined
sFmap1 :: forall (f :: Type -> Type) (u :: Type) (b :: Type) (g :: b) (x :: f u).
(Generic1 f,
PFunctor (Rep1 f),
Fmap g x ~ To1 f b (Fmap g (From1 f u x)) )
=> Proxy g -> Proxy x -> Proxy (Fmap g x)
sFmap1 sg sx = sTo1 (sFmap sg (sFrom1 sx))
sFmap2 :: forall (p :: Type) (a :: Type) (b :: Type) (g :: b) (x :: (p, a)).
Proxy g -> Proxy x -> Proxy (Fmap g x)
sFmap2 = sFmap1
......@@ -51,3 +51,5 @@ test('T14845_compile', normal, compile, [''])
test('T14991', normal, compile, [''])
test('T15264', normal, compile, [''])
test('DkNameRes', normal, compile, [''])
test('T15346', normal, compile, [''])
test('T15419', 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