[GHC] #12919: Equality not used for substitution

[GHC]

#12919: Equality not used for substitution
-------------------------------------+-------------------------------------
        Reporter:  int-index         |                Owner:  goldfire
            Type:  bug               |               Status:  new
        Priority:  high              |            Milestone:
       Component:  Compiler (Type    |              Version:  8.0.1
  checker)                           |
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  GHC rejects       |  Unknown/Multiple
  valid program                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by simonpj):

 * owner:   => goldfire


@@ -6,0 +6,2 @@
+ module T12919 where
+
@@ -8,1 +10,1 @@
- data N = Z
+ data Nat = Z
@@ -10,2 +12,2 @@
- data V :: N -> Type where
-   VZ :: V Z
+ data D :: Nat -> Type where
+   DZ :: D Z
@@ -13,1 +15,1 @@
- type family VC (n :: N) :: Type where
+ type family VC (n :: Nat) :: Type where
@@ -16,2 +18,2 @@
- type family VF (xs :: V n) (f :: VC n) :: Type where
-   VF VZ f = f
+ type family VF (xs :: D n) (f :: VC n) :: Type where
+   VF DZ f = f
@@ -22,1 +24,1 @@
- prop :: xs ~ VZ => Dict (VF xs f ~ f)
+ prop :: xs ~ DZ => Dict (VF xs f ~ f)

New description:

 This code

 {{{
 {-# LANGUAGE TypeInType, TypeFamilies, GADTs, ConstraintKinds #-}

 module T12919 where

 import Data.Kind

 data Nat = Z

 data D :: Nat -> Type where
   DZ :: D Z

 type family VC (n :: Nat) :: Type where
   VC Z = Type

 type family VF (xs :: D n) (f :: VC n) :: Type where
   VF DZ f = f

 data Dict c where
   Dict :: c => Dict c

 prop :: xs ~ DZ => Dict (VF xs f ~ f)
 prop = Dict
 }}}

 fails with this error:

 {{{
 Op.hs:20:8: error:
     • Couldn't match type ‘f’ with ‘VF 'VZ f’
         arising from a use of ‘Dict’
       ‘f’ is a rigid type variable bound by
         the type signature for:
           prop :: forall (xs :: V 'Z) f. xs ~ 'VZ => Dict VF xs f ~ f
         at Op.hs:19:9
     • In the expression: Dict
       In an equation for ‘prop’: prop = Dict
     • Relevant bindings include
         prop :: Dict VF xs f ~ f (bound at Op.hs:20:1)
 }}}

 However, if I substitute `xs` with `VZ` (by hand) in the type of `prop`,
 it compiles. Can be reproduced with GHC 8.0.1 but not HEAD.

--

Comment:

 Richard, could you look at this?  It's an outright bug.  I had a look and
 my brain melted.

 * We seem to be flattening a type `((f::*) |> Sym D:R:VC[0])`, where I
 think
 {{{
 axiom D:R:VC[0] :: VC Z ~ Type
 }}}
   But the result of this flattening seems to be `((f:*) |> D:R:VC[0])`,
 which is plainly wrong.

 * I don't understand the code
 {{{
 flatten_one (CastTy ty g)
   = do { (xi, co) <- flatten_one ty
        ; (g', _) <- flatten_co g
        ; return (mkCastTy xi g', castCoercionKind co g' g) }
 }}}
   It seems suspicious that the evidence returned by `flatten_co` is
 discarded.

 *  `flatten_co` is inadequately commented.  Perhaps
 {{{
   If  r is a role
       co :: s ~r t
       flatten_co co = (fco, kco)

   then
       fco :: fs ~r ft
       fs, ft are flattened types
       kco :: (fs ~r ft) ~N# (s ~r t)
 }}}
   But I'm really not sure.

 * The `flatten_one (CastTy ty g)` plan seems quite baroque when applied to
 `((f::*) |> D:R:VC[0])`.  Apparently, in `flatten_co` we
   * Take the coercion `D:R:VC[0]`, and flatten its from-type `*`, and its
 to-type `VC Z`.
   * Flattening its to-type uses `Sym D:R:VC[0]` to produce `*` again.
   * So we end up with `Refl ; D:R:VC[0] : Sym D:R:VC[0]`, which seems a
 bit of a waste.

 Generally, could you add a note about flattening `(t |> g)`?

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12919#comment:2>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler