Skip to content
Snippets Groups Projects

Functional dependencies and type families

    • Closed Issue created by Simon Peyton Jones @simonpj

    Consider

    type family F a :: *

class C a b | a -> b

instance C p (F q) => C p [q]

    Is the instance decl OK under the liberal coverage condition?

    That is, does (C t [s1], C t [s2]) mean that (s1 ~ s2)?

    NO! The context of the instance declaration means that p -> F q but that does not imply p -> q unless F is injective!

    So this program is wrongly accepted.

    I realised this when investigating #10778.

    Edited
    To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information

    Child items 0

    • No child items are currently assigned. Use child items to break down this issue into smaller parts.

    Activity

    Please register or sign in to reply