[GHC] #16204: GHC HEAD-only Core Lint error (Argument value doesn't match argument type)

[GHC]

#16204: GHC HEAD-only Core Lint error (Argument value doesn't match argument type)
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  highest           |            Milestone:  8.8.1
       Component:  Compiler (Type    |              Version:  8.7
  checker)                           |
      Resolution:                    |             Keywords:  TypeInType
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Compile-time      |  Unknown/Multiple
  crash or panic                     |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #16188            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 This isn't even the only issue with this program that's surfaced on GHC
 HEAD. If you use this slightly modified version of `genericToSing` (the
 only difference is that the explicit `@(Rep k)` argument has been
 removed):

 {{{#!hs
 genericToSing :: forall k.
                  ( SingKind k, SGeneric k, SingKind (Rep k)
                  , Generic (Demote k), Rep (Demote k) ~ Demote (Rep k) )
               => Demote k -> SomeSing k
 genericToSing d = withSomeSing (from d) $ SomeSing . sTo
 }}}

 Then GHC 8.6.3 compiles it successfully, whereas GHC HEAD gives a strange
 error:

 {{{
 $ ~/Software/ghc4/inplace/bin/ghc-stage2 Bug.hs
 [1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

 Bug.hs:49:33: error:
     • Could not deduce: Demote k0 ~ Demote (Rep k)
       from the context: (SingKind k, SGeneric k, SingKind (Rep k),
                          Generic (Demote k), Rep (Demote k) ~ Demote (Rep
 k))
         bound by the type signature for:
                    genericToSing :: forall k.
                                     (SingKind k, SGeneric k, SingKind (Rep
 k), Generic (Demote k),
                                      Rep (Demote k) ~ Demote (Rep k)) =>
                                     Demote k -> SomeSing k
         at Bug.hs:(45,1)-(48,39)
       Expected type: Demote k0
         Actual type: Rep (Demote k)
       NB: ‘Demote’ is a non-injective type family
       The type variable ‘k0’ is ambiguous
     • In the first argument of ‘withSomeSing’, namely ‘(from d)’
       In the expression: withSomeSing (from d)
       In the expression: withSomeSing (from d) $ SomeSing . sTo
     • Relevant bindings include
         d :: Demote k (bound at Bug.hs:49:15)
         genericToSing :: Demote k -> SomeSing k (bound at Bug.hs:49:1)
    |
 49 | genericToSing d = withSomeSing (from d) $ SomeSing . sTo
    |                                 ^^^^^^
 }}}

 It's unclear to me if this issue is the same as the one causing the Core
 Lint error or not.

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