Skip to content

GHC forgets constraints

Possibly related: #10338

The following program should compile, but fails with the error:

Could not deduce (Bar (F zq) zq) arising from a use of ‘bar’
    from the context (Bar (Foo (F zq)) (Foo zq))
      bound by the type signature for
                 bug :: Bar (Foo (F zq)) (Foo zq) => Foo (F zq) -> Foo zq

This is definitely incorrect: I am providing a Bar constraint in the context of bug, but GHC is asking for constraints so that it can resolve to the instance declared in Bar.hs.

A few workarounds I've found so far, which may or may not help find the bug:

  1. Adding -XTypeFamilies to Main.hs makes the program compile.
  2. Removing the type signature from x in bug makes the program compile.
  3. Defining bug without a let as bug sk = bar sk :: Foo zq or bug sk = bar sk makes the program compile.
  • *Main.hs:**
{-# LANGUAGE FlexibleContexts, ScopedTypeVariables #-}

module Main where

import Bar

bug :: forall zq . 
  (Bar (Foo (F zq)) (Foo zq))
  => Foo (F zq) -> Foo zq
bug sk = 
  let x = bar sk :: Foo zq
  in x
  • *Bar.hs**
{-# LANGUAGE MultiParamTypeClasses, TypeFamilies #-}

module Bar where

type family F b

newtype Foo r = Foo r

type instance F (Foo r) = Foo (F r)

class Bar a b where
  bar :: a -> b

instance (Bar a b) => Bar (Foo a) (Foo b)
Edited by Ben Gamari
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information