Unable to deduce two constrained types are the same

Question

I have a couple of classes that form part of a wider hierarchy and I'm trying to implement them on DepTag:

class StanfordType a where
  text :: a -> Text

class StanfordType a => Dep a where
  relation :: (StanfordType b) => a -> b

data DepTag a b where
  DepTag :: (StanfordType a) => Text -> a -> DepTag Text a

instance StanfordType (DepTag a b) where 
  text (DepTag s _) = s

instance Dep (DepTag a b) where 
  relation (DepTag _ r) = r

When I try to compile this, I'm thrown the following error:

• Could not deduce: b ~ b1
  from the context: (a ~ Text, N.StanfordType b)
    bound by a pattern with constructor:
               DepTag :: forall b. N.StanfordType b => Text -> b -> DepTag Text b,
             in an equation for ‘relation’
    at src/NLP/Data.hs:17:45-54
  ‘b’ is a rigid type variable bound by
    the instance declaration at src/NLP/Data.hs:17:10
  ‘b1’ is a rigid type variable bound by
    the type signature for:
      relation :: forall b1. N.StanfordType b1 => DepTag a b -> b1
    at src/NLP/Data.hs:17:35
• In the expression: r
  In an equation for ‘relation’: relation (DepTag _ r) = r
  In the instance declaration for ‘N.Dep (DepTag a b)’
• Relevant bindings include
    r :: b (bound at src/NLP/Data.hs:17:54)
    relation :: DepTag a b -> b1 (bound at src/NLP/Data.hs:17:35)

I can't work out why the compiler can't see that both r in relation (Dep) and b in the type signature of relation are the same. What am I missing here?


Show source
| haskell   2017-01-06 15:01 1 Answers

Answers to Unable to deduce two constrained types are the same ( 1 )

  1. 2017-01-06 16:01

    I can't work out why the compiler can't see that both r in relation (Dep) and b in the type signature of relation are the same.

    The problem is that they are not the same. The problem here is, that relation :: (Dep a, StanfordType b) => a -> b has to be able to return every valid b. So while your understanding of the type signature is that you can return any b that you (the writer of relation) want it actually means, that you have to return any b that I (the caller of relation) want. We can make this difference explicit like this (the second variant is not actual Haskell syntax and the first is not standard Haskell):

    relation :: forall b. (Dep a, StanfordType b) => a -> b -- Actual meaning
    relation :: exists b. (Dep a, StanfordType b) => a -> b -- Your interpretation
    

    So if make a type Foo, that is an instance of StanfordType:

    newtype Foo = Foo | Bar
    instance StanfordType Foo where
       text = pack "FooBar"
    

    you can now verify with GHCi, that resolution actually has to be able to return values of type Foo:

     > :t resolution :: Dep a => a -> Foo
     resolution :: Dep a => a -> Foo :: Dep a => a -> Foo
    

    Of course it is impossible to create values of any unknown type with a StanfordType instance. Especially because literally every type can have a StanfordType instance.

    We can actually express the second type using an existential:

    data ExtStanfordType where
       EST :: StanfordType a => a -> ExtStanfordType
    
    class StanfordType a => Dep a where
        relation :: a -> ExtStanfordType
    
    instance Dep (DepTag a b) where
        relation = (DepTag _ r) = EST r
    

    Now resolution can return any StanfordType wrapped up in an ExtStanfordType. You can then use text like this:

     textExt :: ExtStanfordType -> Text
     textExt (EST b) = text b
    

    See also: Existential type - Haskell Wiki

Leave a reply to - Unable to deduce two constrained types are the same

◀ Go back