Opened 12 months ago

Last modified 7 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 12 months ago by

### comment:2 Changed 12 months ago by

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 12 months ago by

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 12 months ago by

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 12 months ago by

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 12 months ago by

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 7 months ago by

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.

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.