Opened 3 years ago
Closed 3 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 Rev(s): | ||
Wiki Page: |
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 3 years ago by simonpj@…
comment:2 Changed 3 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.
commit 629d1f48b513be3cc662ea79376737dbcdb6b18f