Opened 10 years ago

Closed 10 years ago

#1118 closed bug (fixed)

Type check loop on impredicativaty + GADT mix

Reported by: japple Owned by: simonpj
Priority: normal Milestone: 6.6.1
Component: Compiler Version: 6.6
Keywords: impredicativity, GADTs Cc:
Operating System: Linux Architecture: x86
Type of failure: None/Unknown Test Case: boxy/Compose
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:


The type checker runs out of stack space on checking compose, but not compose' or composeS

{-# OPTIONS_GHC -fglasgow-exts #-}

module Compose where

data Z
data S n

data List n a where
    Nil :: List Z a
    (:-) :: a -> List n a -> List (S n) a

data Hold a = Hold (forall m . a m -> a (S m))

compose' :: List n (Hold a) -> a (S Z) -> a (S n)
compose' Nil x = x
compose' ((Hold f) :- fs) x = f (compose' fs x)

compose :: List n (forall m . a m -> a (S m)) -> a (S Z) -> a (S n)
compose Nil x = x
compose (f :- fs) x = f (compose fs x)

composeS :: [forall m . a m -> a m] -> a n -> a n
composeS [] x = x
composeS (f:fs) x = f (composeS fs x)

Change History (2)

comment:1 Changed 10 years ago by igloo

Milestone: 6.6.1
Owner: set to simonpj

Another one for you, Simon.

comment:2 Changed 10 years ago by simonpj

Resolution: fixed
Status: newclosed
Test Case: boxy/Compose

Jim, this seems to be OK in the HEAD, and also on the 6.6 branch, but it's certainly broken in 6.6 itself. Ideally I should track down exactly which patch fixed it, but that's a bit time consuming, so I propose simply to regard it as "already fixed".

Meanwhile I'll add it to the test suite, so we'll find out if it goes bad again.


Note: See TracTickets for help on using tickets.