Changes between Version 3 and Version 4 of NewAxioms/DiscussionPage


Ignore:
Timestamp:
Jun 6, 2012 12:49:06 AM (23 months ago)
Author:
sweirich
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • NewAxioms/DiscussionPage

    v3 v4  
    4444  For example, at a use site for `F a b`, we can infer `a ~ Int` and `b ~ (Num b0) => b0`, but we can't refine `b` any further. So we don't have sufficient evidence to match pattern `F a a = True`; but neither can we move on to pattern `F a b = False`. 
    4545 
    46  
     46SCW: For these last two, it would be consistent with current treatment (and with multiple groups) to allow 'stuck' type families. Perhaps GHC could flag a few more bugs if the user could specify when a type family was expected to be fully covered, but I don't think that failing to do this check will jeopardize type soundness.   
    4747 
    4848== Suggestions ==