Opened 4 years ago

Last modified 10 months ago

#11621 new bug

GHC doesn't see () as a Constraint in type family

Reported by: Iceland_jack Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 7.10.1
Keywords: ConstraintKinds Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: #11715, #13742, #16139, #16148 Differential Rev(s):
Wiki Page:

Description (last modified by thomie)

{-# LANGUAGE DataKinds, TypeOperators, KindSignatures, MultiParamTypeClasses, TypeFamilies #-}

import GHC.Exts

class NotFound

type family 
  F b where
  F 'False = (NotFound :: Constraint)
  F 'True  = (() :: Constraint)

works fine. Removing all constraints and final line it works without any annotations and infers the type of F :: Bool -> Constraint:

type family
  F b where
  F 'False = NotFound

GHC seems determined that () :: Type unless explicitly told otherwise, I would like to be able to write:

type family 
  F b where
  F 'False = NotFound
  F 'True  = ()

Change History (11)

comment:1 Changed 4 years ago by thomie

Component: CompilerCompiler (Type checker)
Description: modified (diff)
Version: 8.17.10.1

comment:2 Changed 4 years ago by simonpj

See also #11715, which tackles the bigger picture

comment:3 Changed 2 years ago by spacekitteh

Has this been fixed?

comment:4 in reply to:  3 Changed 2 years ago by RyanGlScott

Replying to spacekitteh:

Has this been fixed?

No.

GHCi, version 8.3.20170516: 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:14: error:
    • Expected a constraint, but ‘()’ has kind ‘*’
    • In the type ‘()’
      In the type family declaration for ‘F’
   |
10 |   F 'True  = ()
   |              ^^

Again, this probably requires fixing #11715 first.

comment:5 Changed 2 years ago by simonpj

Keywords: ConstraintKinds added

See also #13742

comment:6 Changed 11 months ago by RyanGlScott

Astoundingly, this program appears to have fixed itself between GHC 8.4 and 8.6, since this program:

{-# LANGUAGE DataKinds, TypeOperators, KindSignatures, MultiParamTypeClasses, TypeFamilies #-}

import GHC.Exts

class NotFound

type family
  F b where
  F 'False = NotFound
  F 'True  = ()

Typechecks without issue on GHC 8.6.2 and HEAD. Should we go ahead and add a test case for this, or is this program fragile without a full fix for #11715?

comment:7 Changed 11 months ago by RyanGlScott

Differential Rev(s): Phab:D5413
Status: newpatch

I decided to be bold and just submit a patch for this. See Phab:D5413.

comment:8 Changed 11 months ago by simonpj

I wish it was really fixed, but it isn't. Try this

type family F2 b where
  F2 'True  = ()
  F2 'False = NotFound

That elicits

T11621.hs:12:14: error:
    * Expected a type, but `NotFound' has kind `Constraint'
    * In the type `NotFound'
      In the type family declaration for `F2'
   |
12 |   F 'False = NotFound
   |              ^^^^^^^^

GHC is generally very good about being robustly order-independent; nothing depends on the order in which the type inference engine encounters code. But this is a rare counter example. The hack is described in Note [Inferring tuple kinds] in TcHsType.

In F, GHC sees NotFound first, and that tells it that the answer is Constraint. IN F2 it sees () first and guesses (wrongly) *.

So I would say not-fixed.

I can think of ad-hoc ways to fix this -- such as having a built-in constraint TK k which means k must be either * or Constraint. But I have thus far lacked the time and energy to think it through enough or implement it. Especially since #11715 is still open.

comment:9 Changed 11 months ago by RyanGlScott

Good catch. Alas, I had a feeling this was too good to be true.

comment:10 Changed 11 months ago by RyanGlScott

Differential Rev(s): Phab:D5413
Status: patchnew

comment:11 Changed 10 months ago by RyanGlScott

Note: See TracTickets for help on using tickets.