#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 )
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.1rc1 nor HEAD do. Here is the error message you get, in its full glory:
$ /opt/ghc/8.2.1/bin/ghci Bug.hs fprintexplicitkinds 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 fmaxrelevantbinds=N or fnomaxrelevantbinds)  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:2536 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 fmaxrelevantbinds=N or fnomaxrelevantbinds)  1328  sInterleave'))  ^^^^^^^^^^^^
Attachments (3)
Change History (18)
Changed 2 years ago by
comment:1 Changed 2 years ago by
Description:  modified (diff) 

comment:2 Changed 2 years ago by
comment:3 Changed 2 years ago by
Version:  8.0.1 → 8.1 

comment:4 Changed 2 years ago by
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!
comment:5 Changed 2 years ago by
Keywords:  TypeInType added 

comment:6 Changed 2 years ago by
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 2 years ago by
Keywords:  TypeInType added 

Changed 2 years ago by
comment:8 Changed 2 years ago by
Update: I removed some cruft from the previous attached file, so now it's down to 633 lines (originally 1367).
Changed 2 years ago by
comment:9 followup: 10 Changed 2 years ago by
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 Changed 2 years ago by
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 1127 1127 lambda_a33gY xs0_a33gZ 1128 1128 = let 1129 1129 sPerms :: 1130 forall arg_a33h0arg_a33h1.1130 forall (arg_a33h0 :: [a_a337f]) arg_a33h1. 1131 1131 Sing arg_a33h0 1132 1132 > Sing arg_a33h1 1133 1133 > Sing (Apply (Apply (Let6989586621679736931PermsSym1 xs0_a33a0) ar … … src/Data/Singletons/Prelude/List.hs:(260,3)(806,4): Splicing declar 1153 1153 lambda_a33ha t_a33hb ts_a33hc is_a33hd 1154 1154 = let 1155 1155 sInterleave' :: 1156 forall arg_a33he arg_a33hf arg_a33hg.1156 forall (arg_a33he :: TyFun [a_a337f] k > Type) arg_a33hf a 1157 1157 Sing arg_a33he 1158 1158 > Sing arg_a33hf 1159 1159 > 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 393 393 lambda_a33gY xs0_a33gZ 394 394 = let 395 395 sPerms :: 396 forall arg_a33h0arg_a33h1.396 forall (arg_a33h0 :: [k]) arg_a33h1. 397 397 Sing arg_a33h0 398 398 > Sing arg_a33h1 399 399 > Sing (Apply (Apply (Let6989586621679736931PermsSym1 xs0_a33a0) ar … … src/Data/Singletons/Prelude/List.hs:(260,3)(806,4): Splicing declarat 419 419 lambda_a33ha t_a33hb ts_a33hc is_a33hd 420 420 = let 421 421 sInterleave' :: 422 forall arg_a33he arg_a33hf arg_a33hg.422 forall (arg_a33he :: TyFun [k] j > Type) arg_a33hf arg_a33 423 423 Sing arg_a33he 424 424 > Sing arg_a33hf 425 425 > Sing arg_a33hg

Bug3.hs
diff git a/Bug3.hs b/Bug3.hs index 77484b2..a286b43 100644
a b lambda_a33gY _ 115 115 lambda_a33ha _ _ _ 116 116 = let 117 117 sInterleave' :: 118 forall arg_a33he arg_a33hf arg_a33hg.118 forall (arg_a33he :: TyFun [k] j > Type) (arg_a33hf :: [y]) (arg_a33hg :: z). 119 119 Sing arg_a33he 120 120 > Sing arg_a33hf 121 121 > 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 2 years ago by
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 2 years ago by
Milestone:  8.2.1 → 8.4.1 

Priority:  high → normal 
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.
comment:13 Changed 2 years ago by
Resolution:  → duplicate 

Status:  new → closed 
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 typechecking 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 2 years ago by
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 kindgeneralised? 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 2 years ago by
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 typecheck, 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 nogeneralization 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.
Commit 109a2429493c2a2d5481b67f5b0c1086a959813e caused this regression.
Richard, might you have an idea of what's going on here?