Opened 2 years ago

Closed 2 years ago

#7293 closed bug (fixed)

Wrong location reported for inaccessible code with GADTs

Reported by: goldfire Owned by:
Priority: normal Milestone:
Component: Compiler Version: 7.6.1
Keywords: GADTs Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: gadt/T7293
Blocked By: Blocking:
Related Tickets: Differential Revisions:

Description

Consider this code:

{-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeFamilies,
             TypeOperators #-}

data Nat = Zero | Succ Nat

data Vec :: * -> Nat -> * where
  Nil :: Vec a Zero
  Cons :: a -> Vec a n -> Vec a (Succ n)

type family (m :: Nat) :< (n :: Nat) :: Bool
type instance m :< Zero = False
type instance Zero :< Succ n = True
type instance Succ n :< Succ m = n :< m

data SNat :: Nat -> * where
  SZero :: SNat Zero
  SSucc :: forall (n :: Nat) => SNat n -> SNat (Succ n)

nth :: ((k :< n) ~ True) => Vec a n -> SNat k -> a
nth (Cons x _) SZero = x
nth (Cons _ xs) (SSucc k) = nth xs k
nth Nil _ = undefined

The pattern match on the last line is invalid and should indeed cause an error. However, the error is reported for the line declaring the type of nth, which is confusing. It seems the error should be reported at the location of the pattern match.

Here is the error:

/Users/rae/temp/sing.hs:20:8:
    Couldn't match type 'False with 'True
    Inaccessible code in
      the type signature for
        nth :: (k :< n) ~ 'True => Vec a n -> SNat k -> a

Change History (2)

comment:1 Changed 2 years ago by simonpj@…

commit 629d1f48b513be3cc662ea79376737dbcdb6b18f

Author: Simon Peyton Jones <[email protected]>
Date:   Thu Oct 4 17:54:38 2012 +0100

    Improve erorr location for Given errors
    
    Note [Inaccessible code].
    Fixes Trac #7293.

 compiler/typecheck/TcErrors.lhs  |   91 +++++++++++++++++++++++---------------
 compiler/typecheck/TcRnTypes.lhs |    5 ++-
 2 files changed, 59 insertions(+), 37 deletions(-)

comment:2 Changed 2 years ago by simonpj

  • difficulty set to Unknown
  • Resolution set to fixed
  • Status changed from new to closed
  • Test Case set to gadt/T7293
Note: See TracTickets for help on using tickets.