Opened 4 years ago

Closed 4 years ago

Last modified 4 years ago

#9888 closed bug (duplicate)

Inconsistent type family resolution

Reported by: crockeea Owned by:
Priority: normal Milestone:
Component: Compiler Version: 7.8.3
Keywords: 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 is as small as I'm able to make the example. It uses the singletons library. If I write my own Map type family, I can get the code to work. However, there seems to be a problem in GHC since I get seemingly conflicting information in GHCi.

{-# LANGUAGE TypeFamilies, TypeOperators, DataKinds, 
             FlexibleContexts, UndecidableInstances #-}

module Foo where

import Data.Singletons.Prelude hiding (And)

-- if every type in the list is equal, `CommonElt` returns the common type
type family CommonElt xs where
  CommonElt (x ': xs) = 
    EqResult (And (Map ((TyCon2 (==)) $ x) xs)) x

type family a == b where
  a == a = 'True
  a == b = 'False

type family And xs where
  And '[] = 'True
  And ('False ': xs) = 'False
  And ('True ': xs) = And xs

-- converts a True result to a type
type family EqResult b v where
  EqResult 'True r = r

type R = CommonElt '[Int, Int]

f :: R
f = 3

This code does not compile:

Foo.hs:30:5:
    No instance for (Num (EqResult (And ((Int == Int) :$$$ '[])) Int))
      arising from the literal ‘3’
    In the expression: 3
    In an equation for ‘f’: f = 3
Failed, modules loaded: none.

But if I comment out f and load the rest of the file in GHCi, I can easily see that R ~ Int:

> :kind! R
R :: *
= Int

This seems suspicious to me because GHCi can resolve the type of R, but when code requiring R to be resolved is compiled (in GHCi or with GHC), I get the error above. I believe that :kind! is correctly resolving the type to Int, and that the type error is a bug.

This is documented in more detail at this StackOverflow post.

Change History (2)

comment:1 Changed 4 years ago by goldfire

Resolution: duplicate
Status: newclosed

This looks like a duplicate of #9433. You've used (==) unapplied in your code, which is against the rules. It should be a syntax error, but instead, GHC attempts to make progress and falls flat on its face.

Instead of (TyCon2 (==)) in that spot, try (:==$).

comment:2 Changed 4 years ago by crockeea

@goldfire I get the same error using (:==$):

type family CommonElt xs where
  CommonElt (x ': xs) = 
    EqResult (And (Map ((:==$) $ x) xs)) x

but I think that is related to a singletons ticket

Last edited 4 years ago by crockeea (previous) (diff)
Note: See TracTickets for help on using tickets.