Opened 4 years ago

Closed 4 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 4 years ago by

### comment:2 Changed 4 years ago by

difficulty: | → Unknown |
---|---|

Resolution: | → fixed |

Status: | new → closed |

Test Case: | → gadt/T7293 |

**Note:**See TracTickets for help on using tickets.

commit 629d1f48b513be3cc662ea79376737dbcdb6b18f