[GHC] #13822: GHC not using injectivity?

[GHC]

#13822: GHC not using injectivity?
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.0.1
      Resolution:                    |             Keywords:
                                     |  InjectiveFamilies, TypeInType
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 Iceland_jack):

 Output I do not understand, with explicit kinds / coercions

 {{{
 /tmp/v.hs:41:16: error:
     • Couldn't match kind ‘k’ with ‘'STAR’
       ‘k’ is a rigid type variable bound by
         the inferred type of
         maybeInt :: ((I 'STAR
                         ('TInt |> Sym (Ty U(hole:{a2uB}, k1, 'STAR)_N)_N)
 :: IK * 'STAR)
                      ~~
                      ((Int |> Sym Main.D:R:IK[0]) :: IK * 'STAR),
                      (I ('STAR ':> 'STAR)
                         ('TMaybe |> Sym
                                       (Ty
                                          (U(hole:{a2uB}, k1, 'STAR)_N
                                           ':> U(hole:{a2uC}, k,
 'STAR)_N)_N)_N) :: IK
 *
 ('STAR
 ':> 'STAR))
                      ~~
                      ((Maybe |> Sym
                                   (Main.D:R:IK[1] <'STAR>_N <'STAR>_N
                                    ; Sym (Sym Main.D:R:IK[0] -> Sym
 Main.D:R:IK[0]))) :: IK
 *
 ('STAR
 ':> 'STAR))) =>
                     TyRep
                       'STAR
                       ('TApp
                          'STAR
                          'STAR
                          ('TMaybe |> Sym
                                        (Ty
                                           (U(hole:{a2uB}, k1, 'STAR)_N
                                            ':> U(hole:{a2uC}, k,
 'STAR)_N)_N)_N)
                          ('TInt |> Sym (Ty U(hole:{a2uB}, k1,
 'STAR)_N)_N))
                     -> Maybe Int
         at /tmp/v.hs:23:3
       When matching types
         ('TMaybe |> Sym
                       (Ty
                          (U(hole:{a2uB}, k1, 'STAR)_N
                           ':> U(hole:{a2uC}, k, 'STAR)_N)_N)_N) :: Ty (k1
 ':> k)
         'TMaybe :: Ty ('STAR ':> 'STAR)
       Expected type: Maybe Int
         Actual type: (I 'STAR
                         ('TApp
                            'STAR
                            'STAR
                            ('TMaybe |> Sym
                                          (Ty
                                             (U(hole:{a2uB}, k1, 'STAR)_N
                                              ':> U(hole:{a2uC}, k,
 'STAR)_N)_N)_N)
                            ('TInt |> Sym
                                        (Ty U(hole:{a2uB}, k1,
 'STAR)_N)_N)) |> Main.D:R:IK[0])
     • In the expression: zero rep :: Maybe Int
       In an equation for ‘maybeInt’: maybeInt rep = zero rep :: Maybe Int
     • Relevant bindings include
         rep :: TyRep
                  'STAR
                  ('TApp
                     'STAR
                     'STAR
                     ('TMaybe |> Sym
                                   (Ty
                                      (U(hole:{a2uB}, k1, 'STAR)_N
                                       ':> U(hole:{a2uC}, k,
 'STAR)_N)_N)_N)
                     ('TInt |> Sym (Ty U(hole:{a2uB}, k1, 'STAR)_N)_N))
           (bound at /tmp/v.hs:41:10)
         maybeInt :: TyRep
                       'STAR
                       ('TApp
                          'STAR
                          'STAR
                          ('TMaybe |> Sym
                                        (Ty
                                           (U(hole:{a2uB}, k1, 'STAR)_N
                                            ':> U(hole:{a2uC}, k,
 'STAR)_N)_N)_N)
                          ('TInt |> Sym (Ty U(hole:{a2uB}, k1,
 'STAR)_N)_N))
                     -> Maybe Int
           (bound at /tmp/v.hs:41:1)
 Failed, modules loaded: none.
 }}}

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