[GHC] #13549: GHC 8.2.1's typechecker rejects code generated by singletons that 8.0 accepts
#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 | Version: 8.0.1 (Type checker) | Keywords: | 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: -------------------------------------+------------------------------------- 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 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 xs_a33fp -> Sing r_a33fq -> Sing (Apply (Apply (Let6989586621679736980InterleaveSym4 xs0_a33a0 t_a33aL ts_a33aM is_a33aO) arg_a33hh) arg_a33hi) at Bug.hs:(1289,35)-(1294,157) Expected type: Sing t -> Sing t1 -> Sing t2 -> Sing (((Let6989586621679736980Interleave'Sym4 xs0_a33a0 t_a33aL ts_a33aM is_a33aO @@ t) @@ t1) @@ t2) Actual type: Sing t -> Sing t1 -> Sing t2 -> Sing (Apply (Apply (Apply (Let6989586621679736980Interleave'Sym4 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 (Let6989586621679737265X_6989586621679737266Sym6 xs0_a33a0 t_a33aL ts_a33aM is_a33aO xs_a33fp r_a33fq) (bound at Bug.hs:1321:41) r_a33iK :: Sing r_a33fq (bound at Bug.hs:1295:57) xs_a33iJ :: Sing xs_a33fp (bound at Bug.hs:1295:48) lambda_a33iH :: Sing xs_a33fp -> Sing r_a33fq -> Sing (Apply (Apply (Let6989586621679736980InterleaveSym4 xs0_a33a0 t_a33aL ts_a33aM is_a33aO) arg_a33hh) arg_a33hi) (bound at Bug.hs:1295:35) sR :: Sing arg_a33hi (bound at Bug.hs:1287:45) sXs :: Sing arg_a33hh (bound at Bug.hs:1287:41) sInterleave' :: forall (arg_a33he :: TyFun [a_a337f] c69895866216793215480 -> *) (arg_a33hf :: [a_a337f]) (arg_a33hg :: [c69895866216793215480]). Sing arg_a33he -> Sing arg_a33hf -> Sing arg_a33hg -> Sing (Apply (Apply (Apply (Let6989586621679736980Interleave'Sym4 xs0_a33a0 t_a33aL ts_a33aM is_a33aO) arg_a33he) arg_a33hf) arg_a33hg) (bound at Bug.hs:1166:29) lambda_a33ha :: Sing t_a33aL -> Sing ts_a33aM -> Sing is_a33aO -> Sing (Apply (Apply (Let6989586621679736931PermsSym1 xs0_a33a0) arg_a33h0) arg_a33h1) (bound at Bug.hs:1153:23) sTs :: Sing n_a1kQd (bound at Bug.hs:1143:34) sT :: Sing n_a1kQc (bound at Bug.hs:1143:31) lambda_a33gY :: Sing xs0_a33a0 -> Sing (Apply PermutationsSym0 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' xs0_a33a0 t_a33aL ts_a33aM is_a33aO t t1 t2 ~ Let6989586621679736980Interleave' xs0_a33a0 t_a33aL ts_a33aM is_a33aO t t1 t2 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 xs0_a33a0 -> Sing (Apply PermutationsSym0 t_a33gX) at Bug.hs:(1122,11)-(1126,67) or from: arg_a33h0 ~ (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 ~ (n_a1kQc : n_a1kQd) => Sing n_a1kQc -> Sing n_a1kQd -> Sing z_a1kQb, in an equation for ‘sPerms’ at Bug.hs:1143:25-36 or from: (arg_a33h0 ~ Apply (Apply (:$) 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 (Apply (:$) t_a33aL) ts_a33aM, arg_a33h1 ~ is_a33aO) => Sing t_a33aL -> Sing ts_a33aM -> Sing is_a33aO -> Sing (Apply (Apply (Let6989586621679736931PermsSym1 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 xs_a33fp -> Sing r_a33fq -> Sing (Apply (Apply (Let6989586621679736980InterleaveSym4 xs0_a33a0 t_a33aL ts_a33aM is_a33aO) arg_a33hh) arg_a33hi) at Bug.hs:(1289,35)-(1294,157) Expected type: Sing t -> Sing t1 -> Sing t2 -> Sing (((Let6989586621679736980Interleave'Sym4 xs0_a33a0 t_a33aL ts_a33aM is_a33aO @@ t) @@ t1) @@ t2) Actual type: Sing t -> Sing t1 -> Sing t2 -> Sing (Apply (Apply (Apply (Let6989586621679736980Interleave'Sym4 xs0_a33a0 t_a33aL ts_a33aM is_a33aO) t) t1) t2) The type variable ‘c69895866216793215480’ is ambiguous Use -fprint-explicit-kinds to see the kind arguments • 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 (Let6989586621679737265X_6989586621679737266Sym6 xs0_a33a0 t_a33aL ts_a33aM is_a33aO xs_a33fp r_a33fq) (bound at Bug.hs:1321:41) r_a33iK :: Sing r_a33fq (bound at Bug.hs:1295:57) xs_a33iJ :: Sing xs_a33fp (bound at Bug.hs:1295:48) lambda_a33iH :: Sing xs_a33fp -> Sing r_a33fq -> Sing (Apply (Apply (Let6989586621679736980InterleaveSym4 xs0_a33a0 t_a33aL ts_a33aM is_a33aO) arg_a33hh) arg_a33hi) (bound at Bug.hs:1295:35) sR :: Sing arg_a33hi (bound at Bug.hs:1287:45) sXs :: Sing arg_a33hh (bound at Bug.hs:1287:41) sInterleave' :: forall (arg_a33he :: TyFun [a_a337f] c69895866216793215480 -> *) (arg_a33hf :: [a_a337f]) (arg_a33hg :: [c69895866216793215480]). Sing arg_a33he -> Sing arg_a33hf -> Sing arg_a33hg -> Sing (Apply (Apply (Apply (Let6989586621679736980Interleave'Sym4 xs0_a33a0 t_a33aL ts_a33aM is_a33aO) arg_a33he) arg_a33hf) arg_a33hg) (bound at Bug.hs:1166:29) lambda_a33ha :: Sing t_a33aL -> Sing ts_a33aM -> Sing is_a33aO -> Sing (Apply (Apply (Let6989586621679736931PermsSym1 xs0_a33a0) arg_a33h0) arg_a33h1) (bound at Bug.hs:1153:23) sTs :: Sing n_a1kQd (bound at Bug.hs:1143:34) sT :: Sing n_a1kQc (bound at Bug.hs:1143:31) lambda_a33gY :: Sing xs0_a33a0 -> Sing (Apply PermutationsSym0 t_a33gX) (bound at Bug.hs:1127:11) (Some bindings suppressed; use -fmax-relevant-binds=N or -fno-max- relevant-binds) | 1328 | sInterleave')) | ^^^^^^^^^^^^ }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13549 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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.0.1 checker) | Resolution: | Keywords: 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: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * Attachment "Bug.hs" added. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13549 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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.0.1 checker) | Resolution: | Keywords: 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: | -------------------------------------+------------------------------------- Description changed by RyanGlScott: Old description:
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 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 xs_a33fp -> Sing r_a33fq -> Sing (Apply (Apply (Let6989586621679736980InterleaveSym4 xs0_a33a0 t_a33aL ts_a33aM is_a33aO) arg_a33hh) arg_a33hi) at Bug.hs:(1289,35)-(1294,157) Expected type: Sing t -> Sing t1 -> Sing t2 -> Sing (((Let6989586621679736980Interleave'Sym4 xs0_a33a0 t_a33aL ts_a33aM is_a33aO @@ t) @@ t1) @@ t2) Actual type: Sing t -> Sing t1 -> Sing t2 -> Sing (Apply (Apply (Apply (Let6989586621679736980Interleave'Sym4 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 (Let6989586621679737265X_6989586621679737266Sym6 xs0_a33a0 t_a33aL ts_a33aM is_a33aO xs_a33fp r_a33fq) (bound at Bug.hs:1321:41) r_a33iK :: Sing r_a33fq (bound at Bug.hs:1295:57) xs_a33iJ :: Sing xs_a33fp (bound at Bug.hs:1295:48) lambda_a33iH :: Sing xs_a33fp -> Sing r_a33fq -> Sing (Apply (Apply (Let6989586621679736980InterleaveSym4 xs0_a33a0 t_a33aL ts_a33aM is_a33aO) arg_a33hh) arg_a33hi) (bound at Bug.hs:1295:35) sR :: Sing arg_a33hi (bound at Bug.hs:1287:45) sXs :: Sing arg_a33hh (bound at Bug.hs:1287:41) sInterleave' :: forall (arg_a33he :: TyFun [a_a337f] c69895866216793215480 -> *) (arg_a33hf :: [a_a337f]) (arg_a33hg :: [c69895866216793215480]). Sing arg_a33he -> Sing arg_a33hf -> Sing arg_a33hg -> Sing (Apply (Apply (Apply (Let6989586621679736980Interleave'Sym4 xs0_a33a0 t_a33aL ts_a33aM is_a33aO) arg_a33he) arg_a33hf) arg_a33hg) (bound at Bug.hs:1166:29) lambda_a33ha :: Sing t_a33aL -> Sing ts_a33aM -> Sing is_a33aO -> Sing (Apply (Apply (Let6989586621679736931PermsSym1 xs0_a33a0) arg_a33h0) arg_a33h1) (bound at Bug.hs:1153:23) sTs :: Sing n_a1kQd (bound at Bug.hs:1143:34) sT :: Sing n_a1kQc (bound at Bug.hs:1143:31) lambda_a33gY :: Sing xs0_a33a0 -> Sing (Apply PermutationsSym0 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' xs0_a33a0 t_a33aL ts_a33aM is_a33aO t t1 t2 ~ Let6989586621679736980Interleave' xs0_a33a0 t_a33aL ts_a33aM is_a33aO t t1 t2 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 xs0_a33a0 -> Sing (Apply PermutationsSym0 t_a33gX) at Bug.hs:(1122,11)-(1126,67) or from: arg_a33h0 ~ (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 ~ (n_a1kQc : n_a1kQd) => Sing n_a1kQc -> Sing n_a1kQd -> Sing z_a1kQb, in an equation for ‘sPerms’ at Bug.hs:1143:25-36 or from: (arg_a33h0 ~ Apply (Apply (:$) 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 (Apply (:$) t_a33aL) ts_a33aM, arg_a33h1 ~ is_a33aO) => Sing t_a33aL -> Sing ts_a33aM -> Sing is_a33aO -> Sing (Apply (Apply (Let6989586621679736931PermsSym1 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 xs_a33fp -> Sing r_a33fq -> Sing (Apply (Apply (Let6989586621679736980InterleaveSym4 xs0_a33a0 t_a33aL ts_a33aM is_a33aO) arg_a33hh) arg_a33hi) at Bug.hs:(1289,35)-(1294,157) Expected type: Sing t -> Sing t1 -> Sing t2 -> Sing (((Let6989586621679736980Interleave'Sym4 xs0_a33a0 t_a33aL ts_a33aM is_a33aO @@ t) @@ t1) @@ t2) Actual type: Sing t -> Sing t1 -> Sing t2 -> Sing (Apply (Apply (Apply (Let6989586621679736980Interleave'Sym4 xs0_a33a0 t_a33aL ts_a33aM is_a33aO) t) t1) t2) The type variable ‘c69895866216793215480’ is ambiguous Use -fprint-explicit-kinds to see the kind arguments • 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 (Let6989586621679737265X_6989586621679737266Sym6 xs0_a33a0 t_a33aL ts_a33aM is_a33aO xs_a33fp r_a33fq) (bound at Bug.hs:1321:41) r_a33iK :: Sing r_a33fq (bound at Bug.hs:1295:57) xs_a33iJ :: Sing xs_a33fp (bound at Bug.hs:1295:48) lambda_a33iH :: Sing xs_a33fp -> Sing r_a33fq -> Sing (Apply (Apply (Let6989586621679736980InterleaveSym4 xs0_a33a0 t_a33aL ts_a33aM is_a33aO) arg_a33hh) arg_a33hi) (bound at Bug.hs:1295:35) sR :: Sing arg_a33hi (bound at Bug.hs:1287:45) sXs :: Sing arg_a33hh (bound at Bug.hs:1287:41) sInterleave' :: forall (arg_a33he :: TyFun [a_a337f] c69895866216793215480 -> *) (arg_a33hf :: [a_a337f]) (arg_a33hg :: [c69895866216793215480]). Sing arg_a33he -> Sing arg_a33hf -> Sing arg_a33hg -> Sing (Apply (Apply (Apply (Let6989586621679736980Interleave'Sym4 xs0_a33a0 t_a33aL ts_a33aM is_a33aO) arg_a33he) arg_a33hf) arg_a33hg) (bound at Bug.hs:1166:29) lambda_a33ha :: Sing t_a33aL -> Sing ts_a33aM -> Sing is_a33aO -> Sing (Apply (Apply (Let6989586621679736931PermsSym1 xs0_a33a0) arg_a33h0) arg_a33h1) (bound at Bug.hs:1153:23) sTs :: Sing n_a1kQd (bound at Bug.hs:1143:34) sT :: Sing n_a1kQc (bound at Bug.hs:1143:31) lambda_a33gY :: Sing xs0_a33a0 -> Sing (Apply PermutationsSym0 t_a33gX) (bound at Bug.hs:1127:11) (Some bindings suppressed; use -fmax-relevant-binds=N or -fno- max-relevant-binds) | 1328 | sInterleave')) | ^^^^^^^^^^^^ }}}
New description: 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')) | ^^^^^^^^^^^^ }}} -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13549#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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.0.1 checker) | Resolution: | Keywords: 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): Commit 109a2429493c2a2d5481b67f5b0c1086a959813e caused this regression. Richard, might you have an idea of what's going on here? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13549#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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: 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: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * version: 8.0.1 => 8.1 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13549#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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: 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 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 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! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13549#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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: | -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: => TypeInType -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13549#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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: 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: | -------------------------------------+------------------------------------- Changes (by goldfire): * keywords: TypeInType => Comment: I believe this is a dup of #13555, which is a tractable example. So let's work on that ticket first. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13549#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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: | -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: => TypeInType -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13549#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * Attachment "Bug2.hs" added. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13549 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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): Update: I removed some cruft from the previous attached file, so now it's down to 633 lines (originally 1367). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13549#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * Attachment "Bug3.hs" added. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13549 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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): 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 :) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13549#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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
#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 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13549#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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: normal | Milestone: 8.4.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: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * priority: high => normal * milestone: 8.2.1 => 8.4.1 Comment: You are correct that adding more type signatures to the `where`-bound functions of `permutations` (specifically, `interleave'`) resolves the issue upstream in `singletons`. Given that there's a viable workaround, I'm going to reduce the priority of this ticket. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13549#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13549: GHC 8.2.1's typechecker rejects code generated by singletons that 8.0 accepts -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.1 checker) | Resolution: duplicate | 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: | -------------------------------------+------------------------------------- Changes (by goldfire): * status: new => closed * resolution: => duplicate Comment: 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: {{{#!hs 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13549#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13549: GHC 8.2.1's typechecker rejects code generated by singletons that 8.0 accepts -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.1 checker) | Resolution: duplicate | 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 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! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13549#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13549: GHC 8.2.1's typechecker rejects code generated by singletons that 8.0 accepts -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.1 checker) | Resolution: duplicate | 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 goldfire): Here appears to be a smaller, digestible example: {{{#!hs {-# 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13549#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC