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

2 Dec 2016

      #12919: Equality not used for substitution
-------------------------------------+-------------------------------------
        Reporter:  int-index         |                Owner:
            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:                    |
-------------------------------------+-------------------------------------

Comment (by int-index):

 Running the test actually resulted in a Core Lint error:

 {{{
 Compile failed (exit code 1) errors were:
 *** Core Lint errors : in result of Desugar (after optimization) ***
 <no location info>: warning:
     [in body of lambda with binder $d~_aEs :: (xs :: V 'Z)
                                               ~
                                               ('VZ :: V 'Z)]
     From-type of Cast differs from type of enclosed expression
     From-type: VC 'Z
     Type of enclosed expr: Type
     Actual enclosed expr: f
     Coercion used in cast: D:R:VC[0]
 *** Offending Program ***
 prop
   :: forall (xs :: V 'Z) f.
      (xs :: V 'Z) ~ ('VZ :: V 'Z) =>
      Dict (VF xs (f |> Sym (D:R:VC[0])) :: Type) ~ (f :: Type)
 [LclIdX]
 prop =
   \ (@ (xs_aEp :: V 'Z))
     (@ f_aEq)
     ($d~_aEs :: (xs :: V 'Z) ~ ('VZ :: V 'Z)) ->
     case HEq_sc
            @ (V 'Z) @ (V 'Z) @ xs @ 'VZ ($p1~ @ (V 'Z) @ xs @ 'VZ $d~_aEs)
     of cobox_aEM
     { __DEFAULT ->
     (Dict
        @ (f :: Type) ~ (f :: Type)
        ($f~kab
           @ *
           @ f
           @ f
           (Eq# @ * @ * @ f @ f @~ (<f>_N :: (f :: Type) ~# (f :: Type)))))
     `cast` ((Dict
                ((~)
                   <*>_N
                   (Trans
                        (Sym (D:R:VF[0] (Coh <f>_N (D:R:VC[0]))))
                        (VF
                           <'Z>_N
                           (Sym cobox)
                           (Sym (Coh (Sym (Coh <f>_N <Type>_N)) (Sym
 (D:R:VC[0])))))_N)
                   <f>_N)_R)_R
             :: (Dict (f :: *) ~ (f :: *) :: *)
                ~R#
                (Dict (VF xs (f |> Sym (D:R:VC[0])) :: *) ~ (f :: *) :: *))
     }

 $trModule :: Module
 [LclIdX]
 $trModule = Module (TrNameS "main"#) (TrNameS "T12919"#)

 $tc'Z :: TyCon
 [LclIdX]
 $tc'Z =
   TyCon
     4444267892940526647##
     16578485670798467485##
     $trModule
     (TrNameS "'Z"#)

 $tcN :: TyCon
 [LclIdX]
 $tcN =
   TyCon
     17882793663470508219##
     7927123420536316171##
     $trModule
     (TrNameS "N"#)

 $tc'VZ :: TyCon
 [LclIdX]
 $tc'VZ =
   TyCon
     17982818364639448466##
     3866213651802933295##
     $trModule
     (TrNameS "'VZ"#)

 $tcV :: TyCon
 [LclIdX]
 $tcV =
   TyCon
     2444936942366493139##
     17118784387149548812##
     $trModule
     (TrNameS "V"#)

 $tc'Dict :: TyCon
 [LclIdX]
 $tc'Dict =
   TyCon
     12076319013818359472##
     5127630525431558702##
     $trModule
     (TrNameS "'Dict"#)

 $tcDict :: TyCon
 [LclIdX]
 $tcDict =
   TyCon
     8038429513029328469##
     10238893879637068951##
     $trModule
     (TrNameS "Dict"#)

 *** End of Offense ***

 }}}

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