Opened 5 years ago

Last modified 2 years ago

#9118 new feature request

Can't eta-reduce representational coercions

Reported by: goldfire Owned by:
Priority: low Milestone:
Component: Compiler (Type checker) Version: 7.8.2
Keywords: Roles Cc: mail@…, Iceland_jack
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: #9117 Differential Rev(s):
Wiki Page:

Description (last modified by simonpj)

When I say

import Data.Type.Coercion
import Data.Coerce
import Data.Proxy

eta2 :: Coercible (f a) (g a) => Proxy a -> Coercion f g
eta2 _ = Coercion

I get

    Could not coerce from ‘f’ to ‘g’
      because ‘f’ and ‘g’ are different types.
      arising from a use of ‘Coercion’
    from the context (Coercible (f a) (g a))
      bound by the type signature for
                 eta2 :: Coercible (f a) (g a) => Proxy a -> Coercion f g
      at /Users/rae/temp/Roles.hs:5:9-56
    In the expression: Coercion
    In an equation for ‘eta2’: eta2 _ = Coercion

Unlike the case for #9117, this one is not expressible in Core. (At least, I don't see a way to do it.) So, to do this, we would have to update Core and then update the constraint solver. I do think this would be type safe. But, I also think it's reasonable to wait for someone with a real use case to shout before doing this. The only use case I have is to be able to do this:

-- says that a's parameter is representational
class Rep (a :: k1 -> k2) where
  co :: Coercible x y => Coercible (a x) (a x)

instance Rep f => Rep (Compose f) where ...

Change History (10)

comment:1 Changed 5 years ago by nomeata

Cc: mail@… added

Wouldn’t you need something like

eta2 :: (forall a. Coercible (f a) (g a)) => Coercion f g

for this to be sound? Oterwise, assuming eta2 would typecheck, and we had eta from #9117 I could write

type family F1 a :: *
type family F2 a :: *
type instance F1 Int = Int
type instance F2 Int = Int
type instance F1 Bool = Bool
type instance F2 Bool = Char

and then obtain

let f1eqf2 = eta2 (Proxy :: Proxy Int) :: Coercion F1 F2
    absurd = (eta f1eqf2 :: Coercion (F1 Bool) (F2 Bool)) :: Coercion Bool Char

(dry coding, I might be wrong)

comment:2 Changed 5 years ago by simonpj

Description: modified (diff)

comment:3 Changed 5 years ago by rwbarton

nomeata: A type variable can't be instantiated at a(n unsaturated) type family (application), right? So Coercion F1 F2 isn't a legal type-level expression at all.

comment:4 Changed 5 years ago by nomeata

Possibly; I’m don’t know all the details of type families.

What eta2 :: Coercible (f a) (g a) => Proxy a -> Coercion f g says is: If f and g are the same for one arbitrary argument, they must be the same function. Maybe this is the case if type families are excluded for syntactical reasons. In that case, isn’t this an instance of #8555? We are given a more complex constraint Coercible (f a) (g a) and want to decompose it to the simpler Coercible f g.

comment:5 Changed 5 years ago by rwbarton

(Type families are like type synonyms in this regard; you can't define type Pair a = (a, a) and then talk about Functor Pair.)

It looks like #8555 is for Coercion (f a) (f b) -> Coercion a b, while this ticket is for Coercion (f a) (g a) -> Coercion f g. I don't know whether those are literally the same construction in Core but I expect they are equally easy if not.

comment:6 Changed 5 years ago by goldfire

I agree with rwbarton on this -- I think the F1/F2 example doesn't really apply.

But, there remains a problem case:

newtype Pair a = Mk (a, a)

We can easily derive Coercible (Pair Int) ((,) Int Int), but it would be bad to derive Coercible Pair ((,) Int). The problem is that the newtype definition has a repeated variable on the right, and thus the definition cannot be eta-reduced. Probably, a sufficiently complicated Core construction can detect and avoid this case, but I don't think it would be easy.

comment:7 Changed 4 years ago by nomeata

Priority: normallow

comment:8 Changed 4 years ago by thomie

Component: CompilerCompiler (Type checker)

comment:9 Changed 3 years ago by simonpj

Keywords: Roles added

comment:10 Changed 2 years ago by Iceland_jack

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