[GHC] #12919: Equality not used for substitution

[GHC]

#12919: Equality not used for substitution
-------------------------------------+-------------------------------------
        Reporter:  int-index         |                Owner:  goldfire
            Type:  bug               |               Status:  patch
        Priority:  highest           |            Milestone:  8.4.1
       Component:  Compiler (Type    |              Version:  8.0.1
  checker)                           |
      Resolution:                    |             Keywords:  TypeInType
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  GHC rejects       |            Test Case:
  valid program                      |  typecheck/should_compile/T12919
      Blocked By:                    |             Blocking:  14441
 Related Tickets:  #13643            |  Differential Rev(s):  Phab:D3848
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Old description:

> This code
>
> {{{
> {-# LANGUAGE TypeInType, TypeFamilies, GADTs, ConstraintKinds #-}
>
> module T12919 where
>
> import Data.Kind
>
> data N = Z
>
> data V :: N -> Type where
>   VZ :: V Z
>
> type family VC (n :: N) :: Type where
>   VC Z = Type
>
> type family VF (xs :: V n) (f :: VC n) :: Type where
>   VF VZ f = f
>
> data Dict c where
>   Dict :: c => Dict c
>
> prop :: xs ~ VZ => Dict (VF xs f ~ f)
> prop = Dict
> }}}
>
> fails with this error:
>
> {{{
> T12919.hs:22: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 T12919.hs:21:9
>     • In the expression: Dict
>       In an equation for ‘prop’: prop = Dict
>     • Relevant bindings include
>         prop :: Dict VF xs f ~ f (bound at T12919.hs:22: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.

New description:

 This code

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

 module T12919 where

 import Data.Kind

 data N = Z

 data V :: N -> Type where
   VZ :: V Z

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

 type family VF (xs :: V n) (f :: VC n) :: Type where
   VF VZ f = f

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

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

 fails with this error:

 {{{
 T12919.hs:22: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 T12919.hs:21:9
     • In the expression: Dict
       In an equation for ‘prop’: prop = Dict
     • Relevant bindings include
         prop :: Dict VF xs f ~ f (bound at T12919.hs:22: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 (by bgamari):

 A brief status update on this: Richard presented me with a patch fixing
 this a few months ago, giving me the task to reduce its footprint on
 compiler performance. He provided a few possible avenues for inquiry, a
 few of which I have explored. The result can be found on the `wip/T12919`
 branch. Unfortunately more performance improvement is necessary as several
 compiler performance testcases are still regressing in allocations by
 >50%.

 Sadly, I have recently lacked the time to dig back into the issue. Alex
 Vieth will be picking up the task shortly.

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