System Fc has another name: &quot;GHC Core&quot;.   You can read it by running &#39;ghc -ddump-ds&#39; (or, if you want to see the much later results after optimization, -ddump-simpl):<br><br>For example:<br><br>NonGADT.hs:<br>
<br>{-# LANGUAGE TypeFamilies, ExistentialQuantification, GADTs #-}<br>module NonGADT where<br><br>data T a = (a ~ ()) =&gt; T<br>f :: T a -&gt; a<br>f T = ()<br><br>x :: T ()<br>x = T<br><br>C:\haskell&gt;ghc -ddump-ds NonGADT.hs<br>
[1 of 1] Compiling NonGADT          ( NonGADT.hs, NonGADT.o )<br><br>==================== Desugar (after optimization) ====================<br>Result size = 17<br><br>NonGADT.f :: forall a_a9N. NonGADT.T a_a9N -&gt; a_a9N<br>
[LclIdX]<br>NonGADT.f =<br>  \ (@ a_acv) (ds_dcC :: NonGADT.T a_acv) -&gt;<br>    case ds_dcC of _ { NonGADT.T rb_dcE -&gt;<br>    GHC.Tuple.() `cast` (Sym rb_dcE :: () ~# a_acv)<br>    }<br><br>NonGADT.x :: NonGADT.T ()<br>
[LclIdX]<br>NonGADT.x = NonGADT.$WT @ () (GHC.Types.Eq# @ * @ () @ () @~ &lt;()&gt;)<br><br>The &quot;@&quot; is type application; &quot;cast&quot; is a system Fc feature that that allows type equality to be witnessed by terms;<br>
<br>Removing the module names and renaming things to be a bit more readable, we get:<br><br>f :: forall a. T a -&gt; a<br>f = \ (@ a) (x :: T a) -&gt; case x of { T c -&gt; () `cast` (Sym c :: () ~# a) }<br>-- Here ~# is an unboxed type equality witness; it gets erased during compilation.<br>
-- We need Sym c because c :: a ~# () and cast wants to go from () to a, so the<br>-- compiler uses Sym to swap the order.<br><br>x :: T ()<br>x = T @() (Eq# @* @() @() @~ &lt;()&gt;)<br>-- Eq# seems to be the constructor for ~#; I&#39;m not sure what the &lt;()&gt; syntax is.<br>
-- Notice the kind polymorphism; Eq# takes a kind argument as its first<br>-- argument, then two type arguments of that kind.<br><br>  -- ryan<br><br><div class="gmail_quote">On Fri, Aug 24, 2012 at 2:39 AM, Matthew Steele <span dir="ltr">&lt;<a href="mailto:mdsteele@alum.mit.edu" target="_blank">mdsteele@alum.mit.edu</a>&gt;</span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="im">On Aug 23, 2012, at 10:32 PM, wren ng thornton wrote:<br>
<br>
&gt; Now, be careful of something here. The reason this fails is because we&#39;re compiling Haskell to System Fc, which is a Church-style lambda calculus (i.e., it explicitly incorporates types into the term language). It is this fact of being Church-style which forces us to instantiate ifn before we can do case analysis on it. If, instead, we were compiling Haskell down to a Curry-style lambda calculus (i.e., pure lambda terms, with types as mere external annotations) then everything would work fine. In the Curry-style world we wouldn&#39;t need to instantiate ifn at a specific type before doing case analysis, so we don&#39;t have the problem of magicking up a type. And, by parametricity, the function fn can&#39;t do anything particular based on the type of its argument, so we don&#39;t have the problem of instantiating too early[1].<br>

<br>
</div>Okay, I think that&#39;s what I was looking for, and that makes perfect sense.  Thank you!<br>
<div class="im"><br>
&gt; Of course, (strictly) Curry-style lambda calculi are undecidable after rank-2 polymorphism, and the decidability at rank-2 is pretty wonky. Hence the reason for preferring to compile down to a Church-style lambda calculus. There may be some intermediate style which admits your code and also admits the annotations needed for inference/checking, but I don&#39;t know that anyone&#39;s explored such a thing. Curry-style calculi tend to be understudied since they go undecidable much more quickly.<br>

<br>
</div>Gotcha.  So if I&#39;m understanding correctly, it sounds like the answer to one of my earlier questions is (very) roughly, &quot;Yes, the original version of bar would be typesafe at runtime if the typechecker were magically able to allow it, but GHC doesn&#39;t allow it because trying to do so would get us into undecidability nastiness and isn&#39;t worth it.&quot;  Which is sort of what I expected, but I couldn&#39;t figure out why; now I know.<br>

<br>
I think now I will go refresh myself on System F (it&#39;s been a while) and read up on System Fc (which I wasn&#39;t previously aware of). (-:<br>
<br>
Cheers,<br>
-Matt<br>
<div class="HOEnZb"><div class="h5"><br>
<br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
</div></div></blockquote></div><br>