Hi guys,<br><br>We are having trouble with the following program that uses type families:<br><br>&gt; class Blah f a where<br>&gt; &nbsp; blah :: a -&gt; T f f a<br>&nbsp;<br>&gt; class A f where<br>&gt; &nbsp; type T f :: (* -&gt; *) -&gt; * -&gt; *<br>
<br>the following function does not type:<br><br>&gt; wrapper :: forall a f . Blah f a =&gt; a -&gt; T f f a<br>&gt; wrapper x = blah x<br><br>GHC gives the error:<br><br>&nbsp;&nbsp;&nbsp; Couldn&#39;t match expected type `T f1 f1 a&#39;<br>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; against inferred type `T f f a&#39;<br>&nbsp;&nbsp;&nbsp; In the expression: blah x<br>&nbsp;&nbsp;&nbsp; In the definition of `wrapper&#39;: wrapper x = blah x<br><br>Maybe it is a problem with ambiguous types, namely &quot;f&quot; appears only in applications of &quot;T&quot;. But that is not the case, there is a &quot;naked&quot; f appearing as the argument of &quot;T f&quot;. But perhaps the type checker does not want to unify those two f&#39;s precisely because they are the arguments of &quot;T f&quot;.<br>
<br>I have tried to encode the above program using FunDeps, because this procedure helps me understand type errors. But in this case I get no type error!<br><br>&gt; class A&#39; (f :: * -&gt; *) (g :: (* -&gt; *) -&gt; * -&gt; *) | f -&gt; g where<br>
<br>&gt; class Blah&#39; f a where<br>&gt; &nbsp; blah&#39; :: A&#39; f g =&gt; a -&gt; g f a<br><br>&gt; wrapper&#39; :: forall a f g . (Blah&#39; f a,A&#39; f g) =&gt; a -&gt; g f a<br>&gt; wrapper&#39; x = blah&#39; x<br><br>
So my question is whether my encoding is correct. And if it is, why isn&#39;t the type families version working?<br><br>Thanks!<br><br>Alexey<br><br>