On Sun, Dec 5, 2010 at 9:10 AM, Lukasz Stafiniak <lukstafi@gmail.com> wrote:
>
> I don't think that it is very different. Standard-language constraints
> are outside of implications, so they apply to each branch. It already
> behaves this way in the standard language, basically restricting the
> type family to "int term". So I don't see why
>
>> | Embed of 'a : 'a term
>>   constraint 'a = int
>
> shouldn't mean that Embed is "basically" Embed of int : int term.

[To clarify: and the whole family restricted to "int term".]