Opened 15 months ago

Last modified 14 months ago

#11995 new bug

Can't infer type

Reported by: Iceland_jack Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 8.1
Keywords: TypeInType Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description (last modified by thomie)

{-# LANGUAGE RankNTypes, LambdaCase, TypeOperators,
             TypeInType, UnicodeSyntax, GADTs #-}

module T11995 where

import Data.Kind

data NP :: forall k. (ĸ  Type)  ([k]  Type) where
  Nil  :: NP f '[]
  (:*) :: f x  NP f xs  NP f (x:xs)

newtype K a b = K a deriving Show
unK (K a) = a

h'collapse :: NP (K a) xs -> [a]
h'collapse = \case
  Nil     -> []
  K x:*xs -> x : h'collapse xs

if we replace xs by an underscore:

tJN0.hs:13:29-30: error: …
    • Could not deduce: (xs :: [ĸ]) ~~ ((':) ĸ x xs :: [ĸ])
      from the context: ((k :: *) ~~ (ĸ :: *),
                         (t :: [k]) ~~ ((':) ĸ x xs :: [ĸ]))
        bound by a pattern with constructor:
                   :* :: forall k (f :: k -> *) (x :: k) (xs :: [k]).
                         f x -> NP k k f xs -> NP k k f ((':) k x xs),
                 in a case alternative
        at /tmp/tJN0.hs:13:3-9
      ‘xs’ is a rigid type variable bound by
        a pattern with constructor:
          :* :: forall k (f :: k -> *) (x :: k) (xs :: [k]).
                f x -> NP k k f xs -> NP k k f ((':) k x xs),
        in a case alternative
        at /tmp/tJN0.hs:13:3
      Expected type: NP ĸ k (K ĸ a) t
        Actual type: NP ĸ ĸ (K ĸ a) xs
    • In the first argument of ‘h'collapse’, namely ‘xs’
      In the second argument of ‘(:)’, namely ‘h'collapse xs’
      In the expression: x : h'collapse xs
    • Relevant bindings include
        xs :: NP ĸ ĸ (K ĸ a) xs (bound at /tmp/tJN0.hs:13:8)
        h'collapse :: NP ĸ k (K ĸ a) t -> [a] (bound at /tmp/tJN0.hs:11:1)
Compilation failed.

Should it not be able to infer that?

The Glorious Glasgow Haskell Compilation System, version 8.1.20160419

Change History (2)

comment:1 Changed 14 months ago by thomie

Description: modified (diff)
Keywords: TypeInType added

comment:2 Changed 14 months ago by goldfire

This is correct behavior.

Though I failed to find a mention of the fact in either the user manual or in the Haskell 2010 report, a function can use polymorphic recursion only when given a type signature. The Wikipedia page on polymorphic recursion may be helpful. When you stub out the xs with an underscore, GHC considers the type signature to be incomplete and it does type inference -- not type checking -- on the function. Your function is polymorphically recursive, and so this fails.

Still remaining to do:

  • improve the error message to mutter about polymorphic recursion (not sure if this is at all possible)
  • find and/or create documentation to this effect.
Note: See TracTickets for help on using tickets.