Opened 5 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 (6)

### comment:1 Changed 5 months ago by

### comment:2 Changed 5 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 5 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 5 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 5 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 5 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 | ^^^^^^^^

**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.