Opened 10 years ago

Closed 9 years ago

#3584 closed bug (invalid)

type signature involving a type family rejected

Reported by: baramoglo Owned by:
Priority: normal Milestone: 7.0.1
Component: Compiler (Type checker) Version: 6.10.2
Keywords: Cc: 78emil@…
Operating System: Unknown/Multiple Architecture: x86
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

add1 is rejected in the following program:

{-# LANGUAGE EmptyDataDecls, FlexibleContexts, FlexibleInstances, GADTs, TypeFamilies, TypeOperators, UndecidableInstances #-}

data False

type family IsNegative x

type family x :+: y

class Natural x
instance (IsNegative x ~ False) => Natural x

data A n
  where
    A :: Natural n => Int -> A n

getA :: A n -> Int
getA (A n) = n

add1 :: Natural (m:+:n) => A m -> A n -> A (m:+:n)
add1 (A a) (A b) = A (a+b)

add2 (A a) (A b) = A (a+b)

add3 :: (IsNegative (m:+:n) ~ False) => A m -> A n -> A (m:+:n)
add3 (A a) (A b) = A (a+b)

add4 :: Natural (m:+:n) => A m -> A n -> A (m:+:n)
add4 a b = A (getA a + getA b)

add5 :: Natural (m:+:n) => A m -> A n -> A (m:+:n)
add5 (A a) _ = A a

The following modifications of add1 work fine:

  • Removing the type signature (add2)
  • Using the type inferred for add2 (add3)
  • Using the projection function getA instead of pattern matching (add4)
  • Only pattern match on the first argument

Change History (3)

comment:1 Changed 10 years ago by simonpj

difficulty: Unknown

The problem is your instance for Natural x. You are saying "If you want to prove Natural x, then please prove (IsNegative x ~ False)". Now in the RHS of add1, GHC is faced with thee following problem:

 From   (Natural (m:+:n),     -- From signature
         Natural n,           -- From first pattern match
         Natural m)           -- From second pattern match
please prove
         Natural (m:+:n)

That seems easy enough, since the thing to prove is one of the premises. But a possible reasoning step is to use the instance declaration first, leading to

please prove
         IsNegative (m:+:n) ~ False

which we obviously can't do. Your instance declaration promises an alternative way to prove a constraint (Natural ty), but one which turns out to be a blind alley. But GHC does not search for a proof; it follows just one path. (In general the search could be very complicated.)

Nevertheless, I think there is a bug here: GHC should really not use an instance declaration if there is any possibility that one of the local premises might match, rather in the same way that it refrains from committing to one instance if more than one matches. Thanks for pointing this out.

Simon

comment:2 Changed 10 years ago by igloo

Milestone: 6.14.1

comment:3 Changed 9 years ago by simonpj

Resolution: invalid
Status: newclosed
Type of failure: None/Unknown

Hmm. Since there is only one instance for Natural GHC is right to use the (only) instance declaration. So I think there is no bug here and I'm therefore closing it.

Simon

Note: See TracTickets for help on using tickets.