[GHC] #13549: GHC 8.2.1's typechecker rejects code generated by singletons that 8.0 accepts

[GHC]

#13549: GHC 8.2.1's typechecker rejects code generated by singletons that 8.0
accepts
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  high              |            Milestone:  8.2.1
       Component:  Compiler (Type    |              Version:  8.1
  checker)                           |
      Resolution:                    |             Keywords:  TypeInType
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 RyanGlScott):

 Replying to [comment:9 RyanGlScott]:
 > And I think that's probably the limit of my ability to debug this :)

 OK, I lied. I //was// able to discover a workaround by placing kind
 signatures at random places until I found a trick that worked reliably.
 Here's how you can fix each of the files I posted:

 {{{#!diff
 diff --git a/Bug.hs b/Bug.hs
 index d534fe0..52163b8 100644
 --- a/Bug.hs
 +++ b/Bug.hs
 @@ -1127,7 +1127,7 @@ src/Data/Singletons/Prelude/List.hs:(260,3)-(806,4):
 Splicing declar
            lambda_a33gY xs0_a33gZ
              = let
                  sPerms ::
 -                  forall arg_a33h0 arg_a33h1.
 +                  forall (arg_a33h0 :: [a_a337f]) arg_a33h1.
                    Sing arg_a33h0
                    -> Sing arg_a33h1
                       -> Sing (Apply (Apply
 (Let6989586621679736931PermsSym1 xs0_a33a0) ar
 @@ -1153,7 +1153,7 @@ src/Data/Singletons/Prelude/List.hs:(260,3)-(806,4):
 Splicing declar
                        lambda_a33ha t_a33hb ts_a33hc is_a33hd
                          = let
                              sInterleave' ::
 -                              forall arg_a33he arg_a33hf arg_a33hg.
 +                              forall (arg_a33he :: TyFun [a_a337f] k ->
 Type) arg_a33hf a
                                Sing arg_a33he
                                -> Sing arg_a33hf
                                   -> Sing arg_a33hg
 }}}

 {{{#!diff
 diff --git a/Bug2.hs b/Bug2.hs
 index 98fbbf0..75c4523 100644
 --- a/Bug2.hs
 +++ b/Bug2.hs
 @@ -393,7 +393,7 @@ src/Data/Singletons/Prelude/List.hs:(260,3)-(806,4):
 Splicing declarat
            lambda_a33gY xs0_a33gZ
              = let
                  sPerms ::
 -                  forall arg_a33h0 arg_a33h1.
 +                  forall (arg_a33h0 :: [k]) arg_a33h1.
                    Sing arg_a33h0
                    -> Sing arg_a33h1
                       -> Sing (Apply (Apply
 (Let6989586621679736931PermsSym1 xs0_a33a0) ar
 @@ -419,7 +419,7 @@ src/Data/Singletons/Prelude/List.hs:(260,3)-(806,4):
 Splicing declarat
                        lambda_a33ha t_a33hb ts_a33hc is_a33hd
                          = let
                              sInterleave' ::
 -                              forall arg_a33he arg_a33hf arg_a33hg.
 +                              forall (arg_a33he :: TyFun [k] j -> Type)
 arg_a33hf arg_a33
                                Sing arg_a33he
                                -> Sing arg_a33hf
                                   -> Sing arg_a33hg
 }}}

 {{{#!diff
 diff --git a/Bug3.hs b/Bug3.hs
 index 77484b2..a286b43 100644
 --- a/Bug3.hs
 +++ b/Bug3.hs
 @@ -115,7 +115,7 @@ lambda_a33gY _
                    lambda_a33ha _ _ _
                      = let
                          sInterleave' ::
 -                          forall arg_a33he arg_a33hf arg_a33hg.
 +                          forall (arg_a33he :: TyFun [k] j -> Type)
 (arg_a33hf :: [y]) (arg_a33hg :: z).
                            Sing arg_a33he
                            -> Sing arg_a33hf
                               -> Sing arg_a33hg
 }}}

 The `Bug3` fix is interesting, since I didn't have to specify the kind of
 a type variable in `sPerms`. But perhaps that's just because I had
 replaced so many things by `undefined` by that point that the kind
 inference behavior had changed.

 So now the question is: is this just another occurrence of #13555 in
 disguise? Or is there an actual bug here?

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