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

This bug has already been fixed in the HEAD.

Note: See TracTickets for help on using tickets.