[commit: ghc] master: Fix some casts. (af62407)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : master
Link       : http://ghc.haskell.org/trac/ghc/changeset/af624071fa063158d6e963e171280676f9c0a0b0/ghc

>---------------------------------------------------------------

commit af624071fa063158d6e963e171280676f9c0a0b0
Author: Richard Eisenberg <rae at cs.brynmawr.edu>
Date:   Thu Jul 19 00:16:13 2018 -0400

    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}.


>---------------------------------------------------------------

af624071fa063158d6e963e171280676f9c0a0b0
 compiler/coreSyn/CoreOpt.hs                        |  6 +--
 compiler/types/Coercion.hs                         |  2 +-
 testsuite/tests/dependent/should_compile/T15346.hs | 31 ++++++++++++
 testsuite/tests/dependent/should_compile/T15419.hs | 55 ++++++++++++++++++++++
 testsuite/tests/dependent/should_compile/all.T     |  2 +
 5 files changed, 92 insertions(+), 4 deletions(-)

diff --git a/compiler/coreSyn/CoreOpt.hs b/compiler/coreSyn/CoreOpt.hs
index 8684c84..11cbd1e 100644
--- a/compiler/coreSyn/CoreOpt.hs
+++ b/compiler/coreSyn/CoreOpt.hs
@@ -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.
diff --git a/compiler/types/Coercion.hs b/compiler/types/Coercion.hs
index 2ca5151..1557ce0 100644
--- a/compiler/types/Coercion.hs
+++ b/compiler/types/Coercion.hs
@@ -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?
diff --git a/testsuite/tests/dependent/should_compile/T15346.hs b/testsuite/tests/dependent/should_compile/T15346.hs
new file mode 100644
index 0000000..3d8d49b
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T15346.hs
@@ -0,0 +1,31 @@
+{-# 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
diff --git a/testsuite/tests/dependent/should_compile/T15419.hs b/testsuite/tests/dependent/should_compile/T15419.hs
new file mode 100644
index 0000000..68f20e5
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T15419.hs
@@ -0,0 +1,55 @@
+{-# 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
diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T
index 64782c0..4e096c1 100644
--- a/testsuite/tests/dependent/should_compile/all.T
+++ b/testsuite/tests/dependent/should_compile/all.T
@@ -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, [''])