#8503: New GeneralizedNewtypeDeriving check still isn't permissive enough -------------------------------------+------------------------------------ Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by goldfire): This is subtler than I thought. Let's take a simple case: {{{ class C m where meth :: m (m a) instance C Maybe where meth = Nothing newtype NT a = MkNT (Maybe a) deriving C }}} In the derived instance for `C NT`, we need this: {{{ $meth_C_NT = $meth_C_Maybe |> co where co :: forall (a :: *). Maybe (Maybe a) ~R# NT (NT a) }}} What is `co`? Ideally, it would be {{{ co = forall (a :: *). Sym NTCo:NT[0] (Sym NTCo:NT[0] <a>) }}} but that doesn't role-check! `NTCo:NT[0]` has type `NT ~R# Maybe`. But, to apply that coercion to another requires an `AppCo`, which in turn requires its second argument to have a nominal role. The underlying problem here is essentially that eta-reducing the newtype coercion loses information about the roles of its parameters. After all, if `Maybe`'s parameter were at a nominal role, then this deriving would be bogus. By eta-reducing, we're forgetting that `Maybe`'s parameter's role is other than nominal. What to do? One possible solution is to allow `AxiomInstCo` to be oversaturated, and then role information could be stored in an axiom (indeed, role information for all non-eta-reduced parameters is already there). This isn't a terrible plan, but perhaps it has further ramifications that I'm not currently seeing. -- Ticket URL: GHC The Glasgow Haskell Compiler

#8503: New GeneralizedNewtypeDeriving check still isn't permissive enough -------------------------------------+------------------------------------ Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by sweirich): Perhaps another option is to generalize TyConAppCo so that it allows the heads to differ as long as they are (representationally) equal and we have role information for each head. That's slightly more general than changing AxiomInstCo as you'd get transititivity... -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8503#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8503: New GeneralizedNewtypeDeriving check still isn't permissive enough -------------------------------------+------------------------------------ Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by sweirich): Simon, there is more to it than just "if you apply them to representationally-equal arguments you get representationally-equal types?" We need to also look at the roles of the parameters in the application. Consider this example: {{{ type family F a where F Moo = Char F _ = Int newtype T a = MkT (F a) newtype U a = MkU (T a) }}} So T and U are representationally equal, but their parameter has nominal role. That means that we can safely conclude {{{ T Moo ~/R U Moo }}} but it would *not* be safe to say {{{ T Moo ~/R U Int }}} because then we would have Char ~/R Int. That is why I was suggesting the change to TyConAppCo. We're not tracking the parameter roles in kinds, so the only place we can look for them is in the head of an application. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8503#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8503: New GeneralizedNewtypeDeriving check still isn't permissive enough -------------------------------------+------------------------------------ Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by goldfire): I agree with Stephanie -- the rule Simon was looking at in core-spec (Co_AppCo, p. 10) is that way for a good reason. Why eta-reduce? Because it allows for more lifting of newtype coercions, via the `Coercible` mechanism. For example, if we don't eta-reduce {{{ newtype NTMaybe a = MkNT (Maybe a) }}} then we couldn't derive, say `StateT Int NTMaybe a ~R StateT Int Maybe a`. So, we don't need eta-reduction as much as maybe we once did, but it's still useful. One other alternative is to have the cake and eat it too: a newtype declaration like the one for `NTMaybe` can create ''two'' axioms: one eta- reduced and one not. There would have to be some logic to choose which axiom to use, but this would allow for all the constructions that we might want. (Strawman implementation: always use the eta-reduced version, except in GND and in `Coercible` code where we need the extra role info.) I'm personally not a big fan of the generalization of `TyConAppCo`. Stephanie's proposal means that the `TyConAppCo` would have to store two `TyCon`s and a coercion between them, and all the code that thinks about `TyConAppCo`s would now have to consider the possibility that the two `TyCon`s are different. But, after all this, I still think I favor my original idea: allow oversaturated `AxiomInstCo`s, and store extra role information in `CoAxiom`s accordingly. Can we think of reasons why this is bad? We already allow oversaturated `TyConAppCo`s (in fact, we require them to be oversaturated, as a `TyConAppCo` can't be on the left of an `AppCo`). We would introduce a similar invariant between `AxiomInstCo` and `AppCo`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8503#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8503: New GeneralizedNewtypeDeriving check still isn't permissive enough -------------------------------------+------------------------------------ Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by goldfire): Hold the phone! There is an easier solution to the original problem! In my first comment, I wanted a coercion `co :: forall (a :: *). Maybe (Maybe a) ~R NTMaybe (NTMaybe a)`, and then I proposed a possible value of that type that was ill-roled. But, here is a well-roled value: {{{ co = co1 ; co2 co1 :: forall (a :: *). Maybe (Maybe a) ~R Maybe (NT a) co1 = forall (a :: *). Maybe (sym NTCo <a>_N) co2 :: forall (a :: *). Maybe (NT a) ~R NT (NT a) co2 = forall (a :: *). sym NTCo <NT a>_N }}} If we convert the pieces one at a time and then use transitivity, we're all OK. I remember battling against this problem over the summer. So, now we have a new question: how to get GHC to find this solution? Luckily, we happen to have a solver lying around that does just that: the `Coercible` mechanism. I imagine we could get the GND code to just call the `Coercible` code for each method. In fact, I considered this approach when improving the GND mechanism a few weeks ago, but thought it was overkill. My guess is that this would Just Work, when implemented. It might simplify the code a bit, too, but be somewhat less efficient (at compile time) at doing GND. I think this is reasonable. Taking the idea a bit further, what if the `Coercible` mechanism can't derive a coercion for a particular method? It would have to produce unsolved `Coercible` constraints... which we could just add to the constraints on the GND instance! This would allow more GND's to work than we had hoped for, such as this example: {{{ type family F a class C a where meth :: a -> F a type instance F Int = Bool class C Int where meth = (> 0) type instance F Age = Bool newtype Age = MkAge Int deriving C -- just works, no extra constraints because F Age = F Int type instance F [a] = a class C [a] where meth = head type instance F (List a) = Int newtype List a = MkL [a] deriving C -- this would create an instance with head "instance (Coercible a Int) => C (List a) where ..." }}} This all seems quite reasonable behavior, though we would want to make sure we don't produce constraints like `Coercible Int Bool`. Thoughts? Is this a good plan? We could always, as a first pass, implement GND in terms of `Coercible` and fail if there are any unsolved constraints, working for `C Age` above but not `C (List a)`. -- Ticket URL: GHC The Glasgow Haskell Compiler

