Opened 10 months ago

Last modified 5 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 (7)

comment:1 Changed 10 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 10 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 10 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 10 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 10 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 10 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
  |     ^^^^^^^^

comment:7 Changed 5 months ago by RyanGlScott

After reading #14938, I now understand at least why this is happening. I was operating under the misconception that pattern-matching in type families brings a coercion into scope, which would "force" the two wildcards in Cast _ _ Refl x = x to unify. But this isn't the case at all, as https://ghc.haskell.org/trac/ghc/ticket/14938#comment:5 explains—matching on Refl requires a coercion in order to type-check.

Unfortunately, the way type wildcards work is at odds with this, because early on in the renamer, GHC simply renames Cast _ _ Refl x = x to something like Cast _1 _2 Refl x = x. Because _1 and _2 aren't the same, matching on Refl :: _1 :~: _1 isn't going to work.

It seems like we'd need to somehow defer the gensymming of wildcard names until during typechecking to make this work. But the details of that are beyond me.

Note: See TracTickets for help on using tickets.