Opened 2 years ago

Closed 19 months ago

Last modified 13 months ago

#5591 closed bug (fixed)

Type constructor variables not injective

Reported by: daniel.is.fischer Owned by: simonpj
Priority: normal Milestone: 7.6.2
Component: Compiler (Type checker) Version: 7.2.1
Keywords: Cc: dimitris@…, sweirich@…, byorgey@…, illissius@…, adam.gundry@…, andy.adamsmoran@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Difficulty: Unknown
Test Case: indexed-ypes/should_compile/T5591a, T5591b Blocked By:
Blocking: Related Tickets:

Description

I'm not sure whether it is a bug, but there have been two recent reports of ghc-7.2.1 not treating type constructor variables as injective. First, by Daniel Schüssler,

{-# LANGUAGE GADTs, TypeOperators, TypeFamilies, ScopedTypeVariables #-}
module DTest where

data a :=: b where 
    Refl :: a :=: a

subst :: a :=: b -> f a -> f b
subst Refl = id 

-- Then this doesn't work (error message at the bottom):

inj1 :: forall f a b. f a :=: f b -> a :=: b
inj1 Refl = Refl

-- But one can still construct it with a trick that Oleg used in the context of 
-- Leibniz equality:

type family Arg fa

type instance Arg (f a) = a

newtype Helper fa fa' = Helper { runHelper :: Arg fa :=: Arg fa' }

inj2 :: forall f a b. f a :=: f b -> a :=: b
inj2 p = runHelper (subst p (Helper Refl :: Helper (f a) (f a)))

{-
DTest.hs:13:13:
    Could not deduce (a ~ b)
    from the context (f a ~ f b)
      bound by a pattern with constructor
                 Refl :: forall a. a :=: a,
               in an equation for `inj1'
      at DTest.hs:13:6-9
      `a' is a rigid type variable bound by
          the type signature for inj1 :: (f a :=: f b) -> a :=: b
          at DTest.hs:13:1
      `b' is a rigid type variable bound by
          the type signature for inj1 :: (f a :=: f b) -> a :=: b
          at DTest.hs:13:1
    Expected type: a :=: b
      Actual type: a :=: a
    In the expression: Refl
    In an equation for `inj1': inj1 Refl = Refl
-}

compiles fine with ghc-7.0.4. Second, by Sjoerd Visscher,

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, KindSignatures, 
    GADTs, FlexibleInstances, FlexibleContexts #-}
module STest where

class Monad m => Effect p e r m | p e m -> r where
  fin :: p e m -> e -> m r

data ErrorEff :: * -> (* -> *) -> * where 
  CatchError :: (e -> m a) -> ErrorEff ((e -> m a) -> m a) m

instance Monad m => Effect ErrorEff ((e -> m a) -> m a) a m where
  fin (CatchError h) = \f -> f h

{-
STest.hs:12:32:
    Could not deduce (a1 ~ a)
    from the context (Monad m)
      bound by the instance declaration at STest.hs:11:10-59
    or from (((e -> m a) -> m a) ~ ((e1 -> m a1) -> m a1))
      bound by a pattern with constructor
                 CatchError :: forall (m :: * -> *) e a.
                               (e -> m a) -> ErrorEff ((e -> m a) -> m a) m,
               in an equation for `fin'
      at STest.hs:12:8-19
      `a1' is a rigid type variable bound by
           a pattern with constructor
             CatchError :: forall (m :: * -> *) e a.
                           (e -> m a) -> ErrorEff ((e -> m a) -> m a) m,
           in an equation for `fin'
           at STest.hs:12:8
      `a' is a rigid type variable bound by
          the instance declaration at STest.hs:11:46
    Expected type: e1 -> m a1
      Actual type: e -> m a
    In the first argument of `f', namely `h'
    In the expression: f h
-}

also compiles fine with 7.0.4. ghc-7.3.20111026 behaves like 7.2.1. Which version behaves correctly?

Change History (9)

comment:1 Changed 2 years ago by danielo

I reduced second example, compiles in 7.0.3, but not in 7.3.20111021. Seems a serious shortcoming to me

{-# LANGUAGE GADTs #-}

data ErrorEff x where
  CatchError :: m a -> ErrorEff (m a)

fin :: ErrorEff (m a) -> m a
fin (CatchError h) = h

comment:2 Changed 2 years ago by simonpj

  • Cc dimitris@… sweirich@… byorgey@… added

As Brent describes on StackOverflow, we did make a change that simplified GHC's internal language a bit, and allowed us to have unsaturated type functions. The change is described in 6.2 of our POPL'11 paper Generative type abstraction and type-level computation.

Daniel Shussler's email also describes a trick due to Oleg that makes his program compile. Well, it turns out that this trick is really a bug; with the restrictions describe in our paper, we should not allow type functions to match on an argument of shape (a b).

So far as we can all remember, the only reason for the new story was to allow un-saturated type functions in the intermediate language. But we can't allow them in the source language because that would mess up type inference. So we are paying the price (exemplified by this ticket) without getting much benefit.

Brent's conclusion on StackOverflow is that we should go back to

  • having left and right coercion combinators
  • requiring type functions to be saturated in the intermediate language (as well as source)

And that in turn would allow us to type check the program in this ticket.

So that's the plan I think. But gotta get 7.4 out first.

Simon

comment:3 Changed 2 years ago by igloo

  • Milestone set to 7.6.1
  • Owner set to simonpj

comment:4 Changed 23 months ago by illissius

  • Cc illissius@… added

comment:5 Changed 23 months ago by simonpj

  • Difficulty set to Unknown

illissius, do you have an application in mind?

comment:6 Changed 20 months ago by adamgundry

  • Cc adam.gundry@… added

comment:7 Changed 20 months ago by igloo

  • Milestone changed from 7.6.1 to 7.6.2

comment:8 Changed 19 months ago by simonpj

  • Resolution set to fixed
  • Status changed from new to closed
  • Test Case set to indexed-ypes/should_compile/T5591a, T5591b

Fixed at last; see #7205. I added both examples as regression tests.

Simon

comment:9 Changed 13 months ago by morabbin

  • Cc andy.adamsmoran@… added

Is this related to #6018? Brent's stack overflow comment seems to imply it is.

Note: See TracTickets for help on using tickets.