Opened 3 months ago

Last modified 2 months ago

#14366 new bug

Type family equation refuses to unify wildcard type patterns

Reported by: RyanGlScott Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 8.2.1
Keywords: TypeFamilies, TypeInType Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

This typechecks:

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}

import Data.Kind
import Data.Type.Equality

type family Cast (e :: a :~: b) (x :: a) :: b where
  Cast Refl x = x

However, if you try to make the kinds a and b explicit arguments to Cast:

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}

import Data.Kind
import Data.Type.Equality

type family Cast (a :: Type) (b :: Type) (e :: a :~: b) (x :: a) :: b where
  Cast _ _ Refl x = x

Then GHC gets confused:

GHCi, version 8.2.1: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/ryanglscott/.ghci
[1 of 1] Compiling Main             ( Bug.hs, interpreted )

Bug.hs:9:12: error:
    • Expected kind ‘_ :~: _1’, but ‘'Refl’ has kind ‘_ :~: _’
    • In the third argument of ‘Cast’, namely ‘Refl’
      In the type family declaration for ‘Cast’
  |
9 |   Cast _ _ Refl x = x
  |            ^^^^

A workaround is to explicitly write out what should be inferred by the underscores:

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}

import Data.Kind
import Data.Type.Equality

type family Cast (a :: Type) (b :: Type) (e :: a :~: b) (x :: a) :: b where
  Cast a a Refl x = x

Change History (6)

comment:1 Changed 3 months ago by goldfire

I could go either way on this one. (Where I'm choosing between "that's correct behavior" and "that's a bug".) I interpret _ in a type family equation to mean the same as a fresh type variable. And I also think that Cast a b Refl x = x is suspect. On the other hand, this is a bit silly of GHC not to unify.

comment:2 Changed 3 months ago by RyanGlScott

Ah, you bring up a good point. I suppose the thing we really should be scrutinizng is Cast a b Refl x = x. I'm also a bit baffled that that doesn't work either—after all, something quite similar works at the term level!

{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}

import Data.Type.Equality

cast :: a :~: b -> a -> b -> Int
cast Refl (_ :: a) (_ :: b) = 42

I'm aware that this is a bit of a strawman, since comparing type families and scoped type pattern variables is a bit apples-and-oranges. But surely you can see the point I'm driving at here—if a and b are equated by the pattern match on Refl, should we reject the use of two syntactically different type variables for the second and third arguments of cast?

comment:3 Changed 3 months ago by RyanGlScott

Contrast this with a similar type family declaration, which is rejected:

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}

import Data.Kind
import Data.Type.Equality
import GHC.TypeNats

type family Cast (e :: a :~: b) (x :: a) (y :: b) :: Nat where
  Cast Refl (_ :: a) (_ :: b) = 42
GHCi, version 8.2.1: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main             ( Bug.hs, interpreted )

Bug.hs:10:22: error:
    • Expected kind ‘a’, but ‘_’ has kind ‘b’
    • In the third argument of ‘Cast’, namely ‘(_ :: b)’
      In the type family declaration for ‘Cast’
   |
10 |   Cast Refl (_ :: a) (_ :: b) = 42
   |                      ^^^^^^^^

comment:4 Changed 3 months ago by goldfire

I'm pretty sure Agda used to reject having two different variables here, though it seems to be accepting it now. (Any Agda experts out there?)

I think the pattern-signature version is a red herring, because those variables are meant to stand in for others -- indeed, that's their whole point.

But I'm still not terribly bothered by this rejection. Yes, I suppose it's better to accept here, but I don't think that goal is easily achieved.

comment:5 Changed 3 months ago by simonpj

These wildcards are more like wildards in types. E.g

f :: _ -> _
f x = x

Here f gets the infeerred type f :: forall a. a -> a, and both _ holes are reported as standing for a.

Similarly (untested) you can write wildcards in pattern signatures. Thus:

f :: a -> (a -> Char -> Bool) -> Bool
f x (g :: p -> _ -> _) = g (x :: p) 'v' :: Bool

Here the pattern tyupe (p -> _ -> _) gives the shepe of the type expected for g. But the two underscores can certainly turn out to the same type.

So I think yes, we should accept the Description. I don't know how hard it'd be.

comment:6 Changed 2 months ago by RyanGlScott

Here's a much simpler example that is rejected due to this limitation:

{-# LANGUAGE TypeFamilies #-}
module Bug where

type family F (a :: *) :: * where
  F (a :: _) = a
$ /opt/ghc/8.2.1/bin/ghci Bug.hs
GHCi, version 8.2.1: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/ryanglscott/.ghci
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )

Bug.hs:5:5: error:
    • Expected a type, but ‘a’ has kind ‘_’
    • In the first argument of ‘F’, namely ‘(a :: _)’
      In the type family declaration for ‘F’
  |
5 |   F (a :: _) = a
  |     ^^^^^^^^
Note: See TracTickets for help on using tickets.