Opened 4 months ago

Closed 3 months ago

Last modified 3 months ago

#13549 closed bug (duplicate)

GHC 8.2.1's typechecker rejects code generated by singletons that 8.0 accepts

Reported by: RyanGlScott Owned by:
Priority: normal Milestone: 8.4.1
Component: Compiler (Type checker) Version: 8.1
Keywords: TypeInType Cc: goldfire
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description (last modified by RyanGlScott)

I recently attempted to upgrade singletons to use GHC 8.2.1, but was thwarted when GHC's typechecker rejected code that was generated by Template Haskell. I was able to put all of this code in a single module (which I've attached), but sadly, it's 1367 lines long. What's important is that GHC 8.0.1 and 8.0.2 accept this code, but neither 8.2.1-rc1 nor HEAD do. Here is the error message you get, in its full glory:

$ /opt/ghc/8.2.1/bin/ghci Bug.hs -fprint-explicit-kinds
GHCi, version 8.2.0.20170403: http://www.haskell.org/ghc/  :? for help                    
Loaded GHCi configuration from /home/rgscott/.ghci                                        
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )                               
                                                                                          
Bug.hs:1328:59: error:                                                                    
    • Couldn't match type ‘c69895866216793215480’ with ‘[a_a337f]’                        
        ‘c69895866216793215480’ is untouchable                                            
          inside the constraints: (arg_a33hh ~ xs_a33fp, arg_a33hi ~ r_a33fq)             
          bound by the type signature for:                                                
                     lambda_a33iH :: forall (xs_a33fp :: [a_a337f]) (r_a33fq :: [[a_a337f]]).
                                     (arg_a33hh ~ xs_a33fp, arg_a33hi ~ r_a33fq) =>       
                                     Sing [a_a337f] xs_a33fp                              
                                     -> Sing [[a_a337f]] r_a33fq                          
                                     -> Sing                                              
                                          [[a_a337f]]
                                          (Apply
                                             [[a_a337f]]
                                             [[a_a337f]]
                                             (Apply
                                                [a_a337f]
                                                (TyFun [[a_a337f]] [[a_a337f]] -> *)
                                                (Let6989586621679736980InterleaveSym4
                                                   [a_a337f]
                                                   [a_a337f]
                                                   a_a337f
                                                   xs0_a33a0
                                                   t_a33aL
                                                   ts_a33aM
                                                   is_a33aO)
                                                arg_a33hh)
                                             arg_a33hi)
          at Bug.hs:(1289,35)-(1294,157)
      Expected type: Sing (TyFun [a_a337f] [a_a337f] -> *) t
                     -> Sing [a_a337f] t1
                     -> Sing [[a_a337f]] t2
                     -> Sing
                          ([a_a337f], [[a_a337f]])
                          ((@@)
                             [[a_a337f]]
                             ([a_a337f], [[a_a337f]])
                             ((@@)
                                [a_a337f]
                                ([[a_a337f]] ~> ([a_a337f], [[a_a337f]]))
                                ((@@)
                                   (TyFun [a_a337f] [a_a337f] -> *)
                                   ([a_a337f] ~> ([[a_a337f]] ~> ([a_a337f], [[a_a337f]])))
                                   (Let6989586621679736980Interleave'Sym4
                                      [a_a337f]
                                      [a_a337f]
                                      a_a337f
                                      [a_a337f]
                                      xs0_a33a0
                                      t_a33aL
                                      ts_a33aM
                                      is_a33aO)
                                   t)
                                t1)
                             t2)
        Actual type: Sing (TyFun [a_a337f] c69895866216793215480 -> *) t
                     -> Sing [a_a337f] t1
                     -> Sing [c69895866216793215480] t2
                     -> Sing
                          ([a_a337f], [c69895866216793215480])
                          (Apply
                             [c69895866216793215480]
                             ([a_a337f], [c69895866216793215480])
                             (Apply
                                [a_a337f]
                                ([c69895866216793215480] ~> ([a_a337f], [c69895866216793215480]))
                                (Apply
                                   (TyFun [a_a337f] c69895866216793215480 -> *)
                                   ([a_a337f]
                                    ~> ([c69895866216793215480]
                                        ~> ([a_a337f], [c69895866216793215480])))
                                   (Let6989586621679736980Interleave'Sym4
                                      [a_a337f]
                                      [a_a337f]
                                      a_a337f
                                      c69895866216793215480
                                      xs0_a33a0
                                      t_a33aL
                                      ts_a33aM
                                      is_a33aO)
                                   t)
                                t1)
                             t2)
    • In the second argument of ‘singFun3’, namely ‘sInterleave'’
      In the first argument of ‘applySing’, namely
        ‘((singFun3
             (Proxy ::
                Proxy (Let6989586621679736980Interleave'Sym4 xs0_a33a0 t_a33aL ts_a33aM is_a33aO)))
            sInterleave')’
      In the first argument of ‘applySing’, namely
        ‘((applySing
             ((singFun3
                 (Proxy ::
                    Proxy (Let6989586621679736980Interleave'Sym4 xs0_a33a0 t_a33aL ts_a33aM is_a33aO)))
                sInterleave'))
            ((singFun1 (Proxy :: Proxy IdSym0)) sId))’
    • Relevant bindings include
        sX_6989586621679737266 :: Sing
                                    ([a_a337f], [[a_a337f]])
                                    (Let6989586621679737265X_6989586621679737266Sym6
                                       [a_a337f]
                                       [a_a337f]
                                       a_a337f
                                       xs0_a33a0
                                       t_a33aL
                                       ts_a33aM
                                       is_a33aO
                                       xs_a33fp
                                       r_a33fq)
          (bound at Bug.hs:1321:41)
        r_a33iK :: Sing [[a_a337f]] r_a33fq (bound at Bug.hs:1295:57)
        xs_a33iJ :: Sing [a_a337f] xs_a33fp (bound at Bug.hs:1295:48)
        lambda_a33iH :: Sing [a_a337f] xs_a33fp
                        -> Sing [[a_a337f]] r_a33fq
                        -> Sing
                             [[a_a337f]]
                             (Apply
                                [[a_a337f]]
                                [[a_a337f]]
                                (Apply
                                   [a_a337f]
                                   (TyFun [[a_a337f]] [[a_a337f]] -> *)
                                   (Let6989586621679736980InterleaveSym4
                                      [a_a337f]
                                      [a_a337f]
                                      a_a337f
                                      xs0_a33a0
                                      t_a33aL
                                      ts_a33aM
                                      is_a33aO)
                                   arg_a33hh)
                                arg_a33hi)
          (bound at Bug.hs:1295:35)
        sR :: Sing [[a_a337f]] arg_a33hi (bound at Bug.hs:1287:45)
        sXs :: Sing [a_a337f] arg_a33hh (bound at Bug.hs:1287:41)
        sInterleave' :: forall (arg_a33he :: TyFun
                                               [a_a337f] c69895866216793215480
                                             -> *) (arg_a33hf :: [a_a337f]) (arg_a33hg :: [c69895866216793215480]).
                        Sing (TyFun [a_a337f] c69895866216793215480 -> *) arg_a33he
                        -> Sing [a_a337f] arg_a33hf
                        -> Sing [c69895866216793215480] arg_a33hg
                        -> Sing
                             ([a_a337f], [c69895866216793215480])
                             (Apply
                                [c69895866216793215480]
                                ([a_a337f], [c69895866216793215480])
                                (Apply
                                   [a_a337f]
                                   ([c69895866216793215480] ~> ([a_a337f], [c69895866216793215480]))
                                   (Apply
                                      (TyFun [a_a337f] c69895866216793215480 -> *)
                                      ([a_a337f]
                                       ~> ([c69895866216793215480]
                                           ~> ([a_a337f], [c69895866216793215480])))
                                      (Let6989586621679736980Interleave'Sym4
                                         [a_a337f]
                                         [a_a337f]
                                         a_a337f
                                         c69895866216793215480
                                         xs0_a33a0
                                         t_a33aL
                                         ts_a33aM
                                         is_a33aO)
                                      arg_a33he)
                                   arg_a33hf)
                                arg_a33hg)
          (bound at Bug.hs:1166:29)
        lambda_a33ha :: Sing a_a337f t_a33aL
                        -> Sing [a_a337f] ts_a33aM
                        -> Sing [a_a337f] is_a33aO
                        -> Sing
                             [[a_a337f]]
                             (Apply
                                [a_a337f]
                                [[a_a337f]]
                                (Apply
                                   [a_a337f]
                                   ([a_a337f] ~> [[a_a337f]])
                                   (Let6989586621679736931PermsSym1 a_a337f xs0_a33a0)
                                   arg_a33h0)
                                arg_a33h1)
          (bound at Bug.hs:1153:23)
        sTs :: Sing [a_a337f] n_a1kQd (bound at Bug.hs:1143:34)
        sT :: Sing a_a337f n_a1kQc (bound at Bug.hs:1143:31)
        lambda_a33gY :: Sing [a_a337f] xs0_a33a0
                        -> Sing
                             [[a_a337f]]
                             (Apply [a_a337f] [[a_a337f]] (PermutationsSym0 a_a337f) t_a33gX)
          (bound at Bug.hs:1127:11)
        (Some bindings suppressed; use -fmax-relevant-binds=N or -fno-max-relevant-binds)
     |
1328 |                                                           sInterleave'))
     |                                                           ^^^^^^^^^^^^

Bug.hs:1328:59: error:
    • Could not deduce: (Let6989586621679736980Interleave'
                           [a_a337f]
                           [a_a337f]
                           a_a337f
                           c69895866216793215480
                           xs0_a33a0
                           t_a33aL
                           ts_a33aM
                           is_a33aO
                           t
                           t1
                           t2 :: ([a_a337f], [c69895866216793215480]))
                        ~~
                        (Let6989586621679736980Interleave'
                           [a_a337f]
                           [a_a337f]
                           a_a337f
                           [a_a337f]
                           xs0_a33a0
                           t_a33aL
                           ts_a33aM
                           is_a33aO
                           t
                           t1
                           t2 :: ([a_a337f], [c69895866216793215480]))
      from the context: t_a33gX ~ xs0_a33a0
        bound by the type signature for:
                   lambda_a33gY :: forall (xs0_a33a0 :: [a_a337f]).
                                   t_a33gX ~ xs0_a33a0 =>
                                   Sing [a_a337f] xs0_a33a0
                                   -> Sing
                                        [[a_a337f]]
                                        (Apply
                                           [a_a337f] [[a_a337f]] (PermutationsSym0 a_a337f) t_a33gX)
        at Bug.hs:(1122,11)-(1126,67)
      or from: arg_a33h0 ~ (':) a_a337f n_a1kQc n_a1kQd
        bound by a pattern with constructor:
                   SCons :: forall a_11 (z_a1kQb :: [a_11]) (n_a1kQc :: a_11) (n_a1kQd :: [a_11]).
                            z_a1kQb ~ (':) a_11 n_a1kQc n_a1kQd =>
                            Sing a_11 n_a1kQc -> Sing [a_11] n_a1kQd -> Sing [a_11] z_a1kQb,
                 in an equation for ‘sPerms’
        at Bug.hs:1143:25-36
      or from: (arg_a33h0
                ~
                Apply
                  [a_a337f]
                  [a_a337f]
                  (Apply
                     a_a337f (TyFun [a_a337f] [a_a337f] -> *) ((:$) a_a337f) t_a33aL)
                  ts_a33aM,
                arg_a33h1 ~ is_a33aO)
        bound by the type signature for:
                   lambda_a33ha :: forall (t_a33aL :: a_a337f) (ts_a33aM :: [a_a337f]) (is_a33aO :: [a_a337f]).
                                   (arg_a33h0
                                    ~
                                    Apply
                                      [a_a337f]
                                      [a_a337f]
                                      (Apply
                                         a_a337f
                                         (TyFun [a_a337f] [a_a337f] -> *)
                                         ((:$) a_a337f)
                                         t_a33aL)
                                      ts_a33aM,
                                    arg_a33h1 ~ is_a33aO) =>
                                   Sing a_a337f t_a33aL
                                   -> Sing [a_a337f] ts_a33aM
                                   -> Sing [a_a337f] is_a33aO
                                   -> Sing
                                        [[a_a337f]]
                                        (Apply
                                           [a_a337f]
                                           [[a_a337f]]
                                           (Apply
                                              [a_a337f]
                                              ([a_a337f] ~> [[a_a337f]])
                                              (Let6989586621679736931PermsSym1 a_a337f xs0_a33a0)
                                              arg_a33h0)
                                           arg_a33h1)
        at Bug.hs:(1145,23)-(1152,117)
      or from: (arg_a33hh ~ xs_a33fp, arg_a33hi ~ r_a33fq)
        bound by the type signature for:
                   lambda_a33iH :: forall (xs_a33fp :: [a_a337f]) (r_a33fq :: [[a_a337f]]).
                                   (arg_a33hh ~ xs_a33fp, arg_a33hi ~ r_a33fq) =>
                                   Sing [a_a337f] xs_a33fp
                                   -> Sing [[a_a337f]] r_a33fq
                                   -> Sing
                                        [[a_a337f]]
                                        (Apply
                                           [[a_a337f]]
                                           [[a_a337f]]
                                           (Apply
                                              [a_a337f]
                                              (TyFun [[a_a337f]] [[a_a337f]] -> *)
                                              (Let6989586621679736980InterleaveSym4
                                                 [a_a337f]
                                                 [a_a337f]
                                                 a_a337f
                                                 xs0_a33a0
                                                 t_a33aL
                                                 ts_a33aM
                                                 is_a33aO)
                                              arg_a33hh)
                                           arg_a33hi)
        at Bug.hs:(1289,35)-(1294,157)
      Expected type: Sing (TyFun [a_a337f] [a_a337f] -> *) t
                     -> Sing [a_a337f] t1
                     -> Sing [[a_a337f]] t2
                     -> Sing
                          ([a_a337f], [[a_a337f]])
                          ((@@)
                             [[a_a337f]]
                             ([a_a337f], [[a_a337f]])
                             ((@@)
                                [a_a337f]
                                ([[a_a337f]] ~> ([a_a337f], [[a_a337f]]))
                                ((@@)
                                   (TyFun [a_a337f] [a_a337f] -> *)
                                   ([a_a337f] ~> ([[a_a337f]] ~> ([a_a337f], [[a_a337f]])))
                                   (Let6989586621679736980Interleave'Sym4
                                      [a_a337f]
                                      [a_a337f]
                                      a_a337f
                                      [a_a337f]
                                      xs0_a33a0
                                      t_a33aL
                                      ts_a33aM
                                      is_a33aO)
                                   t)
                                t1)
                             t2)
        Actual type: Sing (TyFun [a_a337f] c69895866216793215480 -> *) t
                     -> Sing [a_a337f] t1
                     -> Sing [c69895866216793215480] t2
                     -> Sing
                          ([a_a337f], [c69895866216793215480])
                          (Apply
                             [c69895866216793215480]
                             ([a_a337f], [c69895866216793215480])
                             (Apply
                                [a_a337f]
                                ([c69895866216793215480] ~> ([a_a337f], [c69895866216793215480]))
                                (Apply
                                   (TyFun [a_a337f] c69895866216793215480 -> *)
                                   ([a_a337f]
                                    ~> ([c69895866216793215480]
                                        ~> ([a_a337f], [c69895866216793215480])))
                                   (Let6989586621679736980Interleave'Sym4
                                      [a_a337f]
                                      [a_a337f]
                                      a_a337f
                                      c69895866216793215480
                                      xs0_a33a0
                                      t_a33aL
                                      ts_a33aM
                                      is_a33aO)
                                   t)
                                t1)
                             t2)
      The type variable ‘c69895866216793215480’ is ambiguous
    • In the second argument of ‘singFun3’, namely ‘sInterleave'’
      In the first argument of ‘applySing’, namely
        ‘((singFun3
             (Proxy ::
                Proxy (Let6989586621679736980Interleave'Sym4 xs0_a33a0 t_a33aL ts_a33aM is_a33aO)))
            sInterleave')’
      In the first argument of ‘applySing’, namely
        ‘((applySing
             ((singFun3
                 (Proxy ::
                    Proxy (Let6989586621679736980Interleave'Sym4 xs0_a33a0 t_a33aL ts_a33aM is_a33aO)))
                sInterleave'))
            ((singFun1 (Proxy :: Proxy IdSym0)) sId))’
    • Relevant bindings include
        sX_6989586621679737266 :: Sing
                                    ([a_a337f], [[a_a337f]])
                                    (Let6989586621679737265X_6989586621679737266Sym6
                                       [a_a337f]
                                       [a_a337f]
                                       a_a337f
                                       xs0_a33a0
                                       t_a33aL
                                       ts_a33aM
                                       is_a33aO
                                       xs_a33fp
                                       r_a33fq)
          (bound at Bug.hs:1321:41)
        r_a33iK :: Sing [[a_a337f]] r_a33fq (bound at Bug.hs:1295:57)
        xs_a33iJ :: Sing [a_a337f] xs_a33fp (bound at Bug.hs:1295:48)
        lambda_a33iH :: Sing [a_a337f] xs_a33fp
                        -> Sing [[a_a337f]] r_a33fq
                        -> Sing
                             [[a_a337f]]
                             (Apply
                                [[a_a337f]]
                                [[a_a337f]]
                                (Apply
                                   [a_a337f]
                                   (TyFun [[a_a337f]] [[a_a337f]] -> *)
                                   (Let6989586621679736980InterleaveSym4
                                      [a_a337f]
                                      [a_a337f]
                                      a_a337f
                                      xs0_a33a0
                                      t_a33aL
                                      ts_a33aM
                                      is_a33aO)
                                   arg_a33hh)
                                arg_a33hi)
          (bound at Bug.hs:1295:35)
        sR :: Sing [[a_a337f]] arg_a33hi (bound at Bug.hs:1287:45)
        sXs :: Sing [a_a337f] arg_a33hh (bound at Bug.hs:1287:41)
        sInterleave' :: forall (arg_a33he :: TyFun
                                               [a_a337f] c69895866216793215480
                                             -> *) (arg_a33hf :: [a_a337f]) (arg_a33hg :: [c69895866216793215480]).
                        Sing (TyFun [a_a337f] c69895866216793215480 -> *) arg_a33he
                        -> Sing [a_a337f] arg_a33hf
                        -> Sing [c69895866216793215480] arg_a33hg
                        -> Sing
                             ([a_a337f], [c69895866216793215480])
                             (Apply
                                [c69895866216793215480]
                                ([a_a337f], [c69895866216793215480])
                                (Apply
                                   [a_a337f]
                                   ([c69895866216793215480] ~> ([a_a337f], [c69895866216793215480]))
                                   (Apply
                                      (TyFun [a_a337f] c69895866216793215480 -> *)
                                      ([a_a337f]
                                       ~> ([c69895866216793215480]
                                           ~> ([a_a337f], [c69895866216793215480])))
                                      (Let6989586621679736980Interleave'Sym4
                                         [a_a337f]
                                         [a_a337f]
                                         a_a337f
                                         c69895866216793215480
                                         xs0_a33a0
                                         t_a33aL
                                         ts_a33aM
                                         is_a33aO)
                                      arg_a33he)
                                   arg_a33hf)
                                arg_a33hg)
          (bound at Bug.hs:1166:29)
        lambda_a33ha :: Sing a_a337f t_a33aL
                        -> Sing [a_a337f] ts_a33aM
                        -> Sing [a_a337f] is_a33aO
                        -> Sing
                             [[a_a337f]]
                             (Apply
                                [a_a337f]
                                [[a_a337f]]
                                (Apply
                                   [a_a337f]
                                   ([a_a337f] ~> [[a_a337f]])
                                   (Let6989586621679736931PermsSym1 a_a337f xs0_a33a0)
                                   arg_a33h0)
                                arg_a33h1)
          (bound at Bug.hs:1153:23)
        sTs :: Sing [a_a337f] n_a1kQd (bound at Bug.hs:1143:34)
        sT :: Sing a_a337f n_a1kQc (bound at Bug.hs:1143:31)
        lambda_a33gY :: Sing [a_a337f] xs0_a33a0
                        -> Sing
                             [[a_a337f]]
                             (Apply [a_a337f] [[a_a337f]] (PermutationsSym0 a_a337f) t_a33gX)
          (bound at Bug.hs:1127:11)
        (Some bindings suppressed; use -fmax-relevant-binds=N or -fno-max-relevant-binds)
     |
1328 |                                                           sInterleave'))
     |                                                           ^^^^^^^^^^^^

Attachments (3)

Bug.hs (87.4 KB) - added by RyanGlScott 4 months ago.
Bug2.hs (44.9 KB) - added by RyanGlScott 3 months ago.
Bug3.hs (8.8 KB) - added by RyanGlScott 3 months ago.

Download all attachments as: .zip

Change History (18)

Changed 4 months ago by RyanGlScott

Attachment: Bug.hs added

comment:1 Changed 4 months ago by RyanGlScott

Description: modified (diff)

comment:2 Changed 4 months ago by RyanGlScott

Commit 109a2429493c2a2d5481b67f5b0c1086a959813e caused this regression.

Richard, might you have an idea of what's going on here?

comment:3 Changed 4 months ago by RyanGlScott

Version: 8.0.18.1

comment:4 Changed 3 months ago by goldfire

I've no clue what's going on in that mess of code. Who would ever write such a thing? :)

But I figured this out: if we force do_kind_gen on line 208 of TcHsType to be True always, the module compiles. I've now got to run, but my hunch is that the calculation of when types are closed is a bit off.

Thanks for making an easy repro case and bisecting. That's invaluable!

Last edited 3 months ago by goldfire (previous) (diff)

comment:5 Changed 3 months ago by simonpj

Keywords: TypeInType added

comment:6 Changed 3 months ago by goldfire

Keywords: TypeInType removed

I believe this is a dup of #13555, which is a tractable example. So let's work on that ticket first.

comment:7 Changed 3 months ago by simonpj

Keywords: TypeInType added

Changed 3 months ago by RyanGlScott

Attachment: Bug2.hs added

comment:8 Changed 3 months ago by RyanGlScott

Update: I removed some cruft from the previous attached file, so now it's down to 633 lines (originally 1367).

Changed 3 months ago by RyanGlScott

Attachment: Bug3.hs added

comment:9 Changed 3 months ago by RyanGlScott

I pushed some more, and managed to get it down to 158 lines. And I think that's probably the limit of my ability to debug this :)

comment:10 in reply to:  9 Changed 3 months ago by RyanGlScott

Replying to 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:

  • Bug.hs

    diff --git a/Bug.hs b/Bug.hs
    index d534fe0..52163b8 100644
    a b src/Data/Singletons/Prelude/List.hs:(260,3)-(806,4): Splicing declar 
    11271127          lambda_a33gY xs0_a33gZ
    11281128            = let
    11291129                sPerms ::
    1130                   forall arg_a33h0 arg_a33h1.
     1130                  forall (arg_a33h0 :: [a_a337f]) arg_a33h1.
    11311131                  Sing arg_a33h0
    11321132                  -> Sing arg_a33h1
    11331133                     -> Sing (Apply (Apply (Let6989586621679736931PermsSym1 xs0_a33a0) ar
    src/Data/Singletons/Prelude/List.hs:(260,3)-(806,4): Splicing declar 
    11531153                      lambda_a33ha t_a33hb ts_a33hc is_a33hd
    11541154                        = let
    11551155                            sInterleave' ::
    1156                               forall arg_a33he arg_a33hf arg_a33hg.
     1156                              forall (arg_a33he :: TyFun [a_a337f] k -> Type) arg_a33hf a
    11571157                              Sing arg_a33he
    11581158                              -> Sing arg_a33hf
    11591159                                 -> Sing arg_a33hg
  • Bug2.hs

    diff --git a/Bug2.hs b/Bug2.hs
    index 98fbbf0..75c4523 100644
    a b src/Data/Singletons/Prelude/List.hs:(260,3)-(806,4): Splicing declarat 
    393393          lambda_a33gY xs0_a33gZ
    394394            = let
    395395                sPerms ::
    396                   forall arg_a33h0 arg_a33h1.
     396                  forall (arg_a33h0 :: [k]) arg_a33h1.
    397397                  Sing arg_a33h0
    398398                  -> Sing arg_a33h1
    399399                     -> Sing (Apply (Apply (Let6989586621679736931PermsSym1 xs0_a33a0) ar
    src/Data/Singletons/Prelude/List.hs:(260,3)-(806,4): Splicing declarat 
    419419                      lambda_a33ha t_a33hb ts_a33hc is_a33hd
    420420                        = let
    421421                            sInterleave' ::
    422                               forall arg_a33he arg_a33hf arg_a33hg.
     422                              forall (arg_a33he :: TyFun [k] j -> Type) arg_a33hf arg_a33
    423423                              Sing arg_a33he
    424424                              -> Sing arg_a33hf
    425425                                 -> Sing arg_a33hg
  • Bug3.hs

    diff --git a/Bug3.hs b/Bug3.hs
    index 77484b2..a286b43 100644
    a b lambda_a33gY _ 
    115115                  lambda_a33ha _ _ _
    116116                    = let
    117117                        sInterleave' ::
    118                           forall arg_a33he arg_a33hf arg_a33hg.
     118                          forall (arg_a33he :: TyFun [k] j -> Type) (arg_a33hf :: [y]) (arg_a33hg :: z).
    119119                          Sing arg_a33he
    120120                          -> Sing arg_a33hf
    121121                             -> 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?

comment:11 Changed 3 months ago by goldfire

I still think this is #13555. In all cases, the extra kind signatures mention kind variables, which GHC is now not generalizing.

What surprises me about this case is that no generalization should be necessary to compile the singled permutations. My best guess is that untouchable type variables induced by some GADT pattern matching prevent GHC from inferring the correct kinds of the functions. If their kinds are generalized, then all works out. But since they are not being generalized any more, we run into a problem.

I'm inclined to try to understand this as an infelicity in singletons, that it produces code that GHC can't infer the kinds of. I doubt singletons can fix the problem, but it would be nice to be able to characterize what exactly is the cause of the problem and then document the infelicity. In the meantime, I'd bet that adding a type annotation to perms and interleave in the Data.Singletons.Prelude.List implementation would allow singletons to compile. I'm happy to do the further digging, but not for a few weeks, I'm afraid.

comment:12 Changed 3 months ago by RyanGlScott

Milestone: 8.2.18.4.1
Priority: highnormal

You are correct that adding more type signatures to the where-bound functions of permutations (specifically, interleave') resolves the issue upstream in singletons. See https://github.com/goldfirere/singletons/pull/182. Given that there's a viable workaround, I'm going to reduce the priority of this ticket.

Last edited 3 months ago by RyanGlScott (previous) (diff)

comment:13 Changed 3 months ago by goldfire

Resolution: duplicate
Status: newclosed

I think I understand this now. This is a fundamental difference between inference for types and inference for kinds.

Here is the original, unsingletonized code in question:

permutations            :: [a] -> [[a]]
permutations xs0        =  xs0 : perms xs0 []
  where
    -- perms :: forall a. [a] -> [a] -> [[a]]
    perms []     _  = []
    perms (t:ts) is = foldr interleave (perms ts (t:is)) (permutations is)
      where -- interleave :: [a] -> [[a]] -> [[a]]
            interleave    xs     r = let (_,zs) = interleave' id xs r in zs

            -- interleave' :: ([a] -> [a]) -> [a] -> [[a]] -> ([a],[[a]])
            interleave' _ []     r = (ts, r)
            interleave' f (y:ys) r = let (us,zs) = interleave' (f . (y:)) ys r
                                     in  (y:us, f (t:y:us) : zs)

Note that the local function signatures are commented out. This code compiles, although if you uncomment the type signatures, you'd need ScopedTypeVariables.

Let's consider type-checking this with MonoLocalBinds on (that is, "let should not be generalized"). The body of interleave' mentions t, a variable that's not local to interleave'. Thus, according to MonoLocalBinds, its type should not be generalized. The problem is that the type cannot be fully figured out solely by looking at the definition of interleave': by the time type inference is done with interleave', we know only that its type looks like ([a1] -> a2) -> [a1] -> [a2] -> ([a1], [a2]). Later, we will learn that a2 is really [a1]. This is just fine for type inference, but it's bad for kind inference.

The problem is that when GHC sees a type signature x :: ty, it interprets ty independent of any definition or usage of x. After processing that statement, ty has been desugared and is set in stone -- including the kinds of any type variables in ty.

After singletonizing, the type of the singletonized version of interleave' will mention the type family Interleave', whose body is just like that of interleave'. This type family's kind will mention both a1 and a2, as it has no reason not to. So sInterleave' would also have to have a generalized kind for it all to work out. But with the improvement in decideKindGeneralisationPlan, this doesn't happen.

So, here is the characterization of the infelicity in singletons: if a local function's type would be different depending on the presence of MonoLocalBinds, then it needs a type signature in order for singletons to work. In the case of interleave', without MonoLocalBinds, a2 is quantified over, leading to a different type than it would have otherwise. (Note that the kind for the Interleave' type family is generalized, regardless of MonoLocalBinds.)

I'm fairly confident in this analysis. I'm going to close the ticket as a dup of #13555.

comment:14 Changed 3 months ago by simonpj

This is just fine for type inference, but it's bad for kind inference.

I don't understand this. With MonoLocalBinds we don't generalise and all is well, no?

So, here is the characterization of the infelicity in singletons: if a local function's type would be different depending on the presence of MonoLocalBinds, then it needs a type signature in order for singletons to work.

I don't understand this either. Could you give a small example?

Looking at the Bug3.hs it looks as if there is a type signature, generated by Template Haskell. Perhaps you are saying that this type signature is insufficiently kind-generalised? In which case shouldn't the TH code simply add the necessary kind generalisation?

I'm going to close the ticket as a dup of #13555.

But #13555's conclusion was "not a bug". So is this not a bug goo? If so what about the singletons library?

Very confused!

comment:15 Changed 3 months ago by goldfire

Here appears to be a smaller, digestible example:

{-# LANGUAGE TypeFamilies, TypeOperators, DataKinds, PolyKinds,
             GADTs, ScopedTypeVariables #-}

f :: [a] -> [a]
f [] = []
f [x] = [x]
f (x:y:zs) = g y zs
  where
    g _ bs = x : bs

type family F (as :: [a]) :: [a] where
  F '[] = '[]
  F '[x] = '[x]
  F (x:y:zs) = G x y zs

type family G x a bs where
  G x _ bs = x : bs

data family Sing (x :: k)

data instance Sing (x :: [a]) where
  SNil :: Sing '[]
  SCons :: Sing a -> Sing as -> Sing (a : as)
infixr 5 `SCons`

sF :: forall (p :: [a]). Sing p -> Sing (F p :: [a])
sF SNil = SNil
sF (SCons x SNil) = SCons x SNil
sF ((x :: Sing x) `SCons` y `SCons` zs) = sG y zs
  where
    sG :: forall b c. Sing b -> Sing c -> Sing (G x b c)
    sG _ bs = x `SCons` bs

Let's start by examining f and g, which are ordinary, Haskell98 functions. What's the inferred type of g? It depends on whether or not lets are generalized. In Haskell98 (i.e. NoMonoLocalBinds), g is inferred to have type forall b. b -> [a] -> [a]. With MonoLocalBinds, g is inferred to have type a -> [a] -> [a]. Both types allow f to type-check, and so the user won't notice this difference.

Now let's consider the translation of f and g to type families. g closes over the outer local variable x, so we must add x to G's parameter list (this is lambda lifting). Note that F gets a CUSK, derived from f's type signature. G gets no kind annotations, as g has no type annotation. GHC infers kind forall a b. a -> b -> [a] -> [a] for G. Note that, as G is not local, its kind is always generalized, regardless of MonoLocalBinds.

Finally, we consider the singletonized version of f and g. Note that the type variable bound in sF's type gets a kind signature, as does the result. sG gets a type signature, but no variables get kind signatures. (sG's type signature is entirely formulaic, given the singletons pattern.) The only way GHC can figure out the kinds of b and c is via their usage in the call to G. This tells GHC that c must have kind [a], but it gives no information about b, whose kind remains mysterious. In 8.0, GHC mistakenly quantified over the kind of b, leading to sG :: forall (b :: k) (c :: [a]). .... When sG is called on y :: a, it's specialized with [k |-> a] and all is well. However, now that kind generalization is working properly, GHC does not quantify over k and leaves it as a metavariable to be solved.

What puzzles me a bit now that I look at this is that k should be able to be solved in the no-generalization case: k is determined by the call sG y zs, where we can see that k := a is a good solution. But GHC reports k as untouchable at this point.... and I don't know why. There seems to be no equality constraints brought into scope between sG y zs and the introduction of k, so I don't know why it would be untouchable. I will examine again in due course.

Note: See TracTickets for help on using tickets.