Status of Haskell Prime Language definition

[apfelmus]

Iavor Diatchki wrote:
>> http://hackage.haskell.org/trac/haskell-prime/wiki/FunctionalDependencies#Lossofconfluence
>
> There is nothing about the system being unsound there.  Furthermore, I
> am unclear about the problem described by the link...  The two sets of
> predicates are logically equivalent (have the same set of ground
> instances), here is a full derivation:
> 
> (B a b, C [a] c d)
> using the instance
> (B a b, C [a] c d, C [a] b Bool)
> using the FD rule
> (B a b, C [a] c d, C [a] b Bool, b = c)
> using b = c
> (B a b, C [a] c d, C [a] b Bool, b = c, C [a] b d)
> omitting unnecessary predicates and rearranging:
> (b = c, B a b, C [a] b d)
> 
> The derivation in the other direction is much simpler:
> (b = c, B a b, C [a] b d)
> using b = c
> (b = c, B a b, C [a] b d, C [a] c d)
> omitting unnecessary predicates
> (B a b, C [a] c d)

You're right, I think I'm mixing up soundness with completeness and 
termination. My thought was that not explicitly mentioning the b=c 
constraint could lead to the type inference silently dropping this fact 
and letting an inconsistent set of instance declarations "go through" 
without noticing. But that would only be important in a setting where 
inconsistent instances are not reported early via the consistency 
condition but late when actually constructing terms. The consistency 
condition should be enough for soundness (no inconsistent axioms 
accepted), but I didn't dwell enough into FD to know such things for sure.

Regards,
apfelmus