How can I prove to GHC that (b ~ Foo)?

Question

New Question

I'm not going to pretend that I know how to think or talk about haskell. In pseudo-java-oo-jargon:

What I want to do is have a "structure" that "implements" an "interface." Part of that interface is a function which returns an object which implements another interface.

interface IFiz {}

interface IBuz {
    function IFiz getFiz() 
}

class Foo implements IFiz { ... }
class Bar implements IBuz {
    IFiz fiz = new Foo();
    function getFiz() {
        return fiz;
    }
}

How can I do this in Haskell? My attempt at doing this is described below.

---

Old Question

How can I prove to GHC that (b ~ Foo)?

My understanding of the problem:

Foo is an instance of the type class Fiz.

I would like Bar to be an instance of the type class Buz.

However, the compiler is unable to deduce that (b ~ Foo) in the implementation of the punk method. But what else could it be? I attempted to add data constraints using the deprecated direct way, as well as using GADTs, but neither seemed to work (I continued to get the exact same error.)

data Foo = Foo Int                                                                                                                                                                                                                           
data Bar = Bar Foo                                                                                                                                                                                                                           
                                                                                                                                                                                                                                           
class Fiz a where                                                                                                                                                                                                                            
    funk :: a -> a -- Not important, I just wanted to put something in Fiz                                                                                                                                                                                                                           
                                                                                                                                                                                                                                           
class Buz a where                                                                                                                                                                                                                            
    punk :: Fiz b => a -> b                                                                                                                                                                                                                  
                                                                                                                                                                                                                                           
instance Fiz Foo where                                                                                                                                                                                                                       
    funk a = a                                                                                                                                                                                                                               
                                                                                                                                                                                                                                           
instance Buz Bar where                                                                                                                                                                                                                       
   punk (Bar foo) = foo

---

Could not deduce (b ~ Foo)
from the context (Fiz b)
  bound by the type signature for punk :: Fiz b => Bar -> b
  at Test.hs:42:5-8
  ‘b’ is a rigid type variable bound by
      the type signature for punk :: Fiz b => Bar -> b at Test.hs:42:5
Relevant bindings include punk :: Bar -> b (bound at Test.hs:42:5)
In the expression: foo
In an equation for ‘punk’: punk (Bar foo) = foo

Answer 1

This type signature:

class Buz a where
  punk :: Fiz b => a -> b

says that punk must be able to return something of type b for any type b given it is instance of Fiz. So the problem is not that compiler cannot deduce that Foo is instance of Fiz, but that the return value is not Quux, which is an instance of Fiz.

data Quux = Quux 

instance Fiz Quux where
  funk a = a

If you want to have type class with function returning any instance of Fiz, you can use ExistentionalQuantification extension:

{-# LANGUAGE RankNTypes, ExistentialQuantification #-}   
data Foo = Foo Int
data Bar = Bar Foo
data SomeFiz = forall a . Fiz a => SomeFiz a
class Fiz a where
  funk :: a -> a

class Buz a where
  punk :: a -> SomeFiz

instance Fiz Foo where
  funk a = a

instance Buz Bar where
  punk (Bar foo) = SomeFiz foo

Otherwise if you really mean to implement this typeclass, you can only do this by passing bottoms to funk:

instance Buz Bar where
  punk _ = funk undefined
-- or for example:
instance Buz Bar where
  punk _ = funk (funk undefined)

or by fixing funk:

instance Buz Bar where
  punk _ = fix funk

If you could give more details on what you want to achieve, maybe I'll be able to give more helpful answer.

Answer 2

You can't.

The class Buz says that if a has an instance for Buz, then for every b that has a Fiz instance, you can provide a function from a -> b. The class Fiz provides virtually no help in producing a b; funk will only give you a b if you already have a b.

You are probably misunderstanding the error message from GHC. Type inference goes both ways. In this case, b comes from the signature for punk in the class Buz. It requires that the result of punk be something of type b for every type b. Foo is not something of every type.

  ‘b’ is a rigid type variable bound by
      the type signature for punk :: Fiz b => Bar -> b at Test.hs:42:5