Opened 2 years ago

Closed 9 months ago

#14366 closed bug (fixed)

Type family equation refuses to unify wildcard type patterns

Reported by: RyanGlScott Owned by:
Priority: normal Milestone: 8.8.1
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: typecheck/should_compile/T14366
Blocked By: Blocking:
Related Tickets: Differential Rev(s): Phab:D5229
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 (8)

comment:1 Changed 2 years 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 2 years 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 2 years 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 2 years 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 2 years 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 23 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 18 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.

comment:8 Changed 9 months ago by RyanGlScott

Differential Rev(s): Phab:D5229
Milestone: 8.8.1
Resolution: fixed
Status: newclosed
Test Case: typecheck/should_compile/T14366

This was fixed in 17bd163566153babbf51adaff8397f948ae363ca:

Author: mynguyen <mnguyen1@brynmawr.edu>
Date:   Tue Dec 18 11:52:26 2018 -0500

    Visible kind application
    
    Summary:
    This patch implements visible kind application (GHC Proposal 15/#12045), as well as #15360 and #15362.
    It also refactors unnamed wildcard handling, and requires that type equations in type families in Template Haskell be
    written with full type on lhs. PartialTypeSignatures are on and warnings are off automatically with visible kind
    application, just like in term-level.
    
    There are a few remaining issues with this patch, as documented in
    ticket #16082.
    
    Includes a submodule update for Haddock.
    
    Test Plan: Tests T12045a/b/c/TH1/TH2, T15362, T15592a
    
    Reviewers: simonpj, goldfire, bgamari, alanz, RyanGlScott, Iceland_jack
    
    Subscribers: ningning, Iceland_jack, RyanGlScott, int-index, rwbarton, mpickering, carter
    
    GHC Trac Issues: `#12045`, `#15362`, `#15592`, `#15788`, `#15793`, `#15795`, `#15797`, `#15799`, `#15801`, `#15807`, `#15816`
    
    Differential Revision: https://phabricator.haskell.org/D5229
Note: See TracTickets for help on using tickets.