Ticket #1815 (closed bug: fixed)

Opened 1 year ago

Last modified 1 year ago

Occurs check error from equality constraint

Reported by: guest Assigned to: chak
Priority: normal Milestone: 6.10 branch
Component: Compiler (Type checker) Version: 6.9
Severity: normal Keywords:
Cc: Difficulty: Unknown
Test Case: indexed-types/should_compile/GADT11 Architecture: x86
Operating System: Linux

Description

I was writing that manipulates witnesses for equality constraints, and saw some occurs check errors for equations matching my constraints. (This is with ghc-6.9.20071025). 

Bug.hs:19:31:
    Occurs check: cannot construct the infinite type: n = Sum Z n
    In the pattern: Refl
    In a case alternative: Refl -> Refl
    In the expression: case zerol n of Refl -> Refl

Here is the program producing that error: 

{-# OPTIONS -fglasgow-exts #-}
module Bug where

data Z
data S a

type family Sum n m
type instance Sum n Z = n
type instance Sum n (S m) = S (Sum n m)

data Nat n where
  NZ :: Nat Z
  NS :: (S n ~ sn) => Nat n -> Nat sn

data EQ a b = forall q . (a ~ b) => Refl

zerol :: Nat n -> EQ n (Sum Z n)
zerol NZ = Refl
zerol (NS n) = case zerol n of Refl -> Refl

Change History

11/04/07 18:18:52 changed by chak

  • owner set to chak.
  • milestone set to 6.10 branch.

At the moment type families/equality constraints are not fully integrated with GADTs yet. This should change soon and then this problem should also go away.

12/10/07 21:43:29 changed by chak

  • status changed from new to closed.
  • resolution set to fixed.

12/10/07 21:52:49 changed by chak

  • testcase set to indexed-types/should_compile/GADT11.