[GHC] #15579: topNormaliseType is wrong

[GHC]

#15579: topNormaliseType is wrong
-------------------------------------+-------------------------------------
        Reporter:  simonpj           |                Owner:  goldfire
            Type:  bug               |               Status:  new
        Priority:  highest           |            Milestone:  8.6.1
       Component:  Compiler          |              Version:  8.4.3
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Description changed by flip101:

Old description:

> I’m very puzzled about topNormaliseTYpe_maybe.  Here it is:
> {{{
> topNormaliseType_maybe env ty
>   = topNormaliseTypeX stepper mkTransCo ty
>   where
>     stepper = unwrapNewTypeStepper `composeSteppers` tyFamStepper
>
>     tyFamStepper rec_nts tc tys  -- Try to step a type/data family
>       = let (args_co, ntys) = normaliseTcArgs env Representational tc tys
> in
>           -- NB: It's OK to use normaliseTcArgs here instead of
>           -- normalise_tc_args (which takes the LiftingContext described
>           -- in Note [Normalising types]) because the reduceTyFamApp
> below
>           -- works only at top level. We'll never recur in this function
>           -- after reducing the kind of a bound tyvar.
>
>         case reduceTyFamApp_maybe env Representational tc ntys of
>           Just (co, rhs) -> NS_Step rec_nts rhs (args_co `mkTransCo` co)
>           _              -> NS_Done
> }}}
> I have two puzzlements
>
> 1. First, it seems utterly wrong to normalise the arguments using
> Representational.  Consider
> {{{
> F (N Int)
> where newtype N x = [x]
> }}}
>    We don’t want to reduce `(N Int)` to `[Int]`, and then try reducing
> `(F [Int])`!!   That is totally bogus.  Surely we should use (the role-
> aware) `normalise_tc_args` here?
>
> 2. I have literally no clue what `Note [Normalising types]` is all about.
> Moreover there is no Lifting Context passed to `normalise_tc_args`, so I
> don’t know what this stuff about `LiftingContext` is about. Is this
> historical baggage?
>
> Richard and I discussed this. (1) is a bug; for (2) the comment is
> misleading and should be deleted.
>
> Richard will do these things -- and will add examples to the mysterious
> `Note [Normalising types]`

New description:

 I’m very puzzled about topNormaliseTYpe_maybe.  Here it is:
 {{{#!haskell
 topNormaliseType_maybe env ty
   = topNormaliseTypeX stepper mkTransCo ty
   where
     stepper = unwrapNewTypeStepper `composeSteppers` tyFamStepper

     tyFamStepper rec_nts tc tys  -- Try to step a type/data family
       = let (args_co, ntys) = normaliseTcArgs env Representational tc tys
 in
           -- NB: It's OK to use normaliseTcArgs here instead of
           -- normalise_tc_args (which takes the LiftingContext described
           -- in Note [Normalising types]) because the reduceTyFamApp below
           -- works only at top level. We'll never recur in this function
           -- after reducing the kind of a bound tyvar.

         case reduceTyFamApp_maybe env Representational tc ntys of
           Just (co, rhs) -> NS_Step rec_nts rhs (args_co `mkTransCo` co)
           _              -> NS_Done
 }}}
 I have two puzzlements

 1. First, it seems utterly wrong to normalise the arguments using
 Representational.  Consider
 {{{#!haskell
 F (N Int)
 where newtype N x = [x]
 }}}
    We don’t want to reduce `(N Int)` to `[Int]`, and then try reducing `(F
 [Int])`!!   That is totally bogus.  Surely we should use (the role-aware)
 `normalise_tc_args` here?

 2. I have literally no clue what `Note [Normalising types]` is all about.
 Moreover there is no Lifting Context passed to `normalise_tc_args`, so I
 don’t know what this stuff about `LiftingContext` is about. Is this
 historical baggage?

 Richard and I discussed this. (1) is a bug; for (2) the comment is
 misleading and should be deleted.

 Richard will do these things -- and will add examples to the mysterious
 `Note [Normalising types]`

--

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