Re: [GHC] #13848: Unexpected order of variable quantification with GADT constructor

23 Jun 2017

      #13848: Unexpected order of variable quantification with GADT constructor
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.0.1
  checker)                           |             Keywords:
      Resolution:                    |  TypeApplications
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 Hmm.  Fortunately we already have just the hook we need.

 Every interesting data constructor (including every GADT data con) has a
 wrapper; it is built by `MkId.mkDataConRep`.  Look at `wrapper_reqd` to
 see which data cons have wrappers.

 The wrapper mediates between the nice user view of the data constructor
 and the internal "representation data constructor" that GHC uses
 internally.  So for example
 {{{
   data T a where
     MkT :: forall p q. p -> q -> T (p,q)
 }}}
 The representation data con has this type
 {{{
   MkT :: forall r. forall p q. (r ~ (p,q)) => p -> q -> T r
 }}}
 But the wrapper is defined like this
 {{{
   $WMkT :: forall p q. p -> q -> T (p,q)
   $WMkT = /\p q. \(x::p) (y::q).
           MkT @(p,q) @p @q <(p,q)> x y
 }}}
 The `<(p,q)>` is a coercion argument (refl) witnessing `(p,q)~(p,q)`

 Now currently `dataConUserType` (which claims to show the user-written
 type of the data con) is thus (in `DataCon`):
 {{{
 dataConUserType (MkData { dcUnivTyVars = univ_tvs,
                           dcExTyVars = ex_tvs, dcEqSpec = eq_spec,
                           dcOtherTheta = theta, dcOrigArgTys = arg_tys,
                           dcOrigResTy = res_ty })
   = mkForAllTys (filterEqSpec eq_spec univ_tvs) $
     mkForAllTys ex_tvs $
     mkFunTys theta $
     mkFunTys arg_tys $
     res_ty
 }}}
 This `filterEqSpec` business is fishy!  But now we understand about
 wrappers, for data constructors that have wrappers we could insead use the
 type of the wrapper, thus:
 {{{
 dataConUserTYpe (MkData { dcRep = rep
                         , dcRepType = rep_ty }
   = case rep of
       DCR { dcr_wrap_id = wrap_id } -> idType wrap_id
       NoDataConRep                  -> rep_ty
         -- If there is no wrapper, the "rep-type" is the same
         -- as the "user type"
 }}}
 Whizzo.

 Now, to return to the ticket,
   * We should ensure that the wrapper type reflects exactly the
     type the user wrote including type variable order
   * That in turn may force to make a wrapper when we don't right now,
     just to swizzle round the type variables

 Make sense?

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