Opened 2 years ago

Last modified 18 months ago

#14292 new feature request

Coercing between constraints of newtypes

Reported by: Iceland_jack Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.2.1
Keywords: Roles Cc: adamgundry, vagarenko
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

This doesn't work

{-# Language ConstraintKinds #-}
{-# Language GADTs #-}

import Data.Coerce

newtype USD = USD Int

data Dict c where
  Dict :: c => Dict c

num :: Dict (Num Int) -> Dict (Num USD)
num = coerce

but this does

data NUM a = NUM (a -> a -> a)

num' :: NUM Int -> NUM USD
num' = coerce

is this a fundamental limitation?

Change History (11)

comment:1 Changed 2 years ago by RyanGlScott

I wouldn't say that this is rejected due to a fundamental limitation so much as a deliberate design choice. The immediate reason that the former program is rejected is due to roles. By default, all class parameters are given role nominal, so you can't coerce between Num a and Num b unless a ~ b.

Why is the case? Even if a and b are representationally equal, there's absolutely no guarantee that their corresponding Num dictionaries are also representationally equal. After all, a Num instance for USD might do something crazy like fromInteger _ = USD 42. Defaulting class parameters to nominal is thus a conservative way to avoid the shenanigans that would unfold if you treated a Num USD dictionary as a Num Int one, or vice versa.

Now you might object: "But I'm a careful programmer! I promise to only use Num Int and Num USD dictionaries that are representationally equivalent!" In that case, there is a fallback mechanism in the form of IncoherentInstances:

{-# Language ConstraintKinds #-}
{-# Language GADTs #-}
{-# Language IncoherentInstances #-}
{-# Language RoleAnnotations #-}

import Data.Coerce
import Prelude hiding (Num(..))

newtype USD = USD Int

data Dict c where
  Dict :: c => Dict c

type role Num representational
class Num a where
  -- ...

instance Num Int
instance Num USD

num :: Dict (Num Int) -> Dict (Num USD)
num = coerce

I hope it should be obvious from the name IncoherentInstances alone that this fallback carries significant risks. Use this trick at your own discretion.

Does that answer the question satisfactorily? If so, please feel free to close the ticket.

comment:2 Changed 2 years ago by goldfire

Ryan is, as usual, spot on. The need for -XIncoherentInstances in Ryan's example was a deliberate design choice to discourage non-nominally roled classes. And the extension name is accurate: you're using instances in a fundamentally incoherent (but still type-safe) way.

comment:3 Changed 2 years ago by AntC

IncoherentInstances is a module-wide setting; and nowadays deprecated in favour of the more surgical {-# INCOHERENT #-} pragma on the instance.

Does that also apply for the role mungling?

How does the {-# INCOHERENT #-} pragma go for StandaloneDeriving or GeneralizedNewtypeDeriving? It seems to be accepted by GHC OK, does it have the right effect? (It's hard to put together a test case.)

(I'm asking because I've got a proposal in that will not play well with the module-wide setting. instance Num Int does not overlap instance Num USD at the nominal type level; so I'm not seeing that INCOHERENT is a good choice to abuse for the purpose of roles. In particular, my proposal would reject an instance marked {-# INCOHERENT #-} if it appeared for a class marked {-# INSTANCEGUARDS #-}, under the proposal -- which is to validate eagerly that instances do not overlap.)

Last edited 2 years ago by AntC (previous) (diff)

comment:4 in reply to:  3 ; Changed 2 years ago by RyanGlScott

Replying to AntC:

IncoherentInstances is a module-wide setting; and nowadays deprecated in favour of the more surgical {-# INCOHERENT #-} pragma on the instance.

Does that also apply for the role mungling?

As far as I know, you do need to enable the IncoherentInstances extension proper in order to assign non-nominal roles to class parameters, as the {-# INCOHERENT #-} pragma only works for instance declarations, not class declarations. (This might be partly why you don't get a deprecation warning when enabling IncoherentInstances, but you do with OverlappingInstances, which doesn't have a dual purpose like IncoherentInstances does.)

How does the {-# INCOHERENT #-} pragma go for StandaloneDeriving or GeneralizedNewtypeDeriving? It seems to be accepted by GHC OK, does it have the right effect? (It's hard to put together a test case.)

I'm not sure I understand the question. Derived instances never use {-# INCOHERENT #-} (or even {-# OVERLAPS #-}/{-# OVERLAPPING #-}/{-# OVERLAPPABLE #-}, for that matter) in their emitted code, if that's what you're wondering.

comment:5 in reply to:  4 ; Changed 2 years ago by AntC

Replying to RyanGlScott:

IncoherentInstances is a module-wide setting; and nowadays deprecated in favour of the more surgical {-# INCOHERENT #-} pragma on the instance.

Does that also apply for the role mungling?

As far as I know, you do need to enable the IncoherentInstances extension proper in order to assign non-nominal roles to class parameters,

Thanks Ryan, yes that's what the User Guide says -- if I look up about Roles, section 9.36.

Then BTW the User Guide for IncoherentInstances section 9.8.3.6 doesn't mention it has anything to do with Roles, but only with Overlaps. Likewise the doco for -XIncoherentInstances compiler flag section 6.6.12; which also implies XOverlappingInstances. Does it?

as the {-# INCOHERENT #-} pragma only works for instance declarations, not class declarations. (This might be partly why you don't get a deprecation warning when enabling IncoherentInstances, but you do with OverlappingInstances, which doesn't have a dual purpose like IncoherentInstances does.)

Hmm. Certainly you could say that IncoherentInstances is a poor choice of name if what it means is IncoherentOverlaps. Giving it a "dual purpose" seems like asking for trouble. Why wasn't there a new flag for IncoherentInstanceRoles? (And "dual purpose" seems in violation of the principles in the debate just going on about derived instances for EmptyDataDecls.)

.

How does the {-# INCOHERENT #-} pragma go for StandaloneDeriving or GeneralizedNewtypeDeriving? It seems to be accepted by GHC OK, does it have the right effect? (It's hard to put together a test case.)

I'm not sure I understand the question. Derived instances never use {-# INCOHERENT #-} (or even {-# OVERLAPS #-}/{-# OVERLAPPING #-}/{-# OVERLAPPABLE #-}, for that matter) in their emitted code, ...

I managed to get GHC to accept Standalone

deriving instance {-# INCOHERENT #-}  Num USD

I think you're saying: that pragma would be ignored; wouldn't enable the incoherent Role (in absence of IncoherentInstances on the module); would complain if that instance overlaps. OK there couldn't be an overlap for USD; let's say deriving instance {-# INCOHERENT #-} Num a => Num (N a) where there's also a hand-crafted instance {-# OVERLAPS #-} Num (N Int) where ..., for newtype N a.

If the module has IncoherentInstances, do both those instances get accepted even without the pragmas? (Or perhaps a more devious scenario where one of the instances is imported.)

... if that's what you're wondering.

I'm wondering about the combination of these "dual purposes". Suppose I want GHC to trust the Roles on my instances; but I don't want instances to overlap. That is, if I by accident write instances that overlap, I want GHC to reject them.

Thinking out loud: I perhaps want the effect of IncoherentInstances on the module (to get Role mungling); but {-# NOOVERLAPS #-} on the instance -- no such pragma at the moment.

comment:6 in reply to:  5 Changed 2 years ago by AntC

Replying to AntC:

If the module has IncoherentInstances, do both those instances get accepted even without the pragmas? (Or perhaps a more devious scenario where one of the instances is imported.)

Yes, here we go:

{-# LANGUAGE GeneralizedNewtypeDeriving, StandaloneDeriving, FlexibleInstances,
                          IncoherentInstances  #-}

main = print $ MkN (7 :: Int) + MkN 5

newtype N a = MkN a   deriving (Show)

instance Num a => Num (N a) where
  MkN x + MkN y = MkN (x - y)

deriving instance Num (N Int)  

Without IncoherentInstances the MkN 7 + MkN 5 is rejected: overlapping instances [good! that's what I want].

With IncoherentInstances, this is accepted and prints 12. If I switch round the instance decls such that the hand-crafted one is for Num (N Int) and the derived is for Num (N a), this prints 2.

Ugh!

comment:7 Changed 2 years ago by simonpj

I didn't even know this. FWIW the relevant code is in TcTyClsDecls.checkValidRoleAnnots.

I think the right thing to do here is to use a different flag for the "allow a representational role annotation on a class", or better yet to make it a per-role-annotation flag.

Using IncoherentInstances for both that and the old meaning is asking for trouble. I think we could make this change without hurting anyone much, because I bet that almost no one uses a representational role annotation on a class!

(One other thought. Allowing per-decl things like {-# OVERLAPS #-} means you can't look at the top of the file and see what extensions it uses. Really we should have a language extensions {-# LANGUAGE OverlapsAllowed #-} or something, which enables the per-decl pragmas. Doing that would have a bigger impact!)

Last edited 2 years ago by simonpj (previous) (diff)

comment:8 Changed 2 years ago by adamgundry

Cc: adamgundry added

comment:9 Changed 2 years ago by goldfire

Keywords: Roles added

comment:10 Changed 2 years ago by Iceland_jack

I started a reddit discussion.

  • type role Coercible representational representational is an example of a "type class" with representational roles.
  • Well-Typed has a representational example that could be phantom (class Throws e).
  • Sjoerd Visscher wants this as early as 2 years ago.
  • I use it here to avoid an unsafeCoerce.
Last edited 18 months ago by Iceland_jack (previous) (diff)

comment:11 Changed 2 years ago by vagarenko

Cc: vagarenko added
Note: See TracTickets for help on using tickets.