Re: [GHC] #12919: Equality not used for substitution

18 Dec 2017

      #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