#8503: New GeneralizedNewtypeDeriving check still isn't permissive enough -------------------------------------+------------------------------------ Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by goldfire): Posted this to ghc-devs. Realizing it makes more sense here: I've run up against a limitation of `Coercible` I'd like to know more about. Currently, the stage2 compiler on my branch fails to build because of the problem. In Module.lhs, there is this line: {{{ newtype PackageId = PId FastString deriving( Eq, Typeable ) }}} The deriving mechanism sensibly prefers to use the GND mechanism when it can, and it can (seemingly) for `Eq` here. But, I get this error: {{{ compiler/basicTypes/Module.lhs:297:46: No instance for (ghc-prim:GHC.Types.Coercible FastString PackageId) because ‛PackageId’ is a recursive type constuctor }}} This is curious, because `PackageId` is manifestly ''not'' recursive. A little poking around tells me that any datatype mentioned in a .hs-boot file is considered recursive. There is sense to this, but the error message sure is confusing. In any case, this opens up a broader issue: we want GND to work with recursive newtypes. For example: {{{ class C a where meth :: a instance C (Either a String) where meth = Right "" newtype RecNT = MkRecNT (Either RecNT String) deriving C }}} The above code works just fine in 7.6.3. But, if `Coercible` isn't allowed over recursive newtypes, then this wouldn't work if GND is implemented in terms of `coerce`. So, my question is: why have this restriction? And, if there is a good reason for it, it should probably be documented somewhere. I couldn't find mention of it in the user's guide or in the haddock docs. If we do keep this restriction, what to do about GND? Seems like this may kill the idea of implementing GND in terms of `coerce`, but that makes me sad. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8503#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8503: New GeneralizedNewtypeDeriving check still isn't permissive enough -------------------------------------+------------------------------------ Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by goldfire): Yuck. I'm leery of creating a way for the type-checker to loop without turning on `UndecidableInstances`. And, with the `R2` example that Simon gives, the newtype and the relevant type family instance might be in different modules, so detecting even so simple an infinite regress may be problematic. (And, note that the pieces on their own are innocent- looking.) I've also just looked at `Note [Recursive newtypes]` in !TcDeriv. This note explains why GND ''works'' for recursive newtypes. I repeat it here: {{{ Note [Recursive newtypes] ~~~~~~~~~~~~~~~~~~~~~~~~~ Newtype deriving works fine, even if the newtype is recursive. e.g. newtype S1 = S1 [T1 ()] newtype T1 a = T1 (StateT S1 IO a ) deriving( Monad ) Remember, too, that type families are curretly (conservatively) given a recursive flag, so this also allows newtype deriving to work for type famillies. We used to exclude recursive types, because we had a rather simple minded way of generating the instance decl: newtype A = MkA [A] instance Eq [A] => Eq A -- Makes typechecker loop! But now we require a simple context, so it's ok. }}} I'm confused by the last line. In the code above the note, a context is generated that includes, for this example, `Eq [A]`! Where does the loop get broken? Regardless, here's a possible solution: if `Coercible` over recursive newtypes is sound but otherwise in danger of causing a loop, we could just require `UndecidableInstances` to get the `Coercible` mechanism to go down this road. In this scenario, my example (with `RecNT`) would fail to use GND without `UndecidableInstances` but should succeed with it. We can even give a helpful error message in this scenario. Or, perhaps even better: could the `Coercible` mechanism use `TyCon.checkRecTc`? That function seems to be designed for exactly this scenario, which is where we need to do newtype expansion but don't want to fall into a black hole. That might complicate the `Coercible` code, but I think it would be a step in the right direction. We could still allow users to specify `UndecidableInstances` to bypass even this check... but my guess is that `checkRecTc` would work exactly in the correct cases, meaning that bypassing the check is sure to cause the type-checker to loop. Other, more informed opinions are very welcome here. Lastly, is there a solid reason to require that the recursiveness of a type in a hs-boot file and the recursiveness of the real type are the same? It looks to me that it would be sound to assume types in hs-boot files are recursive, but then not to inherit this trait when processing the real thing. That would fix the problem with compiling Module.lhs, and it would save some embarrassment if we were to suggest `UndecidableInstances` to compile a very ordinary-looking newtype! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8503#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8503: New GeneralizedNewtypeDeriving check still isn't permissive enough -------------------------------------+------------------------------------ Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by nomeata): Using just `TyCon.checkRecTc` is too permissive for `Coercible`. `checkRecTc` succeeds for `Fix (Either x)` (where `newtype Fix f = MkFix (f (Fix f))`) for all type `x`. But then we’d generate the instances {{{ instance Coercible (Either x (Fix (Either x))) b => Coercible (Fix (Either x)) b instance Coercible a (Either x (Fix (Either x))) => Coercible a (Fix (Either x)) }}} so trying to solve the constraint `Coercible (Fix (Either Age)) (Fix (Either Int))` will loop. (With the current implementation, which hooks into the general constraint resolving, I’d expect it to not loop at compile time, but create a diverging witness, and crash at run time. Neither of these are desired). Now what about your example, `newtype RecNT = MkRecNT (Either RecNT String)`. Assume that `Coercible` would work for it, and assume there is also `newtype RecNT2 = MkRecNT2 (Either RecNT2 String)`. Then, similarly, solving `Coercible RecNT RecNT2` will loop with the current implementation... So it is not a matter of relaxing the checks; if we want to support recursive newtypes in `Coercible`, the algorithm needs to be generally overhauled. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8503#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8503: New GeneralizedNewtypeDeriving check still isn't permissive enough -------------------------------------+------------------------------------ Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Changes (by simonpj): * cc: diatchki (added) Comment: Let's note that even with `Fix` there is a legitimate and useful coercion `Coercible (Fix (Either x)) (Either x (Fix (Either x)))`. We can write it by hand, and you might want to get from the `Fix` form to the `Either` form. So the same instance declaration may terminate when solving some constraints, but not for others. The constraint solver already stores a "depth" in each constraint. The depth is incremented by 1 each time you use an instance declaration. For example, when you use `instance Eq a => Eq [a]` to solve `d1:Eq [Int]`, by reducing it to `d2:Eq Int`, then `d2` has a depth one greater than `d1`. Since such instance declarations remove a type constructor, a deep recursion implies a deeply nested type, like `[[[[[[Int]]]]]`. So (proposal) maybe we can simply depth-bound the solver. In fact it already is; this is the `-fcontext-stack` flag. (Actually, in fact I fear that we may instead construct a recursive dictionary instead, which we probably do not want for newtypes, though we do for data types, because we'll see a constraint we have already solved. See [http://research.microsoft.com/en- us/um/people/simonpj/papers/hmap/index.htm Scrap your boilerplate with class] for why we want recursive dictionaries.) Here is one other idea. Suppose we have the wanted constraint `Coercible [alpha] [Int]`. Should we use the `Coercible a b => Coercible [a] [b]` instance to solve it? Well, if it turns out that `alpha` (a unification variable) ultimately is `Int`, then doing so would not be wrong, but it would be a waste because the identity coercion will do the job. So maybe this is a bit like the `Equal` type family in the [http://research.microsoft.com/~simonpj/papers/ext-f Closed type families] paper: we should not do the list/list reduction unless the argument types are "apart" (in the terminology of the paper). But that would be too strong. Consider {{{ f :: Coercible a b => [a] -> [b] f x = coerce x }}} This should work, but it requires use of that list/list instance, and we don't know that `a` and `b` are un-equal. It's just that in this context we can treat `a` and `b` as skolems and hence "apart" for this purpose. Except, even then it's not quite right: we could have {{{ f :: (a~b, Coercible a b) => [a] -> [b] }}} and now `a` and `b` are provably equal. (Or some GADT version thereof.) So I think we probably need the depth-bound thing too. Do any of these ideas make sense to you guys? I'll add Iavor to the cc list. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8503#comment:17 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8503: New GeneralizedNewtypeDeriving check still isn't permissive enough -------------------------------------+------------------------------------ Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by simonpj): I discussed with Joachim. The "apartness" idea definitely doesn't work. Consider {{{ newtype Fix1 x = F1 (x (Fix1 x)) newtype Fix2 x = F2 (x (Fix2 x)) }}} and try solving `Coercible (Fix1 (Either Age)) (Fix2 (Either Int))`. Everything is fully known, and always apart, yet we get a loop. Moreover, analysing the definitions to find loop breakers (as GHC does now) fails in the presence of type functions {{{ newtype Bad a = B (F a) type instance F Int = Bad Int }}} Conclusion: the depth-bound idea is the only real option. We also need to prevent the construction of recursive dictionaries, but we can use the depth of a constraint to stop that too; do not solve a constraint of depth n by using a constraint of lower depth. This is rather conservative, but it's enough to prevent recursive dictionary construction. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8503#comment:19 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8503: New GeneralizedNewtypeDeriving check still isn't permissive enough -------------------------------------+------------------------------------ Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: #8541 -------------------------------------+------------------------------------ Comment (by goldfire): Yes, the depth-bound seems sensible and is probably the only real solution to this problem. We should be aware of a particularly nasty case, like this: {{{ Coercible (Maybe (Fix Maybe)) (Fix Maybe) }}} This should be solvable (and I posit that more sensible cases might come up in practice). The current algorithm simplifies the left-hand type (LHT) as far as it can, then simplifies the right-hand type (RHT) as far as it can. I would worry that the depth would hit its maximum when reducing the LHT and then refuse to simplify the RHT. Even if we tracked depths separately for the two sides, the right side would hit the maximum depth right before the two sides unify, leading to failure, no matter what the depth is! Note that if we just switch the order of the arguments to `Coercible`, this goal is easy to solve, after one reduction on the LHT. Having the solubility of a symmetric constraint depend on the order of arguments is undesirable. I have no good ideas of how to fix this, at the moment. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8503#comment:21 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8503: New GeneralizedNewtypeDeriving check still isn't permissive enough -------------------------------------+------------------------------------ Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: #8541 -------------------------------------+------------------------------------ Comment (by nomeata): Breaking out the individual problems into separate tickets: #8543 for recursive newtypes. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8503#comment:23 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8503: New GeneralizedNewtypeDeriving check still isn't permissive enough -------------------------------------+------------------------------------ Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: #8541 -------------------------------------+------------------------------------ Comment (by nomeata): Hehe, we got a race condition (see #8543), but thanks to purity, the result is equivalent :-) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8503#comment:25 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8503: New GeneralizedNewtypeDeriving check still isn't permissive enough -------------------------------------+------------------------------------ Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: #8541 -------------------------------------+------------------------------------ Comment (by nomeata): I have something that is roughly working, enough to notice problems. While it successfully prevents `Coercible Fix (Either Int)` from looping or generating recursive dictionaries, it does not help a lot against {{{ newtype Void a = Void (Void (a,a)) foo5 = coerce :: Void () -> () }}} Even with a depth of 20, this filly up my memory quickly, especially trying to print the final constraint. Do we have to live with the fact that there will likely always be ways to make the compiler use too many resources? Or should coercing recursive newtypes require `UndecidableInstances` to be enabled? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8503#comment:27 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8503: New GeneralizedNewtypeDeriving check still isn't permissive enough -------------------------------------+------------------------------------ Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: #8541 -------------------------------------+------------------------------------ Comment (by nomeata): Got that code in a working form. I don’t claim to know the solver well enough to be completely certain that there is not a way left to create a recursive dictionary, but at least the examples that I tried worked. Commits 6f5c183cb798a5d5e1011417f1f211834e4e9215 (GHC) and ec83ce7530af5474a3ad49d7120913c7f22266f0 (testsuite); for convenience, here is the note describing the design: {{{ Note [Preventing recursive dictionaries] We have some classes where it is not very useful to build recursive dictionaries (Coercible, at the moment). So we need the constraint solver to prevent that. We conservativey ensure this property using the subgoal depth of the constraints: When solving a Coercible constraint at depth d, we do not consider evicence from a depth <= d as suitable. Therefore we need to record the minimum depth allowed to solve a CtWanted. This is done in the SubGoalDepth field of CtWanted. Most code now uses mkCtWanted, which initializes it to initialSubGoalDepth (i.e. 0); but when requesting a Coercible instance (requestCoercible in TcInteract), we bump the current depth by one and use that. There are two spots where wanted contraints attempted to be solved using existing constraints; doTopReactDict in TcInteract (in the general solver) and newWantedEvVarNonrec (only used by requestCoercible) in TcSMonad. Both use ctEvCheckDepth to make the check. That function ensures that a Given constraint can always be used to solve a goal (i.e. they are at depth infinity, for our purposes) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8503#comment:29 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8503: New GeneralizedNewtypeDeriving check still isn't permissive enough -------------------------------------+------------------------------------ Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: 8548 Blocking: | Related Tickets: #8541 -------------------------------------+------------------------------------ Changes (by nomeata): * blockedby: => 8548 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8503#comment:31 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8503: New GeneralizedNewtypeDeriving check still isn't permissive enough -------------------------------------+------------------------------------ Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: 8548 Blocking: | Related Tickets: #8541 -------------------------------------+------------------------------------ Comment (by goldfire): I think the issue with #2850 is fixable. See that ticket. I actually think these knock-on effects of the GND-via-coerce decision are good. They're forcing us to get `Coercible` right! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8503#comment:33 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8503: New GeneralizedNewtypeDeriving check still isn't permissive enough -------------------------------------+------------------------------------ Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: 8548 Blocking: | Related Tickets: #8541 -------------------------------------+------------------------------------ Comment (by nomeata): Replying to [comment:9 goldfire]:

