Opened 5 years ago
Closed 5 years ago
#3383 closed bug (worksforme)
Confluent type family instances confuse the solver
Reported by: | desp | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | Compiler (Type checker) | Version: | 6.10.3 |
Keywords: | type family families instance instances | Cc: | |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | Difficulty: | ||
Test Case: | Blocked By: | ||
Blocking: | Related Tickets: |
Description
While attempting to define integer arithmetic using type families, I encountered a problem with the type checker failing to recognize equivalent types:
{-# LANGUAGE EmptyDataDecls, TypeFamilies #-} module WithBug where data Z data S a data P a b type family N a type instance N (P Z a) = P Z a type instance N (P a Z) = P a Z -- with bug type instance N (P (S a) (S b)) = N (P a b)
$ ghci WithBug *WithBug> :t (undefined :: N (P Z Z)) :: P Z Z <interactive>:1:1: Couldn't match expected type `P Z Z' against inferred type `N (P Z Z)' In the expression: (undefined :: N (P Z Z)) :: P Z Z
Rewriting the problematic instance fixed the problem:
{-# LANGUAGE EmptyDataDecls, TypeFamilies #-} module WithoutBug where data Z data S a data P a b type family N a type instance N (P Z a) = P Z a type instance N (P (S a) Z) = P (S a) Z -- without bug type instance N (P (S a) (S b)) = N (P a b)
$ ghci WithoutBug *WithoutBug> :t (undefined :: N (P Z Z)) :: P Z Z (undefined :: N (P Z Z)) :: P Z Z :: P Z Z
Change History (2)
comment:1 Changed 5 years ago by desp
- Summary changed from Confluent type instances confuse the solver to Confluent type family instances confuse the solver
comment:2 Changed 5 years ago by chak
- Resolution set to worksforme
- Status changed from new to closed
Note: See
TracTickets for help on using
tickets.
This bug has already been fixed in the HEAD.