GHC 7.10.1 panic due to wildcard in data family instance

The following simple program causes GHC 7.10.1 (for x86_64-apple-darwin) to panic (rnHsTyKi HsWildcardTy):

 {-# LANGUAGE TypeFamilies, GADTs, DataKinds, PolyKinds #-}
    
data MyKind = A | B

data family Sing (a :: k)

data instance Sing (_ :: MyKind) where
    SingA :: Sing A
    SingB :: Sing B

Because data family instances must be fully saturated, we must give some name to the parameter; but because our instance is a GADT, the name of that parameter is meaningless, so using the wildcard makes complete sense here.

Trac metadata

Trac field	Value
Version	7.10.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

mentioned in issue #3699 (closed)

changed weight to 5

added Tbug Trac import labels

Allowing underscores there would be nice. See ticket #3699 (closed). But we surely shouldn't panic here.

Trac metadata

Trac field	Value
Related	→ #3699 (closed)

Yeah, even if they aren't supported (yet), we shouldn't panic! :)

closed

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedFixed

This is fixed in HEAD by D613.

Note that a proper error message is now generated, the wild card is not supported here.

Is it committed, or simply in Phab? Is there a regression test? If so can you update the "Test case" field? If not can you add one? Thanks

Replying to [ticket:10586#comment:102601 simonpj]:

Is it committed, or simply in Phab? Is there a regression test? If so can you update the "Test case" field? If not can you add one? Thanks

Yes. I have a test for a wild card in a type instance, I'll add one for this too then.

I'm actually thinking about adding support for wild cards in data/type instances. I would just replace them with fresh meta variables. This would also address #3699 (closed). I don't think named wild cards or extra-constraints wild cards make sense here. What do you think?

I'm actually thinking about adding support for wild cards in data/type instances. I would just replace them with fresh meta variables. This would also address #3699 (closed). I don't think named wild cards or extra-constraints wild cards make sense here. What do you think?

Yes, I agree. Do not use a meta variable. These are really skolems, just like the named type variables in an ordinary declaration, just anonymous ones.

Would need documentation about exactly where these skolem wildcards can appear.

Replying to [ticket:10586#comment:102606 simonpj]:

I'm actually thinking about adding support for wild cards in data/type instances. I would just replace them with fresh meta variables. This would also address #3699 (closed). I don't think named wild cards or extra-constraints wild cards make sense here. What do you think?

Yes, I agree. Do not use a meta variable. These are really skolems, just like the named type variables in an ordinary declaration, just anonymous ones.

Given the freshly generated Name of an anonymous wild card, which function should I use to create a skolem? newSigTyVar :: Name -> Kind -> TcM TcTyVar in TcMType using newMetaKindVar :: TcM TcKind as kind?

Follow the pattern in TcHsType.tcHsTyVarBndr (which in any case is probably the function you'll need to modify). It uses mkTcTyVar as far as I can see. Just do the same, but with a fresh Name.

Simon

reopened

Trac metadata

Trac field	Value
Resolution	ResolvedFixed → Unresolved
Differential revisions	- → D1092

assigned to @trac-thomasw

See D1092 for a patch adding support for wild cards in type/data family instance declarations.

mentioned in commit d9d2102e

closed

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedFixed

changed milestone to %8.0.1

added Pnormal label