Hold the phone! There is an easier solution to the original problem!

\[..\]

Thoughts? Is this a good plan? We could always, as a first pass, implement GND in terms of `Coercible` and fail if there are any unsolved constraints, working for `C Age` above but not `C (List a)`.

I’ve been trying to get your attempt to work. It works for a lot of easy cases, and it works in theory, but there is an implementational difficulty with extra type variables in the instance. Consider: {{{ import GHC.Exts class Cls a where meth :: a newtype Id m = Id m deriving Cls }}} The instance we want to generate is {{{ instance forall m. Cls m => Cls (Id m) where meth = coerce (meth :: m) :: Id m }}} But that will require `ScopedTypeVariables`. Question one: Can I generate code at `TcGenDeriv` stage that uses scoped type variables, without requiring that extension to be enabled in the whole module? Next problem: Currently the code produces {{{ ==================== Derived instances ==================== Derived instances: instance T3423.Cls m_ayI => T3423.Cls (T3423.Id m_ayI) where T3423.meth = GHC.Prim.coerce (T3423.meth :: m_ayI) :: T3423.Id m_ayI }}} so there is no `forall` in the instance head. For `newtype ... deriving Cls` it might be possible to add that (although I did not yet find where), but the user should be able to specify {{{ deriving instance Cls m => Cls (Id m) }}} without having to add `forall m.`. I’m not sure what to do here. It would be best if we could generate code that works without having to specify types in the method definition at all, maybe using something like `$ClsId = case $superClassDict of D:Cls meth => D:Cls (coerce meth)`, but I do not see how `$superClassDict` should look like. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8503#comment:35 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8503: New GeneralizedNewtypeDeriving check still isn't permissive enough -------------------------------------+------------------------------------ Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: 8548 Blocking: | Related Tickets: #8541 -------------------------------------+------------------------------------ Comment (by Joachim Breitner ): In [changeset:"6468beebcf2b3a2dd9cbedd7b6dc9c7adaee626b/testsuite"]: {{{ #!CommitTicketReference repository="testsuite" revision="6468beebcf2b3a2dd9cbedd7b6dc9c7adaee626b" Add test cases for Coercing recursive newtypes (#8503) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8503#comment:39 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8503: New GeneralizedNewtypeDeriving check still isn't permissive enough -------------------------------------+------------------------------------ Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: 8548 Blocking: | Related Tickets: #8541 -------------------------------------+------------------------------------ Comment (by nomeata): Ok, pushed. Closing this ticket (is is far too long anyways, and trac spends too much time generating it), so any new issues with `Coercible` or GND please in new tickets. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8503#comment:41 